α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
let p i := b i < k
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
let q i := ¬b i < k
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
have h_sum : M⁻¹.toBlock q p ⬝ M.toBlock p p + M⁻¹.toBlock q q ⬝ M.toBlock q p = 0 := by
  rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
  rw [disjoint_iff_inf_le]
  exact fun i h => h.1 h.2
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
have h_zero : M.toBlock q p = 0 := by
  ext (i j)
  simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_lt i.2)
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
have h_mul_eq_zero : M⁻¹.toBlock q p ⬝ M.toBlock p p = 0 := by simpa [h_zero] using h_sum
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this : Invertible (toBlock M p p)
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this✝ : Invertible (toBlock M p p)
this : (fun i => k ≤ b i) = q
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this : Invertible (toBlock M p p)
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
have : (fun i => k ≤ b i) = q := by
  ext
  exact not_lt.symm
no goals
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this✝ : Invertible (toBlock M p p)
this : (fun i => k ≤ b i) = q
⊢ (toBlock M⁻¹ (fun i => k ≤ b i) fun i => b i < k) = 0
rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero,
  mul_inv_cancel_right_of_invertible]
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ Disjoint q p
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ q ⊓ p ≤ ⊥
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ Disjoint q p
rw [disjoint_iff_inf_le]
no goals
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
⊢ q ⊓ p ≤ ⊥
exact fun i h => h.1 h.2
case a.h
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
i : { a // q a }
j : { a // p a }
⊢ toBlock M q p i j = OfNat.ofNat 0 i j
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
⊢ toBlock M q p = 0
ext (i j)
no goals
case a.h
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
i : { a // q a }
j : { a // p a }
⊢ toBlock M q p i j = OfNat.ofNat 0 i j
simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_lt i.2)
no goals
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
⊢ toBlock M⁻¹ q p ⬝ toBlock M p p = 0
simpa [h_zero] using h_sum
case h.a
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this : Invertible (toBlock M p p)
x✝ : m
⊢ k ≤ b x✝ ↔ q x✝
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this : Invertible (toBlock M p p)
⊢ (fun i => k ≤ b i) = q
ext
no goals
case h.a
α : Type u_1
β : Type ?u.151388
m : Type u_2
n : Type ?u.151394
o : Type ?u.151397
m' : α → Type ?u.151402
n' : α → Type ?u.151407
R : Type v
inst✝⁶ : CommRing R
M N : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : BlockTriangular M b
k : α
p : m → Prop := fun i => b i < k
q : m → Prop := fun i => ¬b i < k
h_sum : toBlock M⁻¹ q p ⬝ toBlock M p p + toBlock M⁻¹ q q ⬝ toBlock M q p = 0
h_zero : toBlock M q p = 0
h_mul_eq_zero : toBlock M⁻¹ q p ⬝ toBlock M p p = 0
this : Invertible (toBlock M p p)
x✝ : m
⊢ k ≤ b x✝ ↔ q x✝
exact not_lt.symm