α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b), liftOn q f h = f a
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b
a : α
aq : a ∈ q
⊢ liftOn q f h = f a
revert h
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b), liftOn (mk aq) f h = f a
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a : α), a ∈ q → ∀ (b : α), b ∈ q → f a = f b), liftOn q f h = f a
rw [eq_mk_of_mem aq]
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b
⊢ liftOn (mk aq) f h✝ = f a
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b), liftOn (mk aq) f h = f a
intro
no goals
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ (a_1 : α), a_1 ∈ mk aq → ∀ (b : α), b ∈ mk aq → f a_1 = f b
⊢ liftOn (mk aq) f h✝ = f a
rfl