case a.h
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
ext (a b)
case a.h
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
case a.h
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
simp only [mul_apply, boole_mul, stdBasisMatrix]
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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

case neg
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
case a.h
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
by_cases h₁ : i = a
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
simp only [h₁, true_and, mul_ite, ite_mul, zero_mul, mul_zero, ← ite_and, zero_apply]
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
refine Finset.sum_eq_zero (fun x _ => ?_)
case pos.hnc
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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)
case pos
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
apply if_neg
case pos.hnc.intro.intro
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
case pos.hnc
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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)
rintro ⟨⟨rfl, rfl⟩, h⟩
no goals
case pos.hnc.intro.intro
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
contradiction
no goals
case neg
l✝ : Type ?u.47153
m : Type ?u.47156
n : Type u_1
R : Type ?u.47162
α : Type u_2
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
simp only [h₁, false_and, ite_false, mul_ite, zero_mul, mul_zero, ite_self,
  Finset.sum_const_zero, zero_apply]