awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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)
⊢ (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 x_1 x) (∑ 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l : Type u_2
m : Type u_1
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 m l R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l), Commute (A i j) x
⊢ X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A = (Aᵀ * X * B).vec
have h : ∀ (k : p) (l_1 : l), (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (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_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₂ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
  ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₃ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
  (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (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, X.vec x * (B x.1 k * A x.2 l))
  (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, X.vec x * (B x.1 k * A x.2 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₈ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
  (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, X.vec x * (B x.1 k * A x.2 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₈ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₉ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
  (∑ x : n, ∑ x_1 : m, X x_1 x * A x_1 l * B x k)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, X.vec x * (B x.1 k * A x.2 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₈ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₉ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, X x_1 x * A x_1 l * B x k)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₁₀ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
  (∑ x : n, ∑ x_1 : m, X x_1 x * B x k * A x_1 l)
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l_1 : Type u_2
m : Type u_1
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 m l_1 R
X : Matrix m n R
B : Matrix n p R
hA : ∀ (x : R) (i : m) (j : l_1), Commute (A i j) x
k : p
l : l_1
h : (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B) l k
h₁ : (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) = (Aᵀ * X * B) l k
h₂ :
  (X.vec ⬝ᵥ fun (i : n × m) ↦ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A i (k, l)) =
    ∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k
h₃ :
  Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A x (k, l))
    (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₄ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, (∑ j : m, Aᵀ l j * X j x) * B x k)
h₅ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ i : m, Aᵀ l i * X i x * B x k)
h₆ : Eq.{u_3 + 1} (α := R) (∑ x : n × m, X.vec x * (B x.1 k * A x.2 l)) (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₇ :
  Eq.{u_3 + 1} (α := R)
    (∑ x ∈ SProd.sprod (α := Finset n) (β := Finset m) Finset.univ Finset.univ, X.vec x * (B x.1 k * A x.2 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₈ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, A x_1 l * X x_1 x * B x k)
h₉ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, X x_1 x * A x_1 l * B x k)
h₁₀ :
  Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
    (∑ x : n, ∑ x_1 : m, X x_1 x * B x k * A x_1 l)
⊢ (X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A) (k, l) = (Aᵀ * X * B).vec (k, l)
have h₁₁ : Eq.{u_3 + 1} (α := R) (∑ x : n, ∑ x_1 : m, X.vec (x, x_1) * (B x k * A x_1 l))
  (∑ x : n, ∑ x_1 : m, X x_1 x * (B x k * A x_1 l))
Tactic: simp_rw [vec, vecMul, mul_apply, dotProduct, kroneckerMap_apply, Finset.sum_mul, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product, (hA ..).eq, (hA ..).right_comm, mul_assoc, vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix l m R
B : Matrix m n R
⊢ (A * B).vec = kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) 1 A *ᵥ B.vec
have hB : ∀ (x : R) (i j : n), Commute x (1 i j)
Tactic: rw [kronecker_mulVec_vec_of_commute, transpose_one, Matrix.mul_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix l m R
B : Matrix m n R
x : R
i j : n
⊢ Commute x (1 i j)
have hB : Commute x (1 i i)
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
l : Type u_2
m : Type u_3
n : Type u_1
R : Type u_4
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq n
A : Matrix l m R
B : Matrix m n R
x : R
i j : n
hB : Commute x (1 i i)
⊢ Commute x (1 i j)
have hB₁ : ∀ (hij : i ≠ j), Commute x (1 i j)
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
A : Matrix m n R
B : Matrix n p R
⊢ (A * B).vec = A.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B 1
have hA : ∀ (x : R) (i j : m), Commute (1 i j) x
Tactic: rw [vec_vecMul_kronecker_of_commute, transpose_one, Matrix.one_mul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
A : Matrix m n R
B : Matrix n p R
x : R
i j : m
⊢ Commute (1 i j) x
have hA : Commute (1 i i) x
Tactic: obtain rfl | hij := eq_or_ne i j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_1
n : Type u_2
p : Type u_4
R : Type u_3
inst : Semiring R
inst_1 : Fintype m
inst_2 : Fintype n
inst_3 : DecidableEq m
A : Matrix m n R
B : Matrix n p R
x : R
i j : m
hA : Commute (1 i i) x
⊢ Commute (1 i j) x
have hA₁ : ∀ (hij : i ≠ j), Commute (1 i j) x
Tactic: obtain rfl | hij := eq_or_ne i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : StarAddMonoid R
x : m → R
A B : Matrix m n R
x' : n → R
⊢ star x ⬝ᵥ A ⊙ B *ᵥ x' = star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
have rw : (diagonal (star x)).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
  star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
Tactic: rw [dotProduct_hadamard_mulVec_eq_kronecker, ← map_diagonal_star, star_vec]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Vec (goal)
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : NonUnitalSemiring R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
inst_5 : StarAddMonoid R
x : m → R
A B : Matrix m n R
x' : n → R
rw :
  (diagonal (star x)).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
    star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
⊢ star x ⬝ᵥ A ⊙ B *ᵥ x' = star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
have rw₁ : ((diagonal x).map star).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
  star (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec
Tactic: rw [dotProduct_hadamard_mulVec_eq_kronecker, ← map_diagonal_star, star_vec]