α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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)
rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]
case e_a
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
congr 1
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
case e_a
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
exact equiv_block_det _ fun _ => not_not.symm
no goals
α : Type ?u.96201
β : Type ?u.96204
m : Type u_1
n : Type ?u.96210
o : Type ?u.96213
m' : α → Type ?u.96218
n' : α → Type ?u.96223
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
simpa only [Classical.not_not] using h