internlm/Lean-Github huggingface dataset:
Theorem: MatrixCookbook.eq_495
Proof state before:
ι : Type ?u.5058
R : Type ?u.5061
l : Type ?u.5064
m : Type ?u.5067
n : Type u_1
p : Type ?u.5073
q : Type ?u.5076
r : Type ?u.5079
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix n n ℝ
⊢ exp ℝ (-A) = ∑' (n_1 : ℕ), (↑n_1 !)⁻¹ • (-1) ^ n_1 * A ^ n_1
Tactic:
simp_rw [exp_eq_tsum, neg_pow A, smul_mul_assoc]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_496
Proof state before:
ι : Type ?u.12418
R : Type ?u.12421
l : Type ?u.12424
m : Type ?u.12427
n : Type u_1
p : Type ?u.12433
q : Type ?u.12436
r : Type ?u.12439
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
t : ℝ
A : Matrix n n ℝ
⊢ exp ℝ (t • A) = ∑' (n_1 : ℕ), (↑n_1 !)⁻¹ • t ^ n_1 • A ^ n_1
Tactic:
simp_rw [exp_eq_tsum, smul_pow]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_507
Proof state before:
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
⊢ ¬∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
Tactic:
intro h
Proof state after:
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
⊢ False
Tactic:
obtain ⟨m1, m2, hm⟩ := exists_pair_ne m
Proof state after:
case intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
case intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
⊢ False
Tactic:
obtain ⟨n1⟩ := id ‹Nonempty n›
Proof state after:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
⊢ False
Tactic:
let A := stdBasisMatrix m1 n1 (1 : R)
Proof state after:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
⊢ False
Tactic:
let B := stdBasisMatrix m2 n1 (1 : R)
Proof state after:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
B : Matrix m n R := stdBasisMatrix m2 n1 1
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
B : Matrix m n R := stdBasisMatrix m2 n1 1
⊢ False
Tactic:
have := Matrix.ext_iff.mpr (h A B) (m1, m2) (n1, n1)
Proof state after:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
B : Matrix m n R := stdBasisMatrix m2 n1 1
this :
  kroneckerMap (fun x x_1 => x * x_1) A B (m1, m2) (n1, n1) = kroneckerMap (fun x x_1 => x * x_1) B A (m1, m2) (n1, n1)
⊢ False
Theorem: MatrixCookbook.eq_507
Proof state before:
case intro.intro.intro
ι : Type ?u.23645
R : Type u_3
l : Type ?u.23651
m : Type u_1
n : Type u_2
p : Type ?u.23660
q : Type ?u.23663
r : Type ?u.23666
inst✝¹⁴ : Fintype l
inst✝¹³ : Fintype m
inst✝¹² : Fintype n
inst✝¹¹ : Fintype p
inst✝¹⁰ : Fintype q
inst✝⁹ : Fintype r
inst✝⁸ : DecidableEq l
inst✝⁷ : DecidableEq m
inst✝⁶ : DecidableEq n
inst✝⁵ : DecidableEq p
inst✝⁴ : DecidableEq q
inst✝³ : DecidableEq r
inst✝² : Field R
inst✝¹ : Nontrivial m
inst✝ : Nonempty n
h : ∀ (A B : Matrix m n R), kroneckerMap (fun x x_1 => x * x_1) A B = kroneckerMap (fun x x_1 => x * x_1) B A
m1 m2 : m
hm : m1 ≠ m2
n1 : n
A : Matrix m n R := stdBasisMatrix m1 n1 1
B : Matrix m n R := stdBasisMatrix m2 n1 1
this :
  kroneckerMap (fun x x_1 => x * x_1) A B (m1, m2) (n1, n1) = kroneckerMap (fun x x_1 => x * x_1) B A (m1, m2) (n1, n1)
⊢ False
Tactic:
simp [StdBasisMatrix.apply_same, StdBasisMatrix.apply_of_row_ne hm,
  mul_zero, mul_one, one_ne_zero, A, B] at this
Proof state after:
no goals
Theorem: MatrixCookbook.eq_509
Proof state before:
ι : Type ?u.30122
R : Type u_3
l : Type ?u.30128
m : Type u_1
n : Type u_2
p : Type ?u.30137
q : Type u_5
r : Type u_4
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a b : R
A : Matrix m n R
B : Matrix r q R
⊢ kroneckerMap (fun x x_1 => x * x_1) (a • A) (b • B) = (a * b) • kroneckerMap (fun x x_1 => x * x_1) A B
Tactic:
rw [smul_kronecker, kronecker_smul, smul_smul]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_510
Proof state before:
ι : Type ?u.36304
R : Type u_3
l : Type ?u.36310
m : Type u_1
n : Type u_2
p : Type ?u.36319
q : Type u_5
r : Type u_4
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m n R
B : Matrix r q R
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B)ᵀ = kroneckerMap (fun x x_1 => x * x_1) Aᵀ Bᵀ
Tactic:
rw [kroneckerMap_transpose]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_511
Proof state before:
ι : Type ?u.36909
R : Type u_3
l : Type u_1
m : Type u_2
n : Type u_6
p : Type u_4
q : Type u_5
r : Type u_7
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l m R
B : Matrix p q R
C : Matrix m n R
D : Matrix q r R
⊢ kroneckerMap (fun x x_1 => x * x_1) A B * kroneckerMap (fun x x_1 => x * x_1) C D =
    kroneckerMap (fun x x_1 => x * x_1) (A * C) (B * D)
