-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
Goal:
α : Type u
G : Type u_1
inst : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
zero :
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      0 =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          0 :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          0 :
        G)
of :
  ∀ (x : α),
    (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        (FreeAbelianGroup.of x) =
      HAdd.hAdd (α := G) (β := G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (FreeAbelianGroup.of x) :
          G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (FreeAbelianGroup.of x) :
          G)
⊢ (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      a =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          a :
        G)
have neg : ∀ (x : α),
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        (FreeAbelianGroup.of x) =
      HAdd.hAdd (α := G) (β := G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (FreeAbelianGroup.of x) :
          G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (FreeAbelianGroup.of x) :
          G) →
    (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        (-FreeAbelianGroup.of x) =
      HAdd.hAdd (α := G) (β := G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (-FreeAbelianGroup.of x) :
          G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            (-FreeAbelianGroup.of x) :
          G)
Tactic: induction a using FreeAbelianGroup.induction_on with
  | zero => simp only [(lift _).map_zero, zero_add]
  | of x => simp only [lift_apply_of, Pi.add_apply]
  | neg x => simp only [map_neg, lift_apply_of, Pi.add_apply, neg_add]
  | add x y hx hy => simp only [(lift _).map_add, hx, hy, add_add_add_comm]
Cleared hypotheses: a