awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
inst_2 : Add A
⊢ ∀ (x y : Matrix m n A), Equiv.toFun uniqueEquiv (x + y) = Equiv.toFun uniqueEquiv x + Equiv.toFun uniqueEquiv y

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
inst_2 : Semiring R
inst_3 : AddCommMonoid A
inst_4 : Module R A
⊢ ∀ (m_1 : R) (x : Matrix m n A),
    Equiv.toFun (AddEquiv.toEquiv uniqueAddEquiv) (m_1 • x) =
      HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) m_1 : R) (Equiv.toFun (AddEquiv.toEquiv uniqueAddEquiv) x)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
inst_2 : NonUnitalNonAssocSemiring A
⊢ ∀ (x y : Matrix m m A),
    Equiv.toFun (AddEquiv.toEquiv uniqueAddEquiv) (x * y) =
      Equiv.toFun (AddEquiv.toEquiv uniqueAddEquiv) x * Equiv.toFun (AddEquiv.toEquiv uniqueAddEquiv) y

Tactic:
simp [mul_apply]

Premises used: Matrix.mul_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Unique
Goal:
m : Type u_1
n : Type u_2
A : Type u_3
R : Type u_4
inst : Unique m
inst_1 : Unique n
inst_2 : Semiring A
inst_3 : CommSemiring R
inst_4 : Algebra R A
r : R
⊢ Eq.{u_3 + 1} (α := A)
    (Equiv.toFun (α := Matrix m m A) (RingEquiv.toEquiv uniqueRingEquiv)
        ((algebraMap R (Matrix m m A) : (a : R) → Matrix m m A) r) :
      A)
    ((algebraMap R A : (a : R) → A) r : A)

Tactic:
aesop
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_1
R : Type u_3
f : m → n → R
⊢ vec ((of : (a : m → n → R) → Matrix m n R) f) = Function.uncurry (flip f)

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Matrix m n R
⊢ Aᵀ.vec = A.vec ∘ Prod.swap

Tactic:
rfl

Premises used: Matrix.vec, Matrix.transpose, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
A : Matrix m n R
⊢ A.vec = Function.uncurry fun (i : n) (j : m) ↦ A j i

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
simp_rw₃ : (∀ (a : n) (b : m), A.vec (a, b) = B.vec (a, b)) ↔ ∀ (b : n) (a : m), A a b = B a b
⊢ A.vec = B.vec ↔ A = B

Tactic:
simp_rw [← Matrix.ext_iff, funext_iff, Prod.forall, @forall_comm m n, vec]

Premises used: funext_iff, forall_comm, Matrix.vec, Prod.forall, Matrix.ext_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_3
n : Type u_2
R : Type u_1
⊢ Function.Bijective (α := Matrix m n R) vec

Tactic:
Equiv.curry _ _ _ |>.symm.bijective.comp Function.swap_bijective

Premises used: Equiv.bijective, Matrix, Matrix.vec, Function.swap_bijective, Equiv.curry, Function.Bijective.comp, Equiv.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
S : Type u_4
A : Matrix m n R
f : R → S
⊢ (A.map f).vec = f ∘ A.vec

Tactic:
rfl

Premises used: Matrix.vec, Matrix.map, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_3
n : Type u_2
R : Type u_1
inst : Zero R
⊢ Eq (α := n × m → R) (vec 0) 0

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Zero R
A : Matrix m n R
⊢ A.vec = 0 ↔ A = 0

Tactic:
vec_inj (B := 0)

Premises used: Matrix.vec_inj, Matrix.vec
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Add R
A B : Matrix m n R
⊢ (A + B).vec = A.vec + B.vec

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Neg R
A : Matrix m n R
⊢ (-A).vec = -A.vec

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Sub R
A B : Matrix m n R
⊢ (A - B).vec = A.vec - B.vec

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_3
n : Type u_4
R : Type u_2
α : Type u_1
inst : SMul α R
r : α
A : Matrix m n R
⊢ (r • A).vec = r • A.vec

Tactic:
rfl

Premises used: Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
h : ∀ (x : n × m), Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)
⊢ Eq (α := n × m → R) (vec (∑ i ∈ s, A i)) (∑ i ∈ s, (A i).vec)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
h₂ : Eq.{u_1 + 1} (α := R) ((∑ i ∈ s, A i) x.2 x.1) (∑ x_1 ∈ s, A x_1 x.2 x.1)
⊢ Eq.{u_1 + 1} (α := R) (vec (∑ i ∈ s, A i) x) ((∑ i ∈ s, (A i).vec) x)

Tactic:
simp_rw [vec, Finset.sum_apply, vec, Matrix.sum_apply]

