-- 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 : FreeAbelianGroup α
L2 : α
of :
  (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) : AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
        (a : FreeAbelianGroup α) → R)
      (0 * FreeAbelianGroup.of L2) =
    HMul.hMul (α := R) (β := R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          0 :
        R)
      ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L2) :
        R)
of₁ :
  ∀ (L1 : α),
    (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
            AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
          (a : FreeAbelianGroup α) → R)
        (FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (FreeAbelianGroup.of L1) :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (FreeAbelianGroup.of L2) :
          R)
of₂ :
  ∀ (L1 : α)
    (ih :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              (FreeAbelianGroup.of L1) :
            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)
        (-FreeAbelianGroup.of L1 * FreeAbelianGroup.of L2) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (-FreeAbelianGroup.of L1) :
          R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (FreeAbelianGroup.of L2) :
          R)
of₃ :
  ∀ (x1 x2 : FreeAbelianGroup α)
    (ih1 :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x1 * FreeAbelianGroup.of L2) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              x1 :
            R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              (FreeAbelianGroup.of L2) :
            R))
    (ih2 :
      (((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
              AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
            (a : FreeAbelianGroup α) → R)
          (x2 * FreeAbelianGroup.of L2) =
        HMul.hMul (α := R) (β := R)
          ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                  AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
                (a : FreeAbelianGroup α) → R)
              x2 :
            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)
        ((x1 + x2) * FreeAbelianGroup.of L2) =
      HMul.hMul (α := R) (β := R)
        ((((lift : (a : α → R) → FreeAbelianGroup α →+ R) (⇑f : (a : α) → R) :
                AddMonoidHom.{u, u_2} (FreeAbelianGroup α) R) :
              (a : FreeAbelianGroup α) → R)
            (x1 + x2) :
          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)

Tactic:
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]

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