-- 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)
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)
simp_rw₂ :
  Eq.{u_7 + 1} (α := A)
    (∑ 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)
          (∑ i_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HMul.hMul (α := A) ((b : (a : ι) → A) i : A)
              (HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A)
                ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) i_1 : R) ((b : (a : ι) → A) i_1 : 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) *
        ∑ i ∈ 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) i : R)
              ((b : (a : ι) → A) i : A) *
            z)
simp_rw₃ :
  Eq.{u_7 + 1} (α := A)
    (∑ 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)
          (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : 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) *
        ∑ i ∈ 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) i : R)
              ((b : (a : ι) → A) i : A) *
            z)
simp_rw₄ :
  Eq.{u_7 + 1} (α := A)
    (∑ 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)
          (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
            HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : A))) *
        z)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ i ∈ 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) c : ι →₀ R) : (a : ι) → R) x : R)
            ((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))
simp_rw₅ :
  Eq.{u_7 + 1} (α := A)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : A)))) *
        z)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ i ∈ 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) c : ι →₀ R) : (a : ι) → R) x : R)
            ((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))
simp_rw₆ :
  Eq.{u_7 + 1} (α := A)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : A)))) *
        z)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
          (HMul.hMul (α := A) ((b : (a : ι) → A) x : A)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) ((b : (a : ι) → A) x_1 : A) z))))
simp_rw₇ :
  Eq.{u_7 + 1} (α := A)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      (∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
          HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : A)))) *
        z)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
          (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
            (HMul.hMul (α := A) ((b : (a : ι) → A) x : A) (HMul.hMul (α := A) ((b : (a : ι) → A) x_1 : A) z))))
simp_rw₈ :
  Eq.{u_7 + 1} (α := A)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
            (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) i : R)
              (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) i : A))) *
          z)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      ∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
          (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
            (HMul.hMul (α := A) ((b : (a : ι) → A) x : A) (HMul.hMul (α := A) ((b : (a : ι) → A) x_1 : 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₉ : Eq.{u_7 + 1} (α := A)
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
    ∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
        (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HMul.hMul (α := A) (β := A) ((b : (a : ι) → A) x : A) ((b : (a : ι) → A) x_1 : A) * z)))
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
    ∑ x_1 ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) c : ι →₀ R) : (a : ι) → R) x : R)
        (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x_1 : R)
          (HMul.hMul (α := A) ((b : (a : ι) → A) x : A) (HMul.hMul (α := A) ((b : (a : ι) → A) x_1 : 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]