Premises used: Matrix.sum_apply, Finset.sum_apply, Matrix.vec
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
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)
⊢ A.vec ⬝ᵥ B.vec = (Aᵀ * B).trace

Tactic:
simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, dotProduct, vec, transpose_apply,
    ← Finset.univ_product_univ, Finset.sum_product]

Premises used: Matrix.diag, dotProduct, Matrix.trace, Matrix.mul_apply, Finset.univ_product_univ, Matrix.vec, Matrix.transpose_apply, Finset.sum_product
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Star R
x : Matrix m n R
⊢ star x.vec = (x.map star).vec

Tactic:
rfl

Premises used: Matrix.vec, Matrix.map, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
simp_rw₂ : (Aᴴᵀᵀ * B).trace = (Aᴴ * B).trace
⊢ star A.vec ⬝ᵥ B.vec = (Aᴴ * B).trace

Tactic:
simp_rw [star_vec, vec_dotProduct_vec, ← conjTranspose_transpose, transpose_transpose]

Premises used: Matrix.transpose_transpose, Matrix.star_vec, Matrix.vec_dotProduct_vec, Matrix.conjTranspose_transpose
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_2
n : Type u_3
R : Type u_1
inst : Mul R
A B : Matrix m n R
⊢ (A ⊙ B).vec = A.vec * B.vec

Tactic:
rfl

Premises used: Matrix.hadamard, Matrix.vec, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
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)
⊢ (single i j r).vec = 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]

Premises used: Matrix.vec_of, Pi.uncurry_single_single, Matrix.single_eq_of_single_single, Function.uncurry_flip
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
⊢ 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:
Pi.single_comp_equiv (Equiv.prodComm _ _) _ _

Premises used: Pi.single_comp_equiv, Equiv.prodComm, Prod.swap
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
⊢ 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:
exact Pi.single_comp_equiv (Equiv.prodComm _ _) _ _

Premises used: Pi.single_comp_equiv, Equiv.prodComm
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : CommSemigroup R
A B : Matrix l m R
C D : Matrix n p R
⊢ Eq (α := Matrix (l × n) (m × p) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (A ⊙ B) (C ⊙ D))
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A C ⊙ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B D)

Tactic:
ext fun _ _ => mul_mul_mul_comm _ _ _ _

Premises used: mul_mul_mul_comm, Prod.fst, Prod.snd, Matrix.ext
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : CommSemigroup R
A : Matrix l m R
B : Matrix n p R
C : Matrix l m R
D : Matrix n p R
⊢ Eq (α := Matrix (l × n) (m × p) R)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B ⊙ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) C D)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) (A ⊙ C) (B ⊙ D))

Tactic:
hadamard_kronecker_hadamard _ _ _ _ |>.symm

Premises used: Matrix.hadamard_kronecker_hadamard, Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
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)
⊢ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec

Tactic:
ext ⟨k, l⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
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)
⊢ (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec) (k, l) = (A * X * Bᵀ).vec (k, l)

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]

Premises used: dotProduct, Matrix.mul_apply, Finset.univ_product_univ, Matrix.kroneckerMap_apply, Matrix.vec, Commute.right_comm, Matrix.transpose_apply, Finset.sum_product, Matrix.mulVec, Commute.eq, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
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)
⊢ X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A = (Aᵀ * X * B).vec

Tactic:
ext ⟨k, l⟩
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
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)

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]

Premises used: dotProduct, mul_assoc, Matrix.vecMul, Matrix.mul_apply, Finset.univ_product_univ, Matrix.kroneckerMap_apply, Matrix.vec, Commute.right_comm, Matrix.transpose_apply, Finset.sum_product, Commute.eq, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalCommSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix l m R
X : Matrix m n R
B : Matrix p n R
⊢ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A *ᵥ X.vec = (A * X * Bᵀ).vec

Tactic:
kronecker_mulVec_vec_of_commute _ _ _ fun _ _ _ => Commute.all _ _

Premises used: Commute.all, Matrix.kronecker_mulVec_vec_of_commute
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
l : Type u_2
m : Type u_1
n : Type u_4
p : Type u_5
R : Type u_3
inst : NonUnitalCommSemiring R
inst_1 : Fintype m
inst_2 : Fintype n
A : Matrix m l R
X : Matrix m n R
B : Matrix n p R
⊢ X.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B A = (Aᵀ * X * B).vec

Tactic:
vec_vecMul_kronecker_of_commute _ _ _ fun _ _ _ => Commute.all _ _

Premises used: Matrix.vec_vecMul_kronecker_of_commute, Commute.all
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
hB : ∀ (x : R) (i j : n), Commute x (1 i j)
⊢ (A * B).vec = kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) 1 A *ᵥ B.vec

