case h.e'_3.h
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : (fun x => β) (of x) = (fun x => Multiplicative β) (↑Abelianization.of (FreeGroup.of x))
⊢ f x = ↑(↑FreeGroup.lift f) (FreeGroup.of x)
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
⊢ ↑(↑lift f) (of x) = f x
convert Abelianization.lift.of
   (FreeGroup.lift f (β := Multiplicative β)) (FreeGroup.of x) using 1
no goals
case h.e'_3.h
α : Type u
β : Type v
inst✝ : AddCommGroup β
f : α → β
x : α
e_1✝ : (fun x => β) (of x) = (fun x => Multiplicative β) (↑Abelianization.of (FreeGroup.of x))
⊢ f x = ↑(↑FreeGroup.lift f) (FreeGroup.of x)
exact (FreeGroup.lift.of (β := Multiplicative β)).symm