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

State before:
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ (blockDiagonal' d).BlockTriangular Sigma.fst
Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
State after:
case mk.mk
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : 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 : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0

State before:
case mk.mk
α : Type u_1
β : Type ?u.1255
m : Type ?u.1258
n : Type ?u.1261
o : Type ?u.1264
m' : α → Type u_2
n' : α → Type ?u.1274
R : Type v
inst✝² : CommRing R
M : 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 : ⟨j, j'⟩.fst < ⟨i, i'⟩.fst
⊢ blockDiagonal' d ⟨i, i'⟩ ⟨j, j'⟩ = 0
Tactic:
apply blockDiagonal'_apply_ne d i' j' (fun h' => ne_of_lt h h'.symm)
State after:
no goals