awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A B : Matrix m n R
simp_rw : A.vec = B.vec ↔ ∀ (i : m) (j : n), A i j = B i j
simp_rw₁ : (∀ (x : n × m), A.vec x = B.vec x) ↔ ∀ (i : m) (j : n), A i j = B i j
simp_rw₂ : (∀ (a : n) (b : m), A.vec (a, b) = B.vec (a, b)) ↔ ∀ (i : m) (j : n), A i j = B i j
⊢ A.vec = B.vec ↔ A = B
have simp_rw₃ : (∀ (a : n) (b : m), A.vec (a, b) = B.vec (a, b)) ↔ ∀ (b : n) (a : m), A a b = B a b
Tactic: simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
⊢ Eq (α := n × m → R) (vec (∑ i ∈ s, A i)) (∑ i ∈ s, (A i).vec)
have h : ∀ (x : n × m), Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x : n × m
⊢ Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)
have h : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) ((∑ i ∈ s, (A i).vec) x)
Tactic: simp_rw [vec, Finset.sum_apply, vec, Matrix.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x : n × m
h : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) ((∑ i ∈ s, (A i).vec) x)
⊢ Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)
have h₁ : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) (∑ c ∈ s, (A c).vec x)
Tactic: simp_rw [vec, Finset.sum_apply, vec, Matrix.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
ι : Type u_2
m : Type u_3
n : Type u_4
R : Type u_1
inst : AddCommMonoid R
s : Finset ι
A : ι → Matrix m n R
x : n × m
h : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) ((∑ i ∈ s, (A i).vec) x)
h₁ : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) (∑ c ∈ s, (A c).vec x)
⊢ Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)
have h₂ : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) (∑ x_1 ∈ s, A x_1 x.2 x.1)
Tactic: simp_rw [vec, Finset.sum_apply, vec, Matrix.sum_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₂ : A.vec ⬝ᵥ B.vec = ∑ x : n, ∑ j : m, Aᵀ x j * B j x
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
simp_rw₂ : A.vec ⬝ᵥ B.vec = ∑ x : n, ∑ j : m, Aᵀ x j * B j x
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₃ : Eq.{u_1 + 1} (α := R) (∑ i : n × m, A.vec i * B.vec i) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
simp_rw₂ : A.vec ⬝ᵥ B.vec = ∑ x : n, ∑ j : m, Aᵀ x j * B j x
simp_rw₃ : Eq.{u_1 + 1} (α := R) (∑ i : n × m, A.vec i * B.vec i) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₄ : Eq.{u_1 + 1} (α := R) (∑ x : n × m, A x.2 x.1 * B x.2 x.1) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
simp_rw₂ : A.vec ⬝ᵥ B.vec = ∑ x : n, ∑ j : m, Aᵀ x j * B j x
simp_rw₃ : Eq.{u_1 + 1} (α := R) (∑ i : n × m, A.vec i * B.vec i) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
simp_rw₄ : Eq.{u_1 + 1} (α := R) (∑ x : n × m, A x.2 x.1 * B x.2 x.1) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₅ : Eq.{u_1 + 1} (α := R) (∑ x : n × m, A x.2 x.1 * B x.2 x.1) (∑ x : n, ∑ x_1 : m, A x_1 x * B x_1 x)
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Fintype m
inst_3 : Fintype n
A B : Matrix m n R
simp_rw : A.vec ⬝ᵥ B.vec = ∑ i : n, (Aᵀ * B).diag i
simp_rw₁ : A.vec ⬝ᵥ B.vec = ∑ x : n, (Aᵀ * B) x x
simp_rw₂ : A.vec ⬝ᵥ B.vec = ∑ x : n, ∑ j : m, Aᵀ x j * B j x
simp_rw₃ : Eq.{u_1 + 1} (α := R) (∑ i : n × m, A.vec i * B.vec i) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
simp_rw₄ : Eq.{u_1 + 1} (α := R) (∑ x : n × m, A x.2 x.1 * B x.2 x.1) (∑ x : n, ∑ j : m, Aᵀ x j * B j x)
simp_rw₅ : Eq.{u_1 + 1} (α := R) (∑ x : n × m, A x.2 x.1 * B x.2 x.1) (∑ x : n, ∑ x_1 : m, A x_1 x * B x_1 x)
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace
have simp_rw₆ : Eq.{u_1 + 1} (α := R) (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, A x.2 x.1 * B x.2 x.1)
  (∑ x : n, ∑ x_1 : m, A x_1 x * B x_1 x)
Tactic: simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Star R
inst_3 : Fintype m
inst_4 : Fintype n
A B : Matrix m n R
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace
have simp_rw : (A.map star).vec ⬝ᵥ B.vec = (Aᴴ * B).trace
Tactic: simp_rw [star_vec, vec_dotProduct_vec, ← conjTranspose_transpose, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Star R
inst_3 : Fintype m
inst_4 : Fintype n
A B : Matrix m n R
simp_rw : (A.map star).vec ⬝ᵥ B.vec = (Aᴴ * B).trace
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace
have simp_rw₁ : ((A.map star)ᵀ * B).trace = (Aᴴ * B).trace
Tactic: simp_rw [star_vec, vec_dotProduct_vec, ← conjTranspose_transpose, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : AddCommMonoid R
inst_1 : Mul R
inst_2 : Star R
inst_3 : Fintype m
inst_4 : Fintype n
A B : Matrix m n R
simp_rw : (A.map star).vec ⬝ᵥ B.vec = (Aᴴ * B).trace
simp_rw₁ : ((A.map star)ᵀ * B).trace = (Aᴴ * B).trace
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace
have simp_rw₂ : (Aᴴᵀᵀ * B).trace = (Aᴴ * B).trace
Tactic: simp_rw [star_vec, vec_dotProduct_vec, ← conjTranspose_transpose, transpose_transpose]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : DecidableEq m
inst_1 : DecidableEq n
inst_2 : Zero R
i : m
j : n
r : R
⊢ (single i j r).vec = Pi.single (M := fun (j : n × m) ↦ R) (j, i) r
have rw : Eq (α := n × m → R) (Pi.single (M := fun (j : m × n) ↦ R) (i, j) r ∘ Prod.swap)
  (Pi.single (M := fun (j : n × m) ↦ R) (j, i) r)
Tactic: rw [single_eq_of_single_single, vec_of, Function.uncurry_flip, Pi.uncurry_single_single]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
⊢ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec
have h : ∀ (k : p) (l_1 : l), (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l_1) = (A * X * Bᵀ).vec (k, l_1)
Tactic: ext ⟨k, l⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₂ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
  ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₃ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
  (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ i : m, A l i * X i x * Bᵀ x k)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ i : m, A l i * X i x * Bᵀ x k)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ i : m, A l i * X i x * Bᵀ x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₇ : Eq.{u_3 + 1} (α := R)
  (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, B k x.1 * A l x.2 * X.vec x)
  (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ i : m, A l i * X i x * Bᵀ x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, B k x.1 * A l x.2 * X.vec x)
    (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₈ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, B k x * A l x_1 * X.vec (x, x_1))
  (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l_1 m R
X : Matrix m n R
B : Matrix p n R
hB : ∀ (x : R) (i : p) (j : n), Commute x (B i j)
k : p
l : l_1
h : (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ) l k
h₁ : (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec = (A * X * Bᵀ) l k
h₂ :
  (fun (j : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) j) ⬝ᵥ X.vec =
    ∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A (k, l) x * X.vec x)
    (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, (∑ j : m, A l j * X j x) * Bᵀ x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ i : m, A l i * X i x * Bᵀ x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, B k x.1 * A l x.2 * X.vec x) (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, B k x.1 * A l x.2 * X.vec x)
    (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
h₈ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, B k x * A l x_1 * X.vec (x, x_1))
    (∑ x : n, ∑ x_1 : m, A l x_1 * X x_1 x * B k x)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)
have h₉ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, B k x * A l x_1 * X.vec (x, x_1))
  (∑ x : n, ∑ x_1 : m, A l x_1 * B k x * X x_1 x)
Tactic: simp_rw [vec, mulVec, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hB ..).right_comm, vec, (hB ..).eq]