case mk
a b c d : Prop
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) (_ : mk r a = mk r b) = f b
a✝ : α
⊢ (lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) (mk r a✝)).fst = mk r a✝
a b c d : Prop
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) (_ : mk r a = mk r b) = f b
q : Quot r
⊢ (lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) q).fst = q
induction q using Quot.ind
no goals
case mk
a b c d : Prop
α : Sort u
r : α → α → Prop
motive : Quot r → Sort v
f : (a : α) → motive (mk r a)
h : ∀ (a b : α) (p : r a b), Eq.ndrec (f a) (_ : mk r a = mk r b) = f b
a✝ : α
⊢ (lift (Quot.indep f) (_ : ∀ (a b : α), r a b → Quot.indep f a = Quot.indep f b) (mk r a✝)).fst = mk r a✝
exact rfl