-- Lean 4 proof step from Mathlib.Algebra.SkewMonoidAlgebra.Basic (goal)
Goal:
k : Type u_1
G : Type u_2
inst : Semiring k
inst_1 : Monoid G
inst_2 : MulSemiringAction G k
f g : SkewMonoidAlgebra k G →+* k
h₁ :
  ∀ (b : k),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
h_of :
  ∀ (a : G),
    Eq.{u_1 + 1} (α := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
this : ∀ {a : G} {b₁ b₂ : k}, HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b₁) (single a b₂) = single a (b₁ * b₂)
a : G
b : k
rw :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a (b * 1)) :
      k)
rw₁ :
  Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
rw₂ :
  Eq.{u_1 + 1} (α := k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) :
      k)
rw₃ :
  Eq.{u_1 + 1} (α := k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
    ((g : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1)) : k)
rw₄ :
  HMul.hMul (α := k) (β := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k) =
    (g : (a : SkewMonoidAlgebra k G) → k) (HMul.hMul (α := SkewMonoidAlgebra k G) (single 1 b) (single a 1))
rw₅ :
  HMul.hMul (α := k) (β := k) ((f : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k) =
    HMul.hMul (α := k) (β := k) ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
      ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
⊢ Eq.{u_1 + 1} (α := k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) f :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
    (((fun (f : SkewMonoidAlgebra k G →+* k) ↦ ((↑f : SkewMonoidAlgebra k G →+ k) : SkewMonoidAlgebra k G →+ k)) g :
          (a : SkewMonoidAlgebra k G) → k)
        (single a b) :
      k)
have rw₆ : HMul.hMul (α := k) (β := k) ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
    ((f : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k) =
  HMul.hMul (α := k) (β := k) ((g : (a : SkewMonoidAlgebra k G) → k) (single 1 b) : k)
    ((g : (a : SkewMonoidAlgebra k G) → k) (single a 1) : k)
Tactic: rw [← mul_one b, ← this, AddMonoidHom.coe_coe f,
      AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]