-- 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)
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)
⊢ (((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 add : ∀ (x y : FreeAbelianGroup α)
  (hx :
    (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        x =
      HAdd.hAdd (α := G) (β := G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            x :
          G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            x :
          G))
  (hy :
    (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
          (a : FreeAbelianGroup α) → G)
        y =
      HAdd.hAdd (α := G) (β := G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            y :
          G)
        ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
              (a : FreeAbelianGroup α) → G)
            y :
          G)),
  (((lift : (a : α → G) → FreeAbelianGroup α →+ G) (f + g) : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
        (a : FreeAbelianGroup α) → G)
      (x + y) =
    HAdd.hAdd (α := G) (β := G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) f : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (x + y) :
        G)
      ((((lift : (a : α → G) → FreeAbelianGroup α →+ G) g : AddMonoidHom.{u, u_1} (FreeAbelianGroup α) G) :
            (a : FreeAbelianGroup α) → G)
          (x + y) :
        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