Tactic:
rw [kronecker_mulVec_vec_of_commute, transpose_one, Matrix.mul_one]

Premises used: Matrix.transpose_one, Matrix.mul_one, Matrix.kronecker_mulVec_vec_of_commute
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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)
hB₁ : ∀ (hij : i ≠ j), Commute x (1 i j)
⊢ Commute x (1 i j)

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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 : n
⊢ Commute x (1 i i)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
hij : i ≠ j
⊢ Commute x (1 i j)

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
hA : ∀ (x : R) (i j : m), Commute (1 i j) x
⊢ (A * B).vec = A.vec ᵥ* kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) B 1

Tactic:
rw [vec_vecMul_kronecker_of_commute, transpose_one, Matrix.one_mul]

Premises used: Matrix.vec_vecMul_kronecker_of_commute, Matrix.transpose_one, Matrix.one_mul
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
hA₁ : ∀ (hij : i ≠ j), Commute (1 i j) x
⊢ Commute (1 i j) x

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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 : m
⊢ Commute (1 i i) x

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
hij : i ≠ j
⊢ Commute (1 i j) x

Tactic:
simp [*]
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
Goal:
m : Type u_1
n : Type u_2
R : Type u_3
inst : NonUnitalSemiring R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq n
inst_4 : Fintype n
x : m → R
A B : Matrix m n R
x' : n → R
⊢ x ⬝ᵥ A ⊙ B *ᵥ x' = (diagonal x).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec

Tactic:
simp [diagonal, mulVec, dotProduct, Fintype.sum_prod_type]

Premises used: dotProduct, Matrix.mulVec, Fintype.sum_prod_type, Matrix.diagonal
-- Module: Mathlib.LinearAlgebra.Matrix.Vec
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
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
rw₂ rw₃ :
  ((diagonal x).map star).vec ⬝ᵥ kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) A B *ᵥ (diagonal x').vec =
    ((diagonal x).map star).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

Tactic:
rw [dotProduct_hadamard_mulVec_eq_kronecker, ← map_diagonal_star, star_vec]

Premises used: Matrix.star_vec, Matrix.map_diagonal_star, Matrix.dotProduct_hadamard_mulVec_eq_kronecker
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Mul α
x y : WithConv (Matrix m n α)
⊢ x * y = toConv (x.ofConv ⊙ y.ofConv)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : Semigroup α
x x_1 x_2 : WithConv (Matrix m n α)
⊢ x * x_1 * x_2 = x * (x_1 * x_2)

Tactic:
simp [convMul_def, hadamard_assoc]

Premises used: Matrix.hadamard_assoc, convMul_def
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : NonUnitalNonAssocSemiring α
x x_1 x_2 : WithConv (Matrix m n α)
⊢ x * (x_1 + x_2) = x * x_1 + x * x_2

Tactic:
simp [hadamard_add]

Premises used: Matrix.hadamard_add
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : NonUnitalNonAssocSemiring α
x x_1 x_2 : WithConv (Matrix m n α)
⊢ (x + x_1) * x_2 = x * x_2 + x_1 * x_2

Tactic:
simp [add_hadamard]

Premises used: Matrix.add_hadamard
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : NonUnitalNonAssocSemiring α
⊢ ∀ (a : WithConv (Matrix m n α)), 0 * a = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : NonUnitalNonAssocSemiring α
⊢ ∀ (a : WithConv (Matrix m n α)), a * 0 = 0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : CommMagma α
⊢ ∀ (a b : WithConv (Matrix m n α)), a * b = b * a

Tactic:
simp [hadamard_comm]

Premises used: Matrix.hadamard_comm
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : One α
⊢ Eq (α := WithConv (Matrix m n α)) 1 (toConv ((of : (a : m → n → α) → Matrix m n α) 1))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : MulOneClass α
⊢ ∀ (a : WithConv (Matrix m n α)), 1 * a = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : MulOneClass α
⊢ ∀ (a : WithConv (Matrix m n α)), a * 1 = a

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
inst : Star α
x : WithConv (Matrix m n α)
⊢ star x = toConv (x.ofConv.map star)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : InvolutiveStar α
x : WithConv (Matrix m n α)
h : ∀ (i : m) (j : n), (star (star x)).ofConv i j = x.ofConv i j
⊢ star (star x) = x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Matrix.WithConv
Goal:
m : Type u_1
n : Type u_2
α : Type u_3
β : Type u_4
inst : InvolutiveStar α
x : WithConv (Matrix m n α)
i : m
j : n
⊢ (star (star x)).ofConv i j = x.ofConv i j

Tactic:
simp