case mk.mk
α : Type u_1
β : Type ?u.31715
m : Type ?u.31718
n : Type ?u.31721
o : Type ?u.31724
m' : α → Type u_2
n' : α → Type ?u.31734
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : { fst := j, snd := j' }.fst < { fst := i, snd := i' }.fst
⊢ blockDiagonal' d { fst := i, snd := i' } { fst := j, snd := j' } = 0
α : Type u_1
β : Type ?u.31715
m : Type ?u.31718
n : Type ?u.31721
o : Type ?u.31724
m' : α → Type u_2
n' : α → Type ?u.31734
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ BlockTriangular (blockDiagonal' d) Sigma.fst
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
no goals
case mk.mk
α : Type u_1
β : Type ?u.31715
m : Type ?u.31718
n : Type ?u.31721
o : Type ?u.31724
m' : α → Type u_2
n' : α → Type ?u.31734
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : { fst := j, snd := j' }.fst < { fst := i, snd := i' }.fst
⊢ blockDiagonal' d { fst := i, snd := i' } { fst := j, snd := j' } = 0
apply blockDiagonal'_apply_ne d i' j' fun h' => ne_of_lt h h'.symm