Theorem: MatrixCookbook.eq_507 (MatrixCookbook/10FunctionsAndOperators.lean)

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
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

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
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

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›
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

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)
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

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)
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

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)
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

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
State after:
no goals