-- Module: Mathlib.Algebra.SkewMonoidAlgebra.Basic
Goal:
k : Type u_1
G : Type u_2
inst : Mul G
R : Type u_3
inst_1 : Semiring R
inst_2 : NonAssocSemiring k
inst_3 : SMul G k
g_hom : Type u_4
inst_4 : FunLike g_hom G R
inst_5 : MulHomClass g_hom G R
f : k →+* R
g : g_hom
a b : SkewMonoidAlgebra k G
h_comm :
  ∀ {x y : G},
    y ∈ a.support →
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R) =
        HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R)
y : G
hy : y ∈ a.support
x : G
_hx : x ∈ b.support
rw :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := R) ((f : (a : k) → R) (y • b.coeff x) : R)
        (HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((g : (a : G) → R) x : R))) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
rw₁ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (y • b.coeff x) : R) ((g : (a : G) → R) y : R))
        ((g : (a : G) → R) x : R)) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
rw₂ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (β := R) (HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((f : (a : k) → R) (b.coeff x) : R))
        ((g : (a : G) → R) x : R)) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
rw₃ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := R) ((g : (a : G) → R) y : R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R))) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)
rw₄ rw₅ :
  HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := R) ((g : (a : G) → R) y : R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R))) =
    HMul.hMul (α := R) ((f : (a : k) → R) (a.coeff y) : R)
      (HMul.hMul (α := R) ((g : (a : G) → R) y : R)
        (HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)))
⊢ HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((f : (a : k) → R) (y • b.coeff x) : R) *
      HMul.hMul (α := R) (β := R) ((g : (a : G) → R) y : R) ((g : (a : G) → R) x : R) =
    HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (a.coeff y) : R) ((g : (a : G) → R) y : R) *
      HMul.hMul (α := R) (β := R) ((f : (a : k) → R) (b.coeff x) : R) ((g : (a : G) → R) x : R)

Tactic:
rw [mul_assoc, ← mul_assoc (f (y • b.coeff x)), h_comm hy, mul_assoc, mul_assoc]

Premises used: mul_assoc, HSMul.hSMul, DFunLike.coe, SkewMonoidAlgebra.coeff