-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
Goal:
ι : Type u_1
R : Type u_3
A : Type u_7
inst : Semiring R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : Module R A
inst_3 : SMulCommClass R A A
inst_4 : SMulCommClass R R A
inst_5 : IsScalarTower R A A
b : Basis ι R A
z : A
h :
  (∀ (i : ι), Commute ((b : (a : ι) → A) i) z) ∧
    ∀ (i j : ι),
      z * HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) =
          HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) i : A)) ((b : (a : ι) → A) j : A) ∧
        HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) i : A) ((b : (a : ι) → A) j : A) * z =
          HMul.hMul (α := A) ((b : (a : ι) → A) i : A) (HMul.hMul (α := A) ((b : (a : ι) → A) j : A) z)
c d : A
simp_rw :
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
          (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A)
            (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
                HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
                  ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → A) a : A) :
              A))) *
      z =
    (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
            ((b : (a : ι) → A) a : A)) *
        z)
⊢ (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) i : R)
            ((b : (a : ι) → A) i : A) *
          ∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
              ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R) ((b : (a : ι) → A) a : A)) *
      z =
    (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
            ((b : (a : ι) → A) a : A)) *
        z)
have simp_rw₁ : (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
        (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HMul.hMul (α := A) ((b : (a : ι) → A) x : A)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
              ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) i : R) ((b : (a : ι) → A) i : A)))) *
    z =
  (∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) a : R)
        ((b : (a : ι) → A) a : A)) *
    ((∑ a ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) a : R)
          ((b : (a : ι) → A) a : A)) *
      z)
Tactic: simp_rw [smul_mul_assoc, Finset.mul_sum, Finset.sum_mul, mul_smul_comm, Finset.mul_sum,
               Finset.smul_sum, smul_mul_assoc, mul_smul_comm, Finset.sum_mul, smul_mul_assoc,
               (h.2 _ _).2]