awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Basis.Submodule (goal)
Goal:
ι : Type u_1
ι' : Type u_2
R : Type u_3
R₂ : Type u_4
M : Type u_5
M' : Type u_6
inst : Ring R
inst_1 : IsDomain R
inst_2 : AddCommGroup M
inst_3 : Module R M
b_1 : ι → M
b : Basis ι R M
P : Submodule R M → Sort u_7
ih :
  (N : Submodule R M) →
    ((N' : Submodule R M) → N' ≤ N → (x : M) → x ∈ N → (∀ (c : R), ∀ y ∈ N', c • x + y = 0 → c = 0) → P N') → P N
n : ℕ
N : Submodule R M
rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n
this : DecidableEq M
Pbot : P ⊥
zero :
  (N : Submodule R M) →
    (rank_le : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ 0) →
      P N
⊢ P N
have succ : (n : ℕ) →
  (rank_ih :
      (N : Submodule R M) →
        (rank_le :
            ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n) →
          P N) →
    (N : Submodule R M) →
      (rank_le :
          ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val (p := fun (x : M) ↦ x ∈ N) ∘ v) → m ≤ n + 1) →
        P N
Tactic: induction n generalizing N with
  | zero =>
    suffices N = ⊥ by rwa [this]
    apply Basis.eq_bot_of_rank_eq_zero b _ fun m hv => Nat.le_zero.mp (rank_le _ hv)
  | succ n rank_ih =>
    apply ih
    intro N' N'_le x x_mem x_ortho
    apply rank_ih
    intro m v hli
    refine Nat.succ_le_succ_iff.mp (rank_le (Fin.cons ⟨x, x_mem⟩ fun i => ⟨v i, N'_le (v i).2⟩) ?_)
    convert! hli.finCons' x _ ?_
    · ext i
      refine Fin.cases ?_ ?_ i <;> simp
    · intro c y hy hc
      refine x_ortho c y (Submodule.span_le.mpr ?_ hy) hc
      rintro _ ⟨z, rfl⟩
      exact (v z).2
Cleared hypotheses: n, N, rank_le
-- 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
⊢ z ∈ center A ↔
    (∀ (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)
have mp : z ∈ center A →
  (∀ (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)
Tactic: constructor
-- 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
mp :
  z ∈ center A →
    (∀ (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)
⊢ z ∈ center A ↔
    (∀ (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)
have mpr : ((∀ (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)) →
  z ∈ center A
Tactic: constructor
-- 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 : z ∈ center A
⊢ (∀ (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)
have mp : ∀ (i : ι), Commute ((b : (a : ι) → A) i) z
Tactic: constructor
-- 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 : z ∈ center A
mp : ∀ (i : ι), Commute ((b : (a : ι) → A) i) z
⊢ (∀ (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)
have mp₁ : ∀ (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)
Tactic: constructor
-- 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)
⊢ IsMulCentral z
have constructor : ∀ (a : A), Commute z a
Tactic: constructor
-- 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)
constructor : ∀ (a : A), Commute z a
⊢ IsMulCentral z
have constructor₁ : ∀ (b c : A), z * (b * c) = z * b * c
Tactic: constructor
-- 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)
constructor : ∀ (a : A), Commute z a
constructor₁ : ∀ (b c : A), z * (b * c) = z * b * c
⊢ IsMulCentral z
have constructor₂ : ∀ (a b : A), a * b * z = a * (b * z)
Tactic: constructor
-- 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)
y : A
⊢ Commute z y
have rw : Eq.{u_7 + 1} (α := A)
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    z *
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
        ((b : (a : ι) → A) i : A))
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
        ((b : (a : ι) → A) i : A) *
      z)
Tactic: rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]
-- 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)
y : A
⊢ Eq.{u_7 + 1} (α := A)
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      z *
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A))
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A) *
        z)
have simp_rw : Eq.{u_7 + 1} (α := A)
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
      (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)))
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
        ((b : (a : ι) → A) i : A) *
      z)
Tactic: simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]
-- 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)
y : A
simp_rw :
  Eq.{u_7 + 1} (α := A)
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
        (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)))
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A) *
        z)
⊢ Eq.{u_7 + 1} (α := A)
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      z *
        HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A))
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
      HSMul.hSMul.{u_3, u_7, u_7} (α := R) (β := A) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) i : R)
          ((b : (a : ι) → A) i : A) *
        z)
have simp_rw₁ : Eq.{u_7 + 1} (α := A)
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
      (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)))
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) y),
    HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) y : ι →₀ R) : (a : ι) → R) x : R)
      (HMul.hMul (α := A) ((b : (a : ι) → A) x : A) z))
Tactic: simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]
-- 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
⊢ z * (c * d) = z * c * d
have rw : Eq.{u_7 + 1} (α := A)
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
    z *
      (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)))
  (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
        z *
          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)) *
      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))
Tactic: rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, sum, Finset.sum_mul, Finset.mul_sum, Finset.mul_sum,
          Finset.mul_sum]
-- 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
⊢ Eq.{u_7 + 1} (α := A)
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
      z *
        (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)))
    (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
      (∑ i ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) c),
          z *
            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)) *
        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))
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) (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)) ((b : (a : ι) → A) x_1 : A))))
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
    ∑ x_1 ∈ 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_1 : R)
        (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x : R)
          (HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) x_1 : A)) ((b : (a : ι) → A) x : A))))
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, (h.2 _ _).1,
        (@SMulCommClass.smul_comm R R A)]
-- 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
⊢ 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) (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)) ((b : (a : ι) → A) x_1 : A))))
    (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
      ∑ x_1 ∈ 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_1 : R)
          (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x : R)
            (HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) x_1 : A)) ((b : (a : ι) → A) x : A))))
have rw : Eq.{u_7 + 1} (α := A)
  (∑ y ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
    ∑ 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)
        (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) y : R)
          (HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) x : A)) ((b : (a : ι) → A) y : A))))
  (∑ x ∈ Finsupp.support.{u_1, u_3} (M := R) ((b.repr : (a : A) → ι →₀ R) d),
    ∑ x_1 ∈ 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_1 : R)
        (HSMul.hSMul.{u_3, u_7, u_7} (α := R) ((((b.repr : (a : A) → ι →₀ R) d : ι →₀ R) : (a : ι) → R) x : R)
          (HMul.hMul (β := A) (HMul.hMul (β := A) z ((b : (a : ι) → A) x_1 : A)) ((b : (a : ι) → A) x : A))))
Tactic: rw [Finset.sum_comm]