case mk.mk
α : Type u_1
β : Type ?u.32691
m : Type u_2
n : Type ?u.32697
o : Type ?u.32700
m' : α → Type ?u.32705
n' : α → Type ?u.32710
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ blockDiagonal d (i, i') (j, j') = 0
α : Type u_1
β : Type ?u.32691
m : Type u_2
n : Type ?u.32697
o : Type ?u.32700
m' : α → Type ?u.32705
n' : α → Type ?u.32710
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ BlockTriangular (blockDiagonal d) Prod.snd
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
case mk.mk.a
α : Type u_1
β : Type ?u.32691
m : Type u_2
n : Type ?u.32697
o : Type ?u.32700
m' : α → Type ?u.32705
n' : α → Type ?u.32710
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ { fst := j', snd := j }.fst < { fst := i', snd := i }.fst
case mk.mk
α : Type u_1
β : Type ?u.32691
m : Type u_2
n : Type ?u.32697
o : Type ?u.32700
m' : α → Type ?u.32705
n' : α → Type ?u.32710
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ blockDiagonal d (i, i') (j, j') = 0
rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']
no goals
case mk.mk.a
α : Type u_1
β : Type ?u.32691
m : Type u_2
n : Type ?u.32697
o : Type ?u.32700
m' : α → Type ?u.32705
n' : α → Type ?u.32710
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ { fst := j', snd := j }.fst < { fst := i', snd := i }.fst
exact h