[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
⊢ ∀ {x : PresentedGroup rels}, ↑g x = ↑(toGroup h) x
[PROOFSTEP]
intro x
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ↑g x = ↑(toGroup h) x
[PROOFSTEP]
refine' QuotientGroup.induction_on x _
[GOAL]
α : Type u_1
G : Type u_2
inst✝ : Group G
f : α → G
rels : Set (FreeGroup α)
h : ∀ (r : FreeGroup α), r ∈ rels → ↑(↑FreeGroup.lift f) r = 1
g : PresentedGroup rels →* G
hg : ∀ (x : α), ↑g (PresentedGroup.of x) = f x
x : PresentedGroup rels
⊢ ∀ (z : FreeGroup α), ↑g ↑z = ↑(toGroup h) ↑z
[PROOFSTEP]
exact fun _ ↦ FreeGroup.lift.unique (g.comp (QuotientGroup.mk' _)) hg
