α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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 => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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 => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
let p i := b i < k
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
⊢ ((toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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 => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
have h_sum :
  M⁻¹.toBlock p p ⬝ M.toBlock p p +
      (M⁻¹.toBlock p fun i => ¬p i) ⬝ M.toBlock (fun i => ¬p i) p =
    1 :=
  by rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
h_zero : toBlock M (fun i => ¬p i) p = 0
⊢ ((toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
⊢ ((toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
have h_zero : M.toBlock (fun i => ¬p i) p = 0 := by
  ext (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.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
h_zero : toBlock M (fun i => ¬p i) p = 0
⊢ ((toBlock M⁻¹ (fun i => b i < k) fun i => b i < k) ⬝ toBlock M (fun i => b i < k) fun i => b i < k) = 1
simpa [h_zero] using h_sum
no goals
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
case a.h
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
i : { a // ¬p a }
j : { a // p a }
⊢ toBlock M (fun i => ¬p i) p i j = OfNat.ofNat 0 i j
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
⊢ toBlock M (fun i => ¬p i) p = 0
ext (i j)
no goals
case a.h
α : Type u_1
β : Type ?u.126037
m : Type u_2
n : Type ?u.126043
o : Type ?u.126046
m' : α → Type ?u.126051
n' : α → Type ?u.126056
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
h_sum : toBlock M⁻¹ p p ⬝ toBlock M p p + (toBlock M⁻¹ p fun i => ¬p i) ⬝ toBlock M (fun i => ¬p i) p = 1
i : { a // ¬p a }
j : { a // p a }
⊢ toBlock M (fun i => ¬p i) p i j = OfNat.ofNat 0 i j
simpa using hM (lt_of_lt_of_le j.2 (le_of_not_lt i.2))