-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem det_toBlock (M : Matrix m m R) (p : m → Prop) [DecidablePred p] :
    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).det

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M).det =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det

Tactic:
rw [det_apply', det_apply']

Result:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
            (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ M.det =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det

Tactic:
rw [← Matrix.det_reindex_self (Equiv.sumCompl p).symm M]

Result:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
⊢ ((reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm) M).det =
    (fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
            (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Tactic:
congr

Result:
case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
          (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Proof state:
case e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
          (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Tactic:
congr

Result:
case e_f.h.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Proof state:
case e_f.h.e_a.e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ x) x

Tactic:
generalize hy : σ x = y

Result:
case e_f.h.e_a.e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) y x

Proof state:
case e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
          (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Tactic:
ext σ

Result:
case e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
          (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Proof state:
case e_f.h.e_a.e_f
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ i) i

Tactic:
ext x

Result:
case e_f.h.e_a.e_f.h
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
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 (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
      (M.toBlock (fun j => ¬p j) fun j => ¬p j) (σ x) x