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

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
let p := (fun i => b i < k)
State after:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
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]
State after:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
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)) }
State after:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
h_zero : M.toBlock (fun i => ¬p i) p = 0
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
h_zero : M.toBlock (fun i => ¬p i) p = 0
⊢ ((M⁻¹.toBlock (fun i => b i < k) fun i => b i < k) * M.toBlock (fun i => b i < k) fun i => b i < k) = 1
Tactic:
simpa [h_zero] using h_sum
State after:
no goals

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
⊢ M⁻¹.toBlock p p * M.toBlock p p + (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 1
Tactic:
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
State after:
no goals

State before:
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
⊢ M.toBlock (fun i => ¬p i) p = 0
Tactic:
ext i j
State after:
case a
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
i : { a // ¬p a }
j : { a // p a }
⊢ M.toBlock (fun i => ¬p i) p i j = 0 i j

State before:
case a
α : Type u_1
β : Type ?u.3857
m : Type u_2
n : Type ?u.3863
o : Type ?u.3866
m' : α → Type ?u.3871
n' : α → Type ?u.3876
R : Type v
inst✝⁶ : CommRing R
M : Matrix m m R
b : m → α
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : LinearOrder α
inst✝ : Invertible M
hM : M.BlockTriangular b
k : α
p : m → Prop := fun i => b i < k
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
i : { a // ¬p a }
j : { a // p a }
⊢ M.toBlock (fun i => ¬p i) p i j = 0 i j
Tactic:
simpa using hM (lt_of_lt_of_le j.2 (le_of_not_lt i.2))
State after:
no goals