Tactic:
rw [Matrix.mul_kronecker_mul]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_515
Proof state before:
ι : Type ?u.43567
R : Type u_2
l : Type ?u.43573
m : Type u_1
n : Type u_3
p : Type ?u.43582
q : Type ?u.43585
r : Type ?u.43588
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix m m R
B : Matrix n n R
⊢ (kroneckerMap (fun x x_1 => x * x_1) A B).trace = A.trace * B.trace
Tactic:
simp_rw [Matrix.trace, Matrix.diag, Finset.sum_mul, Finset.mul_sum, ← Finset.univ_product_univ,
  Finset.sum_product, kronecker_apply]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_520
Proof state before:
ι : Type ?u.49154
R : Type u_3
l : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l m R
X : Matrix m n R
B : Matrix n p R
⊢ vec (A * X * B) = kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X
Tactic:
ext ⟨k, l⟩
Proof state after:
case a.mk
ι : Type ?u.49154
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix n p R
k : p
l : l✝
j✝ : Unit
⊢ vec (A * X * B) (k, l) j✝ = (kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X) (k, l) j✝
Theorem: MatrixCookbook.eq_520
Proof state before:
case a.mk
ι : Type ?u.49154
R : Type u_3
l✝ : Type u_1
m : Type u_2
n : Type u_4
p : Type u_5
q : Type ?u.49172
r : Type ?u.49175
inst✝¹² : Fintype l✝
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l✝
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A : Matrix l✝ m R
X : Matrix m n R
B : Matrix n p R
k : p
l : l✝
j✝ : Unit
⊢ vec (A * X * B) (k, l) j✝ = (kroneckerMap (fun x x_1 => x * x_1) Bᵀ A * vec X) (k, l) j✝
Tactic:
simp_rw [vec, Matrix.mul_apply, Matrix.kroneckerMap_apply, col_apply, Finset.sum_mul,
  transpose_apply, ← Finset.univ_product_univ, Finset.sum_product, mul_right_comm _ _ (B _ _),
  mul_comm _ (B _ _)]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_521
Proof state before:
ι : Type ?u.55165
R : Type u_3
l : Type ?u.55171
m : Type u_1
n : Type u_2
p : Type ?u.55180
q : Type ?u.55183
r : Type ?u.55186
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
A B : Matrix m n R
⊢ (Aᵀ * B).trace = ((vec A)ᵀ * vec B) () ()
Tactic:
simp_rw [Matrix.trace, Matrix.diag, Matrix.mul_apply, vec, transpose_apply, col_apply, ←
  Finset.univ_product_univ, Finset.sum_product]
Proof state after:
no goals
Theorem: MatrixCookbook.eq_524
Proof state before:
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
⊢ row a * X * B * Xᵀ * col c = (vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X
Tactic:
ext ⟨i, j⟩
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ (row a * X * B * Xᵀ * col c) PUnit.unit j✝ =
    ((vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X) PUnit.unit j✝
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ (row a * X * B * Xᵀ * col c) PUnit.unit j✝ =
    ((vec X)ᵀ * kroneckerMap (fun x x_1 => x * x_1) Bᵀ (col c * row a) * vec X) PUnit.unit j✝
Tactic:
simp only [vec, Matrix.mul_apply, Finset.sum_mul, Finset.mul_sum, Matrix.kroneckerMap_apply,
  transpose_apply, Matrix.row_apply, Matrix.col_apply, Fintype.sum_unique]
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : m, ∑ x_1 : n, ∑ x_2 : n, ∑ i : m, a i * X i x_2 * B x_2 x_1 * X x x_1 * c x =
    ∑ x : n × m, ∑ i : n × m, X i.2 i.1 * (B x.1 i.1 * (c i.2 * a x.2)) * X x.2 x.1
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : m, ∑ x_1 : n, ∑ x_2 : n, ∑ i : m, a i * X i x_2 * B x_2 x_1 * X x x_1 * c x =
    ∑ x : n × m, ∑ i : n × m, X i.2 i.1 * (B x.1 i.1 * (c i.2 * a x.2)) * X x.2 x.1
Tactic:
simp_rw [← Finset.univ_product_univ, Finset.sum_product, @Finset.sum_comm n _ m]
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Tactic:
rw [Finset.sum_comm]
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ y : n, ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Theorem: MatrixCookbook.eq_524
Proof state before:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
⊢ ∑ y : n, ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i y * B y x * X x_1 x * c x_1 =
    ∑ x : n, ∑ y : n, ∑ x_1 : m, ∑ x_2 : m, X x_2 y * (B x y * (c x_2 * a x_1)) * X x_1 x
Tactic:
refine' Finset.sum_congr rfl fun k _ => _
Proof state after:
case a.unit
ι : Type ?u.61791
R : Type u_3
l : Type ?u.61797
m : Type u_1
n : Type u_2
p : Type ?u.61806
q : Type ?u.61809
r : Type ?u.61812
inst✝¹² : Fintype l
inst✝¹¹ : Fintype m
inst✝¹⁰ : Fintype n
inst✝⁹ : Fintype p
inst✝⁸ : Fintype q
inst✝⁷ : Fintype r
inst✝⁶ : DecidableEq l
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : DecidableEq p
inst✝² : DecidableEq q
inst✝¹ : DecidableEq r
inst✝ : Field R
a : m → R
X : Matrix m n R
B : Matrix n n R
c : m → R
j✝ : Unit
k : n
x✝ : k ∈ Finset.univ
⊢ ∑ x : n, ∑ x_1 : m, ∑ i : m, a i * X i k * B k x * X x_1 x * c x_1 =
    ∑ y : n, ∑ x : m, ∑ x_1 : m, X x_1 y * (B k y * (c x_1 * a x)) * X x k