-- Module: Mathlib.GroupTheory.FreeAbelianGroup
Goal:
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst : Monoid α
inst_1 : Ring R
f : α →* R
x y : FreeAbelianGroup α
zero :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * 0) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          0 :
        R)
of :
  ∀ (L2 : α),
    (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (x * FreeAbelianGroup.of L2) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            x :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (FreeAbelianGroup.of L2) :
          R)
neg :
  ∀ (L2 : α)
    (ih :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x * FreeAbelianGroup.of L2) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              x :
            R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              (FreeAbelianGroup.of L2) :
            R)),
    (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (x * -FreeAbelianGroup.of L2) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            x :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (-FreeAbelianGroup.of L2) :
          R)
add :
  ∀ (y1 y2 : FreeAbelianGroup α)
    (ih1 :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x * y1) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              x :
            R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              y1 :
            R))
    (ih2 :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x * y2) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              x :
            R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              y2 :
            R)),
    (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (x * (y1 + y2)) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            x :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (y1 + y2) :
          R)
⊢ (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (x * y) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          x :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          y :
        R)

Tactic:
induction y using FreeAbelianGroup.induction_on with
      | zero => simp only [mul_zero, map_zero]
      | of L2 =>
        induction x using FreeAbelianGroup.induction_on with
        | zero => simp only [zero_mul, map_zero]
        | of L1 =>
          simp_rw [of_mul_of, lift_apply_of]
          exact f.map_mul _ _
        | neg L1 ih =>
          simp_rw [neg_mul, map_neg, neg_mul]
          exact congr_arg Neg.neg ih
        | add x1 x2 ih1 ih2 => simp only [add_mul, map_add, ih1, ih2]
      | neg L2 ih => rw [mul_neg, map_neg, map_neg, mul_neg, ih]
      | add y1 y2 ih1 ih2 => rw [mul_add, map_add, map_add, mul_add, ih1, ih2]

Premises used: add_mul, MulZeroClass.zero_mul, map_zero, FreeAbelianGroup.of_mul_of, map_add, map_neg, MulZeroClass.mul_zero, FreeAbelianGroup.of, mul_add, neg_mul, FreeAbelianGroup.lift_apply_of, MonoidHom.map_mul, mul_neg