α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ (M * N) i j = 0
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
⊢ BlockTriangular (M * N) b
intro i j hij
case h
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ ∀ (x : m), x ∈ univ → (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ (M * N) i j = 0
apply Finset.sum_eq_zero
case h
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
case h
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ ∀ (x : m), x ∈ univ → (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0
intro k _
case pos
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0

case neg
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : ¬b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
case h
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
by_cases hki : b k < b i
no goals
case pos
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
simp_rw [hM hki, MulZeroClass.zero_mul]
no goals
case neg
α : Type u_2
β : Type ?u.34469
m : Type u_1
n : Type ?u.34475
o : Type ?u.34478
m' : α → Type ?u.34483
n' : α → Type ?u.34488
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : ¬b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
simp_rw [hN (lt_of_lt_of_le hij (le_of_not_lt hki)), MulZeroClass.mul_zero]