-- Lean 4 proof step from Mathlib.Algebra.FreeAbelianGroup.Finsupp (goal)
Goal:
X : Type u_1
x : X
H :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            toFinsupp :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₁ :
  Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp (N := X →₀ ℤ)
            ((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
              (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) :
                  (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
                (of x))
            ((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1) :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₂ :
  Eq (α := FreeAbelianGroup X)
    (((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
            (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x) :
          (a : X →₀ ℤ) → FreeAbelianGroup X)
        (((lift : (a : X → X →₀ ℤ) → FreeAbelianGroup X →+ X →₀ ℤ) fun (x : X) ↦ single x 1 :
            (a : FreeAbelianGroup X) → X →₀ ℤ)
          (of x)) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₃ :
  Eq (α := FreeAbelianGroup X)
    (((liftAddHom : (a : X → ℤ →+ FreeAbelianGroup X) → (X →₀ ℤ) →+ FreeAbelianGroup X) fun (x : X) ↦
            (AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x) :
          (a : X →₀ ℤ) → FreeAbelianGroup X)
        (single x 1) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₄ :
  Eq (α := FreeAbelianGroup X)
    ((((AddMonoidHom.flip (smulAddHom ℤ (FreeAbelianGroup X)) : (a : FreeAbelianGroup X) → ℤ →+ FreeAbelianGroup X)
              (of x) :
            ℤ →+ FreeAbelianGroup X) :
          (a : ℤ) → FreeAbelianGroup X)
        1 :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₅ :
  Eq (α := FreeAbelianGroup X)
    ((((smulAddHom ℤ (FreeAbelianGroup X) : (a : ℤ) → FreeAbelianGroup X →+ FreeAbelianGroup X) 1 :
            FreeAbelianGroup X →+ FreeAbelianGroup X) :
          (a : FreeAbelianGroup X) → FreeAbelianGroup X)
        (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
H₆ :
  HSMul.hSMul (α := ℤ) 1 (of x) =
    (AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x)
⊢ Eq (α := FreeAbelianGroup X)
    ((AddMonoidHom.comp toFreeAbelianGroup toFinsupp : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) :
      FreeAbelianGroup X)
    ((AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x) : FreeAbelianGroup X)
have H₇ : of x = (AddMonoidHom.id (FreeAbelianGroup X) : (a : FreeAbelianGroup X) → FreeAbelianGroup X) (of x)
Tactic: rw [toFreeAbelianGroup, toFinsupp, AddMonoidHom.comp_apply, lift_apply_of,
    liftAddHom_apply_single, AddMonoidHom.flip_apply, smulAddHom_apply, one_smul,
    AddMonoidHom.id_apply]