α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = EqvGen.Setoid Setoid.r
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = mapOfSurjective r f h hf
rw [← eqvGen_of_setoid (mapOfSurjective r f h hf)]
no goals
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
h : ker f ≤ r
hf : Surjective f
⊢ map r f = EqvGen.Setoid Setoid.r
rfl