Note about Mathlib/Init/

The files in Mathlib/Init are leftovers from the port from Mathlib3. (They contain content moved from lean3 itself that Mathlib needed but was not moved to lean4.)

We intend to move all the content of these files out into the main Mathlib directory structure. Contributions assisting with this are appreciated.

Quot

Some induction principles tagged with elab_as_elim, since the attribute is missing in core.

@[reducible, inline]

abbrev Quot.recOn' {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) (h : ∀ (a b : α) (p : r a b), ⋯ ▸ f a = f b) : motive q

Dependent recursion principle for Quot. This constructor can be tricky to use, so you should consider the simpler versions if they apply:

• Quot.lift, for nondependent functions
• Quot.ind, for theorems / proofs of propositions about quotients
• Quot.recOnSubsingleton, when the target type is a Subsingleton
• Quot.hrecOn, which uses HEq (f a) (f b) instead of a sound p ▸ f a = f b assummption

Equations

• Quot.recOn' q f h = Quot.rec f h q

@[reducible, inline]

abbrev Quot.recOnSubsingleton' {α : Sort u} {r : α → α → Prop} {motive : Quot r → Sort v} [h : ∀ (a : α), Subsingleton (motive (Quot.mk r a))] (q : Quot r) (f : (a : α) → motive (Quot.mk r a)) : motive q

Version of Quot.recOnSubsingleton tagged with elab_as_elim

Equations

• Quot.recOnSubsingleton' q f = Quot.rec (fun (a : α) => f a) ⋯ q

theorem Quotient.mk'_eq_mk {α : Sort u} [s : Setoid α] : Quotient.mk' = Quotient.mk s