awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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
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)
⊢ Commute z y

Tactic:
rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]

Premises used: Finset.mul_sum, Finsupp.sum, commute_iff_eq, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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)
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))
⊢ 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:
simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]

Premises used: smul_mul_assoc, And.left, mul_smul_comm, Commute.eq
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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)
⊢ ∀ (a : A), Commute z a

Tactic:
case comm =>
      intro y
      rw [← b.linearCombination_repr y, linearCombination_apply, sum, commute_iff_eq,
        Finset.sum_mul, Finset.mul_sum]
      simp_rw [mul_smul_comm, smul_mul_assoc, (h.1 _).eq]

Premises used: Finset.mul_sum, comm, Finsupp.sum, commute_iff_eq, smul_mul_assoc, Finsupp.linearCombination_apply, And.left, mul_smul_comm, Commute.eq, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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
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))
⊢ z * (c * d) = z * c * d

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]

Premises used: Finset.mul_sum, Finsupp.sum, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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 :
  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))))
⊢ 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:
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)]

Premises used: Finset.mul_sum, smul_mul_assoc, And.right, And.left, Finset.smul_sum, mul_smul_comm, SMulCommClass.smul_comm, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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
rw 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))))
⊢ 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:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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)
⊢ ∀ (b c : A), z * (b * c) = z * b * c

Tactic:
case left_assoc =>
      intro c d
      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]
      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)]
      rw [Finset.sum_comm]

Premises used: Finset.mul_sum, Finsupp.sum, smul_mul_assoc, Finsupp.linearCombination_apply, And.right, And.left, Finset.smul_sum, mul_smul_comm, SMulCommClass.smul_comm, Finset.sum_comm, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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
rw :
  (∑ 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)
⊢ c * d * z = c * (d * z)

Tactic:
rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]

Premises used: Finsupp.sum, Finsupp.linearCombination_apply, Module.Basis.linearCombination_repr, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
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)
case case₁ : ∀ (c d : A), c * d * z = c * (d * z)
case₂ :
  ∀ (c d : 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)
              ((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)
⊢ ∀ (a b : A), a * b * z = a * (b * z)

Tactic:
case right_assoc =>
      intro c d
      rw [← b.linearCombination_repr c, ← b.linearCombination_repr d, linearCombination_apply,
          linearCombination_apply, sum, Finsupp.sum, Finset.sum_mul]
      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]

Premises used: Finset.mul_sum, Finsupp.sum, smul_mul_assoc, Finsupp.linearCombination_apply, And.right, Finset.smul_sum, mul_smul_comm, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
i : ι
⊢ Eq.{u_5 + 1} (α := M) ((↑((restrictScalars R b : (a : ι) → ↥(span R (range (⇑b : (a : ι) → M)))) i) : M) : M)
    ((b : (a : ι) → M) i : M)

Tactic:
simp only [Basis.restrictScalars, Basis.span_apply]

Premises used: Module.Basis.span_apply, Module.Basis.restrictScalars
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i : ι
this :
  Eq (α := ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ S)
    (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
      (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R))
    (LinearMap.domRestrict
      ((↑R :
          {S : Type u_7} →
            {M : Type u_5} →
              {M₂ : Type (max u_1 u_7)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑b.repr : M →ₗ[S] ι →₀ S))
      (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
⊢ Eq.{u_7 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((((repr (restrictScalars R b) : (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ R) m : ι →₀ R) : (a : ι) → R)
            i :
          R) :
      S)
    ((((b.repr : (a : M) → ι →₀ S) (↑m : M) : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
DFunLike.congr_fun (LinearMap.congr_fun this m) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun
-- Module: Mathlib.LinearAlgebra.Basis.Submodule
Goal:
ι : Type u_1
R : Type u_3
M : Type u_5
S : Type u_7
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Ring S
inst_3 : Nontrivial S
inst_4 : AddCommGroup M
inst_5 : Algebra R S
inst_6 : Module S M
inst_7 : Module R M
inst_8 : IsScalarTower R S M
inst_9 : IsTorsionFree R S
b : Basis ι S M
m : ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M)))
i : ι
this :
  Eq (α := ↥(span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ S)
    (mapRange.linearMap (Algebra.linearMap R S) ∘ₗ
      (↑(repr (restrictScalars R b)) : ↥(span R (range (⇑b : (a : ι) → M))) →ₗ[R] ι →₀ R))
    (LinearMap.domRestrict
      ((↑R :
          {S : Type u_7} →
            {M : Type u_5} →
              {M₂ : Type (max u_1 u_7)} →
                [inst : Semiring R] →
                  [inst_10 : Semiring S] →
                    [inst_11 : AddCommMonoid M] →
                      [inst_12 : AddCommMonoid M₂] →
                        [inst_13 : Module R M] →
                          [inst_14 : Module R M₂] →
                            [inst_15 : Module S M] →
                              [inst_16 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        (↑b.repr : M →ₗ[S] ι →₀ S))
      (span R (range.{u_5, u_1 + 1} (ι := ι) (⇑b : (a : ι) → M))))
⊢ Eq.{u_7 + 1} (α := S)
    ((algebraMap R S : (a : R) → S)
        ((((repr (restrictScalars R b) : (a : ↥(span R (range (⇑b : (a : ι) → M)))) → ι →₀ R) m : ι →₀ R) : (a : ι) → R)
            i :
          R) :
      S)
    ((((b.repr : (a : M) → ι →₀ S) (↑m : M) : ι →₀ S) : (a : ι) → S) i : S)

Tactic:
exact DFunLike.congr_fun (LinearMap.congr_fun this m) i

Premises used: DFunLike.congr_fun, LinearMap.congr_fun