Quot

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

@[inline, reducible]

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), (_ : Quot.mk r a = Quot.mk r 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

@[inline, reducible]

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) (_ : ∀ (a b : α) (p : r a b), (_ : Quot.mk r a = Quot.mk r b) ▸ f a = f b) q

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