mathlib4

mathlib4 copied to clipboard

## This is work in progress Current status: * `initialize_simps_projections` has been mostly ported and tested * documentation is copied from Lean 3, and needs a proofread * `@[simps]` has...

fpvandoorn

feat: generalize_proofs tactic

1

alexjbest

feat: port choose

1

jcommelin

The `simp_intro` tactic is a combination of `simp` and `intro`: it will simplify the types of variables as it introduces them and uses the new variables to simplify later arguments...

digama0

should `clear_` tactic also clear inaccessible hypotheses?

1

In mathlib3, `pairwise_and_iff` has a usage of `clear_` with this context: ``` α : Type u_1, R S : α → α → Prop, l : list α, _x :...

dwrensha

digama0

gebner

Port logic/relator.lean and add comments in the places where the linter demands them. Compare to the mathlib3 version: https://github.com/leanprover-community/mathlib/blob/7362d50a80c3e7f7a1fb5adb1c0b6ba593db103d/src/logic/relator.lean

dwrensha

copy lean3port/ported into mathlib4

1

https://github.com/leanprover-community/lean3port/compare/ported

gebner

gebner