-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u_2
β : Type u_3
γ : Type u_4
inst : AddCommGroup γ
f : α → β
g : β → γ
x : FreeAbelianGroup α
zero :
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        0 :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) 0) :
      γ)
of :
  ∀ (x : α),
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          (FreeAbelianGroup.of x) :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (FreeAbelianGroup.of x) : FreeAbelianGroup β) :
        γ)
neg :
  ∀ (x : α)
    (h :
      Eq.{u_4 + 1} (α := γ)
        ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
              (a : FreeAbelianGroup α) → γ)
            (FreeAbelianGroup.of x) :
          γ)
        ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
              (a : FreeAbelianGroup β) → γ)
            ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (FreeAbelianGroup.of x) : FreeAbelianGroup β) :
          γ)),
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          (-FreeAbelianGroup.of x) :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (-FreeAbelianGroup.of x) : FreeAbelianGroup β) :
        γ)
⊢ Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        x :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
      γ)
have add : ∀ (x y : FreeAbelianGroup α)
  (h₁ :
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          x :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) x : FreeAbelianGroup β) :
        γ))
  (h₂ :
    Eq.{u_4 + 1} (α := γ)
      ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
            (a : FreeAbelianGroup α) → γ)
          y :
        γ)
      ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
            (a : FreeAbelianGroup β) → γ)
          ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) y : FreeAbelianGroup β) :
        γ)),
  Eq.{u_4 + 1} (α := γ)
    ((((lift : (a : α → γ) → FreeAbelianGroup α →+ γ) (g ∘ f) : AddMonoidHom.{u_2, u_4} (FreeAbelianGroup α) γ) :
          (a : FreeAbelianGroup α) → γ)
        (x + y) :
      γ)
    ((((lift : (a : β → γ) → FreeAbelianGroup β →+ γ) g : AddMonoidHom.{u_3, u_4} (FreeAbelianGroup β) γ) :
          (a : FreeAbelianGroup β) → γ)
        ((map f : (a : FreeAbelianGroup α) → FreeAbelianGroup β) (x + y) : FreeAbelianGroup β) :
      γ)
Tactic: induction x using FreeAbelianGroup.induction_on with
  | zero => simp only [map_zero]
  | of => simp only [lift_apply_of, map, Function.comp]
  | neg _ h => simp only [h, map_neg]
  | add _ _ h₁ h₂ => simp only [h₁, h₂, map_add]
Cleared hypotheses: x