-- Module: Mathlib.GroupTheory.FreeAbelianGroup
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)
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)
⊢ (((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)

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]

Premises used: AddMonoidHom.map_zero, neg_add, map_neg, zero_add, Pi.add_apply, FreeAbelianGroup.lift, FreeAbelianGroup.of, add_add_add_comm, FreeAbelianGroup.lift_apply_of, AddMonoidHom.map_add, DFunLike.coe