[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
⊢ BlockTriangular (↑(reindex e e) M) b ↔ BlockTriangular M (b ∘ ↑e)
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ BlockTriangular M (b ∘ ↑e)
[PROOFSTEP]
convert h.submatrix
[GOAL]
case h.e'_6
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular (↑(reindex e e) M) b
⊢ M = submatrix (↑(reindex e e) M) ↑e ↑e
[PROOFSTEP]
simp only [reindex_apply, submatrix_submatrix, submatrix_id_id, Equiv.symm_comp_self]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ BlockTriangular (↑(reindex e e) M) b
[PROOFSTEP]
convert h.submatrix
[GOAL]
case h.e'_7
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b✝ : m → α
inst✝ : LT α
b : n → α
e : m ≃ n
h : BlockTriangular M (b ∘ ↑e)
⊢ b = (b ∘ ↑e) ∘ fun i => ↑e.symm i
[PROOFSTEP]
simp only [comp.assoc b e e.symm, Equiv.self_comp_symm, comp.right_id]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b : m → α
inst✝ : LT α
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
h : b j < b i
⊢ (M + N) i j = 0
[PROOFSTEP]
simp_rw [Matrix.add_apply, hM h, hN h, zero_add]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝¹ : CommRing R
M N : Matrix m m R
b : m → α
inst✝ : LT α
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
h : b j < b i
⊢ (M - N) i j = 0
[PROOFSTEP]
simp_rw [Matrix.sub_apply, hM h, hN h, sub_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
⊢ BlockTriangular (blockDiagonal' d) Sigma.fst
[PROOFSTEP]
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : (i : α) → Matrix (m' i) (m' i) R
i : α
i' : m' i
j : α
j' : m' j
h : { fst := j, snd := j' }.fst < { fst := i, snd := i' }.fst
⊢ blockDiagonal' d { fst := i, snd := i' } { fst := j, snd := j' } = 0
[PROOFSTEP]
apply blockDiagonal'_apply_ne d i' j' fun h' => ne_of_lt h h'.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ BlockTriangular (blockDiagonal d) Prod.snd
[PROOFSTEP]
rintro ⟨i, i'⟩ ⟨j, j'⟩ h
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ blockDiagonal d (i, i') (j, j') = 0
[PROOFSTEP]
rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']
[GOAL]
case mk.mk.a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M N : Matrix m m R
b : m → α
inst✝¹ : Preorder α
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').snd < (i, i').snd
⊢ { fst := j', snd := j }.fst < { fst := i', snd := i }.fst
[PROOFSTEP]
exact h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
⊢ BlockTriangular (M * N) b
[PROOFSTEP]
intro i j hij
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ (M * N) i j = 0
[PROOFSTEP]
apply Finset.sum_eq_zero
[GOAL]
case h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
⊢ ∀ (x : m), x ∈ univ → (fun j => M i j) x * (fun j_1 => N j_1 j) x = 0
[PROOFSTEP]
intro k _
[GOAL]
case h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
[PROOFSTEP]
by_cases hki : b k < b i
[GOAL]
case pos
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
[PROOFSTEP]
simp_rw [hM hki, zero_mul]
[GOAL]
case neg
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
R : Type v
inst✝² : CommRing R
M✝ N✝ : Matrix m m R
b : m → α
inst✝¹ : LinearOrder α
inst✝ : Fintype m
M N : Matrix m m R
hM : BlockTriangular M b
hN : BlockTriangular N b
i j : m
hij : b j < b i
k : m
a✝ : k ∈ univ
hki : ¬b k < b i
⊢ (fun j => M i j) k * (fun j_1 => N j_1 j) k = 0
[PROOFSTEP]
simp_rw [hN (lt_of_lt_of_le hij (le_of_not_lt hki)), mul_zero]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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)
[PROOFSTEP]
rintro (c | c) (d | d) hcd
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : m
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inl d) < Sum.elim (fun x => a) (fun x => b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0
[PROOFSTEP]
first
| simp [hab.not_lt] at hcd ⊢
[GOAL]
case inl.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : m
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inl d) < Sum.elim (fun x => a) (fun x => b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inl d) = 0
[PROOFSTEP]
simp [hab.not_lt] at hcd ⊢
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : m
d : n
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inr d) < Sum.elim (fun x => a) (fun x => b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0
[PROOFSTEP]
first
| simp [hab.not_lt] at hcd ⊢
[GOAL]
case inl.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : m
d : n
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inr d) < Sum.elim (fun x => a) (fun x => b) (Sum.inl c)
⊢ fromBlocks A B 0 D (Sum.inl c) (Sum.inr d) = 0
[PROOFSTEP]
simp [hab.not_lt] at hcd ⊢
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : n
d : m
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inl d) < Sum.elim (fun x => a) (fun x => b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0
[PROOFSTEP]
first
| simp [hab.not_lt] at hcd ⊢
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : n
d : m
hcd : Sum.elim (fun x => a) (fun x => b) (Sum.inl d) < Sum.elim (fun x => a) (fun x => b) (Sum.inr c)
⊢ fromBlocks A B 0 D (Sum.inr c) (Sum.inl d) = 0
[PROOFSTEP]
simp [hab.not_lt] at hcd ⊢
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
first
| simp [hab.not_lt] at hcd ⊢
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simp [hab.not_lt] at hcd ⊢
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p q : m → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
e : ∀ (x : m), q x ↔ p x
⊢ det (toSquareBlockProp M p) = det (toSquareBlockProp M q)
[PROOFSTEP]
convert Matrix.det_reindex_self (Equiv.subtypeEquivRight e) (toSquareBlockProp M q)
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ det M =
    det
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
        (toBlock M (fun j => ¬p j) fun j => ¬p j))
