[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : FreeGroup (Generators G) →* H
⊢ (fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G)))
      ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G)))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : FreeGroup (Generators G) →* H
a✝ : Generators G
⊢ ↑((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G)))
          ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G)))) f))
      (FreeGroup.of a✝) =
    ↑f (FreeGroup.of a✝)
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : G →* H
⊢ (fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G))))
      ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G))) f) =
    f
[PROOFSTEP]
ext
[GOAL]
case h
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : G →* H
x✝ : G
⊢ ↑((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv.symm (MulEquiv G))))
          ((fun f => MonoidHom.comp f (MulEquiv.toMonoidHom (MulEquiv G))) f))
      x✝ =
    ↑f x✝
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : IsFreeGroup G
H : Type u_2
inst✝ : Group H
f : Generators G → H
⊢ ∃! F, ∀ (a : Generators G), ↑F (of a) = f a
[PROOFSTEP]
simpa only [Function.funext_iff] using lift.symm.bijective.existsUnique f
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of) = MonoidHom.id (FreeGroup X)
[PROOFSTEP]
apply FreeGroup.ext_hom
[GOAL]
case h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ ∀ (a : X),
    ↑(MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of)) (FreeGroup.of a) =
      ↑(MonoidHom.id (FreeGroup X)) (FreeGroup.of a)
[PROOFSTEP]
intro x
[GOAL]
case h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
x : X
⊢ ↑(MonoidHom.comp (↑lift FreeGroup.of) (↑FreeGroup.lift of)) (FreeGroup.of x) =
    ↑(MonoidHom.id (FreeGroup X)) (FreeGroup.of x)
[PROOFSTEP]
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of, lift_of]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of) = MonoidHom.id G
[PROOFSTEP]
let lift_symm_of : ∀ {H : Type u} [Group H], ∀ (f : G →* H) (a), lift.symm f a = f (of a) := by intro H _ f a;
  simp [← lift_of (lift.symm f)]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
⊢ ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a)
[PROOFSTEP]
intro H _ f a
[GOAL]
G✝ : Type u_1
inst✝⁴ : Group G✝
inst✝³ : IsFreeGroup G✝
H✝ : Type u_2
inst✝² : Group H✝
G : Type u
inst✝¹ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
H : Type u
inst✝ : Group H
f : G →* H
a : X
⊢ ↑lift.symm f a = ↑f (of a)
[PROOFSTEP]
simp [← lift_of (lift.symm f)]
[GOAL]
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
⊢ MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of) = MonoidHom.id G
[PROOFSTEP]
apply lift.symm.injective
[GOAL]
case a
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
⊢ ↑lift.symm (MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of)) = ↑lift.symm (MonoidHom.id G)
[PROOFSTEP]
ext x
[GOAL]
case a.h
G✝ : Type u_1
inst✝³ : Group G✝
inst✝² : IsFreeGroup G✝
H : Type u_2
inst✝¹ : Group H
G : Type u
inst✝ : Group G
X : Type u
of : X → G
lift : {H : Type u} → [inst : Group H] → (X → H) ≃ (G →* H)
lift_of : ∀ {H : Type u} [inst : Group H] (f : X → H) (a : X), ↑(↑lift f) (of a) = f a
lift_symm_of : ∀ {H : Type u} [inst : Group H] (f : G →* H) (a : X), ↑lift.symm f a = ↑f (of a) :=
  fun {H} [Group H] f a =>
    of_eq_true
      (Eq.trans
        (congrFun
          (congrArg Eq
            (Eq.trans ((fun a => Eq.symm (lift_of (↑lift.symm f) a)) a)
              (congrFun (congrArg FunLike.coe (Equiv.apply_symm_apply lift f)) (of a))))
          (↑f (of a)))
        (eq_self (↑f (of a))))
x : X
⊢ ↑lift.symm (MonoidHom.comp (↑FreeGroup.lift of) (↑lift FreeGroup.of)) x = ↑lift.symm (MonoidHom.id G) x
[PROOFSTEP]
simp only [MonoidHom.coe_comp, Function.comp_apply, MonoidHom.id_apply, FreeGroup.lift.of, lift_of, lift_symm_of]
