Theorem: Matrix.BlockTriangular_blockDiagonal (CvxLean/Lib/Math/LinearAlgebra/Matrix/Block.lean)

State before:
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ (blockDiagonal d).BlockTriangular Prod.snd
Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
State after:
case mk.mk
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0

State before:
case mk.mk
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0
Tactic:
rw [blockDiagonal'_eq_blockDiagonal, BlockTriangular_blockDiagonal']
State after:
case mk.mk.a
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst

State before:
case mk.mk.a
α : Type u_1
β : Type ?u.2091
m : Type u_2
n : Type ?u.2097
o : Type ?u.2100
m' : α → Type ?u.2105
n' : α → Type ?u.2110
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
Tactic:
exact h
State after:
no goals