-- Lean 4 proof step from Mathlib.GroupTheory.FreeAbelianGroup (goal)
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)
⊢ (((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)
have 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)
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]
Cleared hypotheses: x