no goals
α : Type u_1
β : Type ?u.37208
m : Type u_2
n : Type u_3
o : Type ?u.37217
m' : α → Type ?u.37222
n' : α → Type ?u.37227
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
⊢ BlockTriangular (fromBlocks A B 0 D) (Sum.elim (fun x => a) fun x => b)
rintro (c | c) (d | d) hcd <;> first | simp [hab.not_lt] at hcd ⊢
no goals
case inr.inr
α : Type u_1
β : Type ?u.37208
m : Type u_2
n : Type u_3
o : Type ?u.37217
m' : α → Type ?u.37222
n' : α → Type ?u.37227
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : Preorder α
A : Matrix m m R
B : Matrix m n R
D : Matrix n n R
a b : α
hab : a < b
c d : n
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inr d) < Sum.elim (fun x => a) (fun x => b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inr d) = 0
simp [hab.not_lt] at hcd ⊢