[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ b • stdBasisMatrix i j a = stdBasisMatrix i j (b • a)
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ (b • fun i' j' => if i = i' ∧ j = j' then a else 0) = fun i' j' => if i = i' ∧ j = j' then b • a else 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
⊢ (b • fun i' j' => if i = i' ∧ j = j' then a else 0) i✝ x✝ = if i = i✝ ∧ j = x✝ then b • a else 0
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 0 = 0
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ (fun i' j' => if i = i' ∧ j = j' then 0 else 0) = 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then 0 else 0) = OfNat.ofNat 0 i✝ x✝
[PROOFSTEP]
simp
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ stdBasisMatrix i j (a + b) = stdBasisMatrix i j a + stdBasisMatrix i j b
[PROOFSTEP]
unfold stdBasisMatrix
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
⊢ (fun i' j' => if i = i' ∧ j = j' then a + b else 0) =
    (fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0
[PROOFSTEP]
ext
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
⊢ (if i = i✝ ∧ j = x✝ then a + b else 0) =
    ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
h : i = i✝ ∧ j = x✝
⊢ a + b = ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
simp [h]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
a b : α
i✝ : m
x✝ : n
h : ¬(i = i✝ ∧ j = x✝)
⊢ 0 = ((fun i' j' => if i = i' ∧ j = j' then a else 0) + fun i' j' => if i = i' ∧ j = j' then b else 0) i✝ x✝
[PROOFSTEP]
simp [h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
⊢ x = ∑ i : m, ∑ j : n, stdBasisMatrix i j (x i j)
[PROOFSTEP]
ext i j
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ x i j = Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j
[PROOFSTEP]
symm
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
iterate 2
  rw [Finset.sum_apply]
    -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun i => ∑ j : n, stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
rw [Finset.sum_apply]
  -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun c => Finset.sum Finset.univ (fun j => stdBasisMatrix c j (x c j)) i) j = x i j
[PROOFSTEP]
rw [Finset.sum_apply]
  -- Porting note: was `convert`
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∑ c : m, Finset.sum Finset.univ (fun j => stdBasisMatrix c j (x c j)) i j = x i j
[PROOFSTEP]
refine (Fintype.sum_eq_single i ?_).trans ?_
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∀ (x_1 : m), x_1 ≠ i → Finset.sum Finset.univ (fun j => stdBasisMatrix x_1 j (x x_1 j)) i j = 0
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
swap
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix i j (x i j)) i j = x i j
[PROOFSTEP]
simp only [stdBasisMatrix]
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ Finset.sum Finset.univ (fun x_1 i' j' => if i = i' ∧ x_1 = j' then x i x_1 else 0) i j = x i j
[PROOFSTEP]
rw [Fintype.sum_apply, Fintype.sum_apply]
[GOAL]
case a.h.refine_2
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ (∑ c : n, if i = i ∧ c = j then x i c else 0) = x i j
[PROOFSTEP]
simp
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
⊢ ∀ (x_1 : m), x_1 ≠ i → Finset.sum Finset.univ (fun j => stdBasisMatrix x_1 j (x x_1 j)) i j = 0
[PROOFSTEP]
intro j' hj'
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ Finset.sum Finset.univ (fun j => stdBasisMatrix j' j (x j' j)) i j = 0
[PROOFSTEP]
simp only [stdBasisMatrix]
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ Finset.sum Finset.univ (fun x_1 i' j'_1 => if j' = i' ∧ x_1 = j'_1 then x j' x_1 else 0) i j = 0
[PROOFSTEP]
rw [Fintype.sum_apply, Fintype.sum_apply]
[GOAL]
case a.h.refine_1
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
x : Matrix m n α
i : m
j : n
j' : m
hj' : j' ≠ i
⊢ (∑ c : n, if j' = i ∧ c = j then x j' c else 0) = 0
[PROOFSTEP]
simp [hj']
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
⊢ stdBasisMatrix i j 1 = vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0
[PROOFSTEP]
ext i' j'
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (fun i' => if i = i' then 1 else 0) (fun j' => if j = j' then 1 else 0) i' j'
[PROOFSTEP]
simp only [stdBasisMatrix, vecMulVec, mul_ite, mul_one, mul_zero, of_apply]
  -- Porting note: added next line
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if i = i' ∧ j = j' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
[PROOFSTEP]
simp_rw [@and_comm (i = i')]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
i' : m
j' : n
⊢ (if j = j' ∧ i = i' then 1 else 0) = if j = j' then if i = i' then 1 else 0 else 0
[PROOFSTEP]
exact ite_and _ _ _ _
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P M
[PROOFSTEP]
rw [matrix_eq_sum_std_basis M, ← Finset.sum_product']
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P (∑ x in Finset.univ ×ˢ Finset.univ, stdBasisMatrix x.fst x.snd (M x.fst x.snd))
[PROOFSTEP]
apply Finset.sum_induction _ _ h_add h_zero
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ ∀ (x : m × n), x ∈ Finset.univ ×ˢ Finset.univ → P (stdBasisMatrix x.fst x.snd (M x.fst x.snd))
[PROOFSTEP]
intros
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁵ : DecidableEq l
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : Semiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
x✝ : m × n
a✝ : x✝ ∈ Finset.univ ×ˢ Finset.univ
⊢ P (stdBasisMatrix x✝.fst x✝.snd (M x✝.fst x✝.snd))
[PROOFSTEP]
apply h_std_basis
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
⊢ P 0
[PROOFSTEP]
inhabit m
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h : Inhabited m
⊢ P 0
[PROOFSTEP]
inhabit n
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁷ : DecidableEq l
inst✝⁶ : DecidableEq m
inst✝⁵ : DecidableEq n
inst✝⁴ : Semiring α
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : Nonempty m
inst✝ : Nonempty n
P : Matrix m n α → Prop
M : Matrix m n α
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (stdBasisMatrix i j x)
inhabited_h✝ : Inhabited m
inhabited_h : Inhabited n
⊢ P 0
[PROOFSTEP]
simpa using h_std_basis default default 0
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ stdBasisMatrix i j c i' j' = 0
[PROOFSTEP]
simp only [stdBasisMatrix, and_imp, ite_eq_right_iff]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i : m
j : n
c : α
i' : m
j' : n
h : ¬(i = i' ∧ j = j')
⊢ i = i' → j = j' → c = 0
[PROOFSTEP]
tauto
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i✝ : m
j✝ : n
c : α
i'✝ : m
j'✝ : n
i i' : m
hi : i ≠ i'
j j' : n
a : α
⊢ stdBasisMatrix i j a i' j' = 0
[PROOFSTEP]
simp [hi]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i✝ : m
j✝ : n
c : α
i'✝ : m
j'✝ : n
i i' : m
j j' : n
hj : j ≠ j'
a : α
⊢ stdBasisMatrix i j a i' j' = 0
[PROOFSTEP]
simp [hj]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j : n
c : α
i' j' : n
⊢ diag (stdBasisMatrix i i c) = Pi.single i c
[PROOFSTEP]
ext j
[GOAL]
case h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
by_cases hij : i = j
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
try rw [hij]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
rw [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
try rw [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
rw [hij]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : i = j
⊢ diag (stdBasisMatrix j j c) j = Pi.single j c j
[PROOFSTEP]
simp [hij]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Semiring α
i j✝ : n
c : α
i' j' j : n
hij : ¬i = j
⊢ diag (stdBasisMatrix i i c) j = Pi.single i c j
[PROOFSTEP]
simp [hij]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
h : j ≠ i
⊢ trace (stdBasisMatrix i j c) = 0
[PROOFSTEP]
simp [trace, -diag_apply, h]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
⊢ trace (stdBasisMatrix i i c) = c
[PROOFSTEP]
simp [trace, -diag_apply]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
b : n
M : Matrix n n α
⊢ (stdBasisMatrix i j c * M) i b = c * M j b
[PROOFSTEP]
simp [mul_apply, stdBasisMatrix]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a : n
M : Matrix n n α
⊢ (M * stdBasisMatrix i j c) a j = M a i * c
[PROOFSTEP]
simp [mul_apply, stdBasisMatrix, mul_comm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a b : n
h : a ≠ i
M : Matrix n n α
⊢ (stdBasisMatrix i j c * M) a b = 0
[PROOFSTEP]
simp [mul_apply, h.symm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
a b : n
hbj : b ≠ j
M : Matrix n n α
⊢ (M * stdBasisMatrix i j c) a b = 0
[PROOFSTEP]
simp [mul_apply, hbj.symm]
[GOAL]
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix j k d = stdBasisMatrix i k (c * d)
[PROOFSTEP]
ext a b
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix j k d) a b = stdBasisMatrix i k (c * d) a b
[PROOFSTEP]
simp only [mul_apply, stdBasisMatrix, boole_mul]
[GOAL]
case a.h
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₁ : i = a
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₂ : k = b
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
by_cases h₂ : k = b
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
h₂ : k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : i = a
h₂ : ¬k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case pos
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
h₂ : k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
case neg
l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k : n
d : α
a b : n
h₁ : ¬i = a
h₂ : ¬k = b
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if j = j_1 ∧ k = b then d else 0) =
    if i = a ∧ k = b then c * d else 0
[PROOFSTEP]
simp [h₁, h₂]
[GOAL]
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
⊢ stdBasisMatrix i j c * stdBasisMatrix k l d = 0
[PROOFSTEP]
ext a b
[GOAL]
case a.h
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
⊢ (stdBasisMatrix i j c * stdBasisMatrix k l d) a b = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [mul_apply, boole_mul, stdBasisMatrix]
[GOAL]
case a.h
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
by_cases h₁ : i = a
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [h₁, true_and, mul_ite, ite_mul, zero_mul, mul_zero, ← ite_and, zero_apply]
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
⊢ (∑ x : n, if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0
[PROOFSTEP]
refine Finset.sum_eq_zero (fun x _ => ?_)
[GOAL]
case pos
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
x : n
x✝ : x ∈ Finset.univ
⊢ (if (k = x ∧ l = b) ∧ j = x then c * d else 0) = 0
[PROOFSTEP]
apply if_neg
[GOAL]
case pos.hnc
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : i = a
x : n
x✝ : x ∈ Finset.univ
⊢ ¬((k = x ∧ l = b) ∧ j = x)
[PROOFSTEP]
rintro ⟨⟨rfl, rfl⟩, h⟩
[GOAL]
case pos.hnc.intro.intro
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h✝ : j ≠ k
d : α
a : n
h₁ : i = a
x✝ : k ∈ Finset.univ
h : j = k
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case neg
l✝ : Type u_1
m : Type u_2
n : Type u_3
R : Type u_4
α : Type u_5
inst✝⁴ : DecidableEq l✝
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Semiring α
i j : n
c : α
i' j' : n
inst✝ : Fintype n
k l : n
h : j ≠ k
d : α
a b : n
h₁ : ¬i = a
⊢ (∑ j_1 : n, (if i = a ∧ j = j_1 then c else 0) * if k = j_1 ∧ l = b then d else 0) = OfNat.ofNat 0 a b
[PROOFSTEP]
simp only [h₁, false_and, ite_false, mul_ite, zero_mul, mul_zero, ite_self, Finset.sum_const_zero, zero_apply]
