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

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1
Tactic:
let p := (λ i => b i = k)
State after:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1
Tactic:
have h_sum : M⁻¹.toBlock p p * M.toBlock p p +
    M⁻¹.toBlock p (λ i => ¬ p i) * M.toBlock (λ 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.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1
Tactic:
have h_zero : ∀ i j l,
  M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0 := by
{ intro i j l
  by_cases hj : b j.1 ≤ k
  { have hj := lt_of_le_of_ne hj j.2
    have hM' := blockTriangular_inv_of_blockTriangular hM
    apply mul_eq_zero_of_left
    simpa using hM' (lt_of_lt_of_eq hj i.2.symm) }
  { have hj := lt_of_not_ge hj
    apply mul_eq_zero_of_right
    simpa using hM (lt_of_eq_of_lt l.2 hj) }}
State after:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
⊢ M⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
⊢ M⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1
Tactic:
have h_zero' :
  M⁻¹.toBlock p (λ (i : m) => ¬p i) * M.toBlock (λ (i : m) => ¬p i) p = 0 := by
{ ext i l
  apply sum_eq_zero (λ j _ => h_zero i j l) }
State after:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
h_zero' : (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 0
⊢ M⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
h_zero' : (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 0
⊢ M⁻¹.toSquareBlock b k * M.toSquareBlock b k = 1
Tactic:
simpa [h_zero'] using h_sum
State after:
no goals

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
intro i j l
State after:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
by_cases hj : b j.1 ≤ k
State after:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
{ have hj := lt_of_le_of_ne hj j.2
  have hM' := blockTriangular_inv_of_blockTriangular hM
  apply mul_eq_zero_of_left
  simpa using hM' (lt_of_lt_of_eq hj i.2.symm) }
State after:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
{ have hj := lt_of_not_ge hj
  apply mul_eq_zero_of_right
  simpa using hM (lt_of_eq_of_lt l.2 hj) }
State after:
no goals

State before:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
have hj := lt_of_le_of_ne hj j.2
State after:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
have hM' := blockTriangular_inv_of_blockTriangular hM
State after:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
hM' : M⁻¹.BlockTriangular b
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
case pos
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
hM' : M⁻¹.BlockTriangular b
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
apply mul_eq_zero_of_left
State after:
case pos.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
hM' : M⁻¹.BlockTriangular b
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j = 0

State before:
case pos.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : b ↑j ≤ k
hj : b ↑j < k
hM' : M⁻¹.BlockTriangular b
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j = 0
Tactic:
simpa using hM' (lt_of_lt_of_eq hj i.2.symm)
State after:
no goals

State before:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj : ¬b ↑j ≤ k
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
have hj := lt_of_not_ge hj
State after:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0

State before:
case neg
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
apply mul_eq_zero_of_right
State after:
case neg.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M.toBlock (fun i => ¬p i) p j l = 0

State before:
case neg.h
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 // (fun i => ¬p i) a }
l : { a // p a }
hj✝ : ¬b ↑j ≤ k
hj : k < b ↑j
⊢ M.toBlock (fun i => ¬p i) p j l = 0
Tactic:
simpa using hM (lt_of_eq_of_lt l.2 hj)
State after:
no goals

State before:
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
⊢ (M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p = 0
Tactic:
ext i l
State after:
case a
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
i l : { a // p a }
⊢ ((M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p) i l = 0 i l

State before:
case a
α : Type u_1
β : Type ?u.27607
m : Type u_2
n : Type ?u.27613
o : Type ?u.27616
m' : α → Type ?u.27621
n' : α → Type ?u.27626
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 :
  ∀ (i : { a // p a }) (j : { a // (fun i => ¬p i) a }) (l : { a // p a }),
    M⁻¹.toBlock p (fun i => ¬p i) i j * M.toBlock (fun i => ¬p i) p j l = 0
i l : { a // p a }
⊢ ((M⁻¹.toBlock p fun i => ¬p i) * M.toBlock (fun i => ¬p i) p) i l = 0 i l
Tactic:
apply sum_eq_zero (λ j _ => h_zero i j l)
State after:
no goals