[PROOFSTEP]
rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ det (↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M) =
    det
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
        (toBlock M (fun j => ¬p j) fun j => ¬p j))
[PROOFSTEP]
rw [det_apply', det_apply']
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ∑ σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a }),
      ↑↑(↑Equiv.Perm.sign σ) *
        ∏ i : { a // p a } ⊕ { a // ¬p a }, ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (↑σ i) i =
    ∑ σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a }),
      ↑↑(↑Equiv.Perm.sign σ) *
        ∏ i : { a // p a } ⊕ { a // ¬p a },
          fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
            (toBlock M (fun j => ¬p j) fun j => ¬p j) (↑σ i) i
[PROOFSTEP]
congr
[GOAL]
case e_f
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ (fun σ =>
      ↑↑(↑Equiv.Perm.sign σ) *
        ∏ i : { a // p a } ⊕ { a // ¬p a }, ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (↑σ i) i) =
    fun σ =>
    ↑↑(↑Equiv.Perm.sign σ) *
      ∏ i : { a // p a } ⊕ { a // ¬p a },
        fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
          (toBlock M (fun j => ¬p j) fun j => ¬p j) (↑σ i) i
[PROOFSTEP]
ext σ
[GOAL]
case e_f.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ ↑↑(↑Equiv.Perm.sign σ) *
      ∏ i : { a // p a } ⊕ { a // ¬p a }, ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (↑σ i) i =
    ↑↑(↑Equiv.Perm.sign σ) *
      ∏ i : { a // p a } ⊕ { a // ¬p a },
        fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
          (toBlock M (fun j => ¬p j) fun j => ¬p j) (↑σ i) i
[PROOFSTEP]
congr
[GOAL]
case e_f.h.e_a.e_f
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
⊢ (fun i => ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (↑σ i) i) = fun i =>
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (↑σ i) i
[PROOFSTEP]
ext x
[GOAL]
case e_f.h.e_a.e_f.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x : { a // p a } ⊕ { a // ¬p a }
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (↑σ x) x =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (↑σ x) x
[PROOFSTEP]
generalize hy : σ x = y
[GOAL]
case e_f.h.e_a.e_f.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
x y : { a // p a } ⊕ { a // ¬p a }
hy : ↑σ x = y
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y x =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) y x
[PROOFSTEP]
cases x
[GOAL]
case e_f.h.e_a.e_f.h.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
y : { a // p a } ⊕ { a // ¬p a }
val✝ : { a // p a }
hy : ↑σ (Sum.inl val✝) = y
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y (Sum.inl val✝) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) y (Sum.inl val✝)
[PROOFSTEP]
cases y
[GOAL]
case e_f.h.e_a.e_f.h.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
y : { a // p a } ⊕ { a // ¬p a }
val✝ : { a // ¬p a }
hy : ↑σ (Sum.inr val✝) = y
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M y (Sum.inr val✝) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) y (Sum.inr val✝)
[PROOFSTEP]
cases y
[GOAL]
case e_f.h.e_a.e_f.h.inl.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // p a }
hy : ↑σ (Sum.inl val✝¹) = Sum.inl val✝
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inl val✝¹) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (Sum.inl val✝) (Sum.inl val✝¹)
[PROOFSTEP]
simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Equiv.sumCompl_apply_inl,
  fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁, fromBlocks_apply₂₂, Matrix.submatrix_apply]
[GOAL]
case e_f.h.e_a.e_f.h.inl.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // p a }
val✝ : { a // ¬p a }
hy : ↑σ (Sum.inl val✝¹) = Sum.inr val✝
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inl val✝¹) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (Sum.inr val✝) (Sum.inl val✝¹)
[PROOFSTEP]
simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Equiv.sumCompl_apply_inl,
  fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁, fromBlocks_apply₂₂, Matrix.submatrix_apply]
[GOAL]
case e_f.h.e_a.e_f.h.inr.inl
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ : { a // ¬p a }
val✝ : { a // p a }
hy : ↑σ (Sum.inr val✝¹) = Sum.inl val✝
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inl val✝) (Sum.inr val✝¹) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (Sum.inl val✝) (Sum.inr val✝¹)
[PROOFSTEP]
simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Equiv.sumCompl_apply_inl,
  fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁, fromBlocks_apply₂₂, Matrix.submatrix_apply]
[GOAL]
case e_f.h.e_a.e_f.h.inr.inr
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
σ : Equiv.Perm ({ a // p a } ⊕ { a // ¬p a })
val✝¹ val✝ : { a // ¬p a }
hy : ↑σ (Sum.inr val✝¹) = Sum.inr val✝
⊢ ↑(reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M (Sum.inr val✝) (Sum.inr val✝¹) =
    fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
      (toBlock M (fun j => ¬p j) fun j => ¬p j) (Sum.inr val✝) (Sum.inr val✝¹)
[PROOFSTEP]
simp only [Matrix.reindex_apply, toBlock_apply, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Equiv.sumCompl_apply_inl,
  fromBlocks_apply₁₁, fromBlocks_apply₁₂, fromBlocks_apply₂₁, fromBlocks_apply₂₂, Matrix.submatrix_apply]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det M = det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
[PROOFSTEP]
rw [det_toBlock M p]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det
      (fromBlocks (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) p)
        (toBlock M (fun j => ¬p j) fun j => ¬p j)) =
    det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
[PROOFSTEP]
convert det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j) (toBlock M (fun j => ¬p j) fun j => ¬p j)
[GOAL]
case h.e'_2.h.e'_6.h.e'_8
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ toBlock M (fun j => ¬p j) p = 0
[PROOFSTEP]
ext i j
[GOAL]
case h.e'_2.h.e'_6.h.e'_8.a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a // ¬p a }
j : { a // p a }
⊢ toBlock M (fun j => ¬p j) p i j = OfNat.ofNat 0 i j
[PROOFSTEP]
exact h (↑i) i.2 (↑j) j.2
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ det M = det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
[PROOFSTEP]
rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ det (toSquareBlockProp M fun i => ¬¬p i) * det (toSquareBlockProp M fun i => ¬p i) =
    det (toSquareBlockProp M p) * det (toSquareBlockProp M fun i => ¬p i)
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
[PROOFSTEP]
congr 1
[GOAL]
case e_a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ det (toSquareBlockProp M fun i => ¬¬p i) = det (toSquareBlockProp M p)
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
[PROOFSTEP]
exact equiv_block_det _ fun _ => not_not.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
[PROOFSTEP]
simpa only [Classical.not_not] using h
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : BlockTriangular M b
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
clear N
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : BlockTriangular M b
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
induction' hs : univ.image b using Finset.strongInduction with s ih generalizing m
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs✝ : image b✝ univ = x✝
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
hs : image b univ = s
⊢ det M = ∏ a in s, det (toSquareBlock M b a)
[PROOFSTEP]
subst hs
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
cases isEmpty_or_nonempty m
[GOAL]
case H.inl
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : IsEmpty m
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
simp
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
let k := (univ.image b).max' (univ_nonempty.image _)
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ det M = ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
rw [twoBlockTriangular_det' M fun i => b i = k]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ det (toSquareBlockProp M fun i => b i = k) * det (toSquareBlockProp M fun i => ¬b i = k) =
    ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
have : univ.image b = insert k ((univ.image b).erase k) :=
  by
  rw [insert_erase]
  apply max'_mem
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ image b univ = insert k (erase (image b univ) k)
[PROOFSTEP]
rw [insert_erase]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ k ∈ image b univ
[PROOFSTEP]
apply max'_mem
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
⊢ det (toSquareBlockProp M fun i => b i = k) * det (toSquareBlockProp M fun i => ¬b i = k) =
    ∏ a in image b univ, det (toSquareBlock M b a)
[PROOFSTEP]
rw [this, prod_insert (not_mem_erase _ _)]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
⊢ det (toSquareBlockProp M fun i => b i = k) * det (toSquareBlockProp M fun i => ¬b i = k) =
    det (toSquareBlock M b k) * ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
refine' congr_arg _ _
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
⊢ det (toSquareBlockProp M fun i => ¬b i = k) = ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
let b' := fun i : { a // b a ≠ k } => b ↑i
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
⊢ det (toSquareBlockProp M fun i => ¬b i = k) = ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
⊢ det (toSquareBlockProp M fun i => ¬b i = k) = ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
have hb' : image b' univ = (image b univ).erase k := by convert image_subtype_ne_univ_eq_image_erase k b
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
⊢ image b' univ = erase (image b univ) k
[PROOFSTEP]
convert image_subtype_ne_univ_eq_image_erase k b
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
⊢ det (toSquareBlockProp M fun i => ¬b i = k) = ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
rw [ih _ (erase_ssubset <| max'_mem _ _) h' hb']
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
⊢ ∏ a in erase (image b univ) (max' (image b univ) (_ : Finset.Nonempty (image b univ))),
      det (toSquareBlock (toSquareBlockProp M fun i => b i ≠ k) b' a) =
    ∏ x in erase (image b univ) k, det (toSquareBlock M b x)
[PROOFSTEP]
refine' Finset.prod_congr rfl fun l hl => _
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
l : α
hl : l ∈ erase (image b univ) k
⊢ det (toSquareBlock (toSquareBlockProp M fun i => b i ≠ k) b' l) = det (toSquareBlock M b l)
[PROOFSTEP]
let he : { a // b' a = l } ≃ { a // b a = l } :=
  haveI hc : ∀ i, b i = l → b i ≠ k := fun i hi => ne_of_eq_of_ne hi (ne_of_mem_erase hl)
  Equiv.subtypeSubtypeEquivSubtype @(hc)
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
l : α
hl : l ∈ erase (image b univ) k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype (_ : ∀ (i : m), b i = l → b i ≠ k)
⊢ det (toSquareBlock (toSquareBlockProp M fun i => b i ≠ k) b' l) = det (toSquareBlock M b l)
[PROOFSTEP]
simp only [toSquareBlock_def]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
l : α
hl : l ∈ erase (image b univ) k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype (_ : ∀ (i : m), b i = l → b i ≠ k)
⊢ det
      (↑of fun i j =>
        toSquareBlockProp M (fun i => b i ≠ max' (image b univ) (_ : Finset.Nonempty (image b univ))) ↑i ↑j) =
    det (↑of fun i j => M ↑i ↑j)
[PROOFSTEP]
erw [← Matrix.det_reindex_self he.symm fun i j : { a // b a = l } => M ↑i ↑j]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
this : image b univ = insert k (erase (image b univ) k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : BlockTriangular (toSquareBlockProp M fun i => b i ≠ k) b'
hb' : image b' univ = erase (image b univ) k
l : α
hl : l ∈ erase (image b univ) k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype (_ : ∀ (i : m), b i = l → b i ≠ k)
⊢ det
      (↑of fun i j =>
        toSquareBlockProp M (fun i => b i ≠ max' (image b univ) (_ : Finset.Nonempty (image b univ))) ↑i ↑j) =
    det (↑(reindex he.symm he.symm) fun i j => M ↑i ↑j)
[PROOFSTEP]
rfl
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ ∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0
[PROOFSTEP]
intro i hi j hj
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ M i j = 0
[PROOFSTEP]
apply hM
[GOAL]
case H.inr.a
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j < b i
[PROOFSTEP]
rw [hi]
[GOAL]
case H.inr.a
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j < k
[PROOFSTEP]
apply lt_of_le_of_ne _ hj
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝³ : DecidableEq α
inst✝² : LinearOrder α
hM✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
        BlockTriangular M b → image b univ = t → det M = ∏ a in t, det (toSquareBlock M b a)
h✝ : Nonempty m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j ≤ k
[PROOFSTEP]
exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
⊢ det M = ∏ k : α, det (toSquareBlock M b k)
[PROOFSTEP]
refine' h.det.trans (prod_subset (subset_univ _) fun a _ ha => _)
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
⊢ det (toSquareBlock M b a) = 1
[PROOFSTEP]
have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : LinearOrder α
h : BlockTriangular M b
a : α
x✝ : a ∈ univ
ha : ¬a ∈ image b univ
this : IsEmpty { i // b i = a }
⊢ det (toSquareBlock M b a) = 1
[PROOFSTEP]
exact det_isEmpty
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 m
h : BlockTriangular M id
⊢ det M = ∏ i : m, M i i
[PROOFSTEP]
haveI : DecidableEq R := Classical.decEq _
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 m
h : BlockTriangular M id
this : DecidableEq R
⊢ det M = ∏ i : m, M i i
[PROOFSTEP]
simp_rw [h.det, image_id, det_toSquareBlock_id]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 m
M : Matrix m m R
h : BlockTriangular M ↑toDual
⊢ det M = ∏ i : m, M i i
[PROOFSTEP]
rw [← det_transpose]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 m
M : Matrix m m R
h : BlockTriangular M ↑toDual
⊢ det Mᵀ = ∏ i : m, M i i
[PROOFSTEP]
exact det_of_upperTriangular h.transpose
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
let p i := b i < k
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
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]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_self]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
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))
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simpa using hM (lt_of_lt_of_le j.2 (le_of_not_lt i.2))
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simpa [h_zero] using h_sum
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simpa only [invOf_eq_nonsing_inv] using hM.toBlock_inverse_mul_toBlock_eq_one k
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
let p i := b i < k
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
let q i := ¬b i < k
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
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
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
rw [← toBlock_mul_eq_add, inv_mul_of_invertible M, toBlock_one_disjoint]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
rw [disjoint_iff_inf_le]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 ≤ ⊥
[PROOFSTEP]
exact fun i h => h.1 h.2
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
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)
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
ext i j
[GOAL]
case a.h
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simpa using hM (lt_of_lt_of_le j.2 <| le_of_not_lt i.2)
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
have h_mul_eq_zero : M⁻¹.toBlock q p * M.toBlock p p = 0 := by simpa [h_zero] using h_sum
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
simpa [h_zero] using h_sum
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
haveI : Invertible (M.toBlock p p) := hM.invertibleToBlock k
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
have : (fun i => k ≤ b i) = q := by
  ext
  exact not_lt.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
ext
[GOAL]
case h.a
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝
[PROOFSTEP]
exact not_lt.symm
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
[PROOFSTEP]
rw [this, ← Matrix.zero_mul (M.toBlock p p)⁻¹, ← h_mul_eq_zero, mul_inv_cancel_right_of_invertible]
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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
⊢ BlockTriangular M⁻¹ b
[PROOFSTEP]
clear N
[GOAL]
α : Type u_1
β : Type u_2
m : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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 : BlockTriangular M b
⊢ BlockTriangular M⁻¹ b
[PROOFSTEP]
induction' hs : univ.image b using Finset.strongInduction with s ih generalizing m
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs✝ : image b✝ univ = x✝
s : Finset α
ih :
  ∀ (t : Finset α),
    t ⊂ s →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
hs : image b univ = s
⊢ BlockTriangular M⁻¹ b
[PROOFSTEP]
subst hs
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
⊢ BlockTriangular M⁻¹ b
[PROOFSTEP]
intro i j hij
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
⊢ M⁻¹ i j = 0
[PROOFSTEP]
haveI : Inhabited m := ⟨i⟩
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
⊢ M⁻¹ i j = 0
[PROOFSTEP]
let k := (univ.image b).max' (univ_nonempty.image _)
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
⊢ M⁻¹ i j = 0
[PROOFSTEP]
let b' := fun i : { a // b a < k } => b ↑i
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
⊢ M⁻¹ i j = 0
[PROOFSTEP]
let A := M.toBlock (fun i => b i < k) fun j => b j < k
[GOAL]
case H
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
⊢ M⁻¹ i j = 0
[PROOFSTEP]
obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
[GOAL]
case H.inl
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hbi : b i = k
⊢ M⁻¹ i j = 0
[PROOFSTEP]
have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
  simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hbi : b i = k
⊢ toBlock M⁻¹ (fun i => k ≤ b i) (fun i => b i < k) { val := i, property := (_ : k ≤ b i) }
      { val := j, property := (_ : (fun i => b i < k) j) } =
    0
[PROOFSTEP]
simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
[GOAL]
case H.inl
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hbi : b i = k
this :
  toBlock M⁻¹ (fun i => k ≤ b i) (fun i => b i < k) { val := i, property := (_ : k ≤ b i) }
      { val := j, property := (_ : (fun i => b i < k) j) } =
    0
⊢ M⁻¹ i j = 0
[PROOFSTEP]
simp [this.symm]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
⊢ M⁻¹ i j = 0
[PROOFSTEP]
haveI : Invertible A := hM.invertibleToBlock _
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
⊢ M⁻¹ i j = 0
[PROOFSTEP]
have hA : A.BlockTriangular b' := hM.submatrix
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
⊢ M⁻¹ i j = 0
[PROOFSTEP]
have hb' : image b' univ ⊂ image b univ :=
  by
  convert image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
  convert max'_mem (α := α) _ _
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
⊢ image b' univ ⊂ image b univ
[PROOFSTEP]
convert image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
⊢ k ∈ image b univ
[PROOFSTEP]
convert max'_mem (α := α) _ _
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
hb' : image b' univ ⊂ image b univ
⊢ M⁻¹ i j = 0
[PROOFSTEP]
have hij' : b' ⟨j, hij.trans hi⟩ < b' ⟨i, hi⟩ := by simp_rw [hij]
[GOAL]
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
hb' : image b' univ ⊂ image b univ
⊢ b' { val := j, property := (_ : b j < k) } < b' { val := i, property := hi }
[PROOFSTEP]
simp_rw [hij]
[GOAL]
case H.inr
α : Type u_1
β : Type u_2
m✝ : Type u_3
n : Type u_4
o : Type u_5
m' : α → Type u_6
n' : α → Type u_7
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✝ : BlockTriangular M✝ b✝
x✝ : Finset α
hs : image b✝ univ = x✝
m : Type u_3
M : Matrix m m R
b : m → α
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : Invertible M
hM : BlockTriangular M b
ih :
  ∀ (t : Finset α),
    t ⊂ image b univ →
      ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m]
        [inst_2 : Invertible M], BlockTriangular M b → image b univ = t → BlockTriangular M⁻¹ b
i j : m
hij : b j < b i
this✝ : Inhabited m
k : α := max' (image b univ) (_ : Finset.Nonempty (image b univ))
b' : { a // b a < k } → α := fun i => b ↑i
A : Matrix { a // b a < k } { a // b a < k } R := toBlock M (fun i => b i < k) fun j => b j < k
hi : b i < max' (image b univ) (_ : ∃ x, x ∈ image b univ)
this : Invertible A
hA : BlockTriangular A b'
hb' : image b' univ ⊂ image b univ
hij' : b' { val := j, property := (_ : b j < k) } < b' { val := i, property := hi }
⊢ M⁻¹ i j = 0
[PROOFSTEP]
simp [hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]
