awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
x y : { a : m // p a } ⊕ { a : m // ¬p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) x = y
e_f :
  ∀ (val : { a : m // p a })
    (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = y),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M y (Sum.inl val) =
      fromBlocks (m := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
        (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y (Sum.inl val)
e_f₁ :
  ∀ (val : { a : m // ¬p a })
    (hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) = y),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M y (Sum.inr val) =
      fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y (Sum.inr val)
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M y x =
    fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
      (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y x

Tactic:
cases x
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
y : { a : m // p a } ⊕ { a : m // ¬p a }
val : { a : m // p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) = y
e_f :
  ∀ (val_1 : { a : m // p a })
    (hy :
      Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
          { a : m // p a } ⊕ { a : m // ¬p a })
        (Sum.inl val_1 : { a : m // p a } ⊕ { a : m // ¬p a })),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M (Sum.inl val_1) (Sum.inl val) =
      fromBlocks (m := { a : m // ¬p a }) (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
        (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inl val_1)
        (Sum.inl val)
e_f₁ :
  ∀ (val_1 : { a : m // ¬p a })
    (hy :
      Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
          { a : m // p a } ⊕ { a : m // ¬p a })
        (Sum.inr val_1 : { a : m // p a } ⊕ { a : m // ¬p a })),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M (Sum.inr val_1) (Sum.inl val) =
      fromBlocks (m := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
        (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inr val_1)
        (Sum.inl val)
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M y (Sum.inl val) =
    fromBlocks (m := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y (Sum.inl val)

Tactic:
cases y
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
y : { a : m // p a } ⊕ { a : m // ¬p a }
val : { a : m // ¬p a }
hy : (σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) = y
e_f :
  ∀ (val_1 : { a : m // p a })
    (hy :
      Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) :
          { a : m // p a } ⊕ { a : m // ¬p a })
        (Sum.inl val_1 : { a : m // p a } ⊕ { a : m // ¬p a })),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M (Sum.inl val_1) (Sum.inr val) =
      fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
        (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inl val_1)
        (Sum.inr val)
e_f₁ :
  ∀ (val_1 : { a : m // ¬p a })
    (hy :
      Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
        ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) :
          { a : m // p a } ⊕ { a : m // ¬p a })
        (Sum.inr val_1 : { a : m // p a } ⊕ { a : m // ¬p a })),
    (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
          (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
        M (Sum.inr val_1) (Sum.inr val) =
      fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inr val_1) (Sum.inr val)
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M y (Sum.inr val) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
      (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) y (Sum.inr val)

Tactic:
cases y
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
val val_1 : { a : m // p a }
hy :
  Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
    ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
      { a : m // p a } ⊕ { a : m // ¬p a })
    (Sum.inl val_1 : { a : m // p a } ⊕ { a : m // ¬p a })
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M (Sum.inl val_1) (Sum.inl val) =
    fromBlocks (m := { a : m // ¬p a }) (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inl val_1)
      (Sum.inl val)

Tactic:
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]

Premises used: Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Matrix.reindex_apply, Equiv.sumCompl_apply_inl, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Matrix.fromBlocks_apply₂₁, Matrix.submatrix_apply, Matrix.toBlock_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
val : { a : m // p a }
val_1 : { a : m // ¬p a }
hy :
  Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
    ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inl val) :
      { a : m // p a } ⊕ { a : m // ¬p a })
    (Sum.inr val_1 : { a : m // p a } ⊕ { a : m // ¬p a })
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M (Sum.inr val_1) (Sum.inl val) =
    fromBlocks (m := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inr val_1)
      (Sum.inl val)

Tactic:
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]

Premises used: Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Matrix.reindex_apply, Equiv.sumCompl_apply_inl, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Matrix.fromBlocks_apply₂₁, Matrix.submatrix_apply, Matrix.toBlock_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
val : { a : m // ¬p a }
val_1 : { a : m // p a }
hy :
  Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
    ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) :
      { a : m // p a } ⊕ { a : m // ¬p a })
    (Sum.inl val_1 : { a : m // p a } ⊕ { a : m // ¬p a })
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M (Sum.inl val_1) (Sum.inr val) =
    fromBlocks (o := { a : m // ¬p a }) (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j)
      (M.toBlock (fun (j : m) ↦ ¬p j) p) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inl val_1)
      (Sum.inr val)

Tactic:
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]

Premises used: Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Matrix.reindex_apply, Equiv.sumCompl_apply_inl, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Matrix.fromBlocks_apply₂₁, Matrix.submatrix_apply, Matrix.toBlock_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
σ : Equiv.Perm ({ a : m // p a } ⊕ { a : m // ¬p a })
val val_1 : { a : m // ¬p a }
hy :
  Eq (α := { a : m // p a } ⊕ { a : m // ¬p a })
    ((σ : (a : { a : m // p a } ⊕ { a : m // ¬p a }) → { a : m // p a } ⊕ { a : m // ¬p a }) (Sum.inr val) :
      { a : m // p a } ⊕ { a : m // ¬p a })
    (Sum.inr val_1 : { a : m // p a } ⊕ { a : m // ¬p a })
⊢ (reindex (Equiv.sumCompl p).symm (Equiv.sumCompl p).symm :
        (a : Matrix m m R) → Matrix ({ a : m // p a } ⊕ { a : m // ¬p a }) ({ a : m // p a } ⊕ { a : m // ¬p a }) R)
      M (Sum.inr val_1) (Sum.inr val) =
    fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
      (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j) (Sum.inr val_1) (Sum.inr val)

Tactic:
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]

Premises used: Matrix.fromBlocks_apply₁₁, Matrix.fromBlocks_apply₁₂, Matrix.fromBlocks_apply₂₂, Matrix.reindex_apply, Equiv.sumCompl_apply_inl, Equiv.symm_symm, Equiv.sumCompl_apply_inr, Matrix.fromBlocks_apply₂₁, Matrix.submatrix_apply, Matrix.toBlock_apply
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
rw :
  det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)) =
    (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)
⊢ M.det = (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)

Tactic:
rw [det_toBlock M p]

Premises used: Matrix.det_toBlock
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
⊢ det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) 0
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)) =
    (M.toBlock p p).det * det (n := { a : m // ¬p a }) (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)

Tactic:
det_fromBlocks_zero₂₁ (toBlock M p p) (toBlock M p fun j => ¬p j)
      (toBlock M (fun j => ¬p j) fun j => ¬p j)

Premises used: Matrix.toBlock, Matrix.det_fromBlocks_zero₂₁, Not
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
h₁ : Eq (α := Matrix.{u_3, u_3, v} { a : m // ¬p a } { a : m // p a } R) (M.toBlock (fun (j : m) ↦ ¬p j) p) 0
⊢ det (n := { a : m // p a } ⊕ { a : m // ¬p a })
      (fromBlocks (M.toBlock p p) (M.toBlock p fun (j : m) ↦ ¬p j) (M.toBlock (fun (j : m) ↦ ¬p j) p)
        (M.toBlock (fun (j : m) ↦ ¬p j) fun (j : m) ↦ ¬p j)) =
    (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)

Tactic:
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)

Premises used: Matrix.toBlock, Matrix.det_fromBlocks_zero₂₁, Not
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
h₁ : ∀ (i : { a : m // ¬p a }) (j : { a : m // p a }), M.toBlock (fun (j : m) ↦ ¬p j) p i j = 0 i j
⊢ Eq (α := Matrix.{u_3, u_3, v} { a : m // ¬p a } { a : m // p a } R) (M.toBlock (fun (j : m) ↦ ¬p j) p) 0

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a : m // ¬p a }
j : { a : m // p a }
⊢ M.toBlock (fun (j : m) ↦ ¬p j) p i j = 0 i j

Tactic:
h (↑i) i.2 (↑j) j.2

Premises used: Matrix.submatrix, Matrix.toBlock, Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), ¬p i → ∀ (j : m), p j → M i j = 0
i : { a : m // ¬p a }
j : { a : m // p a }
⊢ M.toBlock (fun (j : m) ↦ ¬p j) p i j = 0 i j

Tactic:
exact h (↑i) i.2 (↑j) j.2

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
rw :
  det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) *
      det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i) =
    (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)
rw₁ : ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
⊢ M.det = (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)

Tactic:
rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]

Premises used: Matrix.twoBlockTriangular_det, mul_comm, Not
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
e_a : det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) = (M.toSquareBlockProp p).det
⊢ det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) *
      det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i) =
    (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) = (M.toSquareBlockProp p).det

Tactic:
equiv_block_det _ fun _ => not_not.symm

Premises used: Classical.not_not, Matrix.equiv_block_det, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) = (M.toSquareBlockProp p).det

Tactic:
exact equiv_block_det _ fun _ => not_not.symm

Premises used: Classical.not_not, Matrix.equiv_block_det, Iff.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
m : Type u_3
R : Type v
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
M : Matrix m m R
p : m → Prop
inst_3 : 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

Tactic:
simpa only [Classical.not_not] using h

Premises used: Classical.not_not
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq α
inst_4 : LinearOrder α
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq α
inst_4 : LinearOrder α
hM : M.BlockTriangular b
this : ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst : CommRing R
inst_1 : DecidableEq m
inst_2 : Fintype m
inst_3 : DecidableEq α
inst_4 : LinearOrder α
hM : M.BlockTriangular b
suffices : ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
suffices ∀ hs : Finset α, univ.image b = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det by
    exact this _ rfl
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : DecidableEq α
inst_2 : LinearOrder α
s : Finset α
ih :
  ∀ s_1 ∈ s,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m]
      (hM : M.BlockTriangular b) (hs : image b univ = s.erase s_1), M.det = ∏ a ∈ s.erase s_1, (M.toSquareBlock b a).det
m : Type u_3
M : Matrix m m R
b : m → α
inst_3 : DecidableEq m
inst_4 : Fintype m
hM : M.BlockTriangular b
hs : image b univ = s
H :
  ∀
    (ih :
      ∀ s ∈ image b univ,
        ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst_5 : DecidableEq m_1] [inst_6 : Fintype m_1]
          (hM : M.BlockTriangular b_1) (hs : image b_1 univ = (image b univ).erase s),
          M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det),
    M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det

Tactic:
subst hs
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : DecidableEq α
inst_2 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_3 : DecidableEq m
inst_4 : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst_5 : DecidableEq m_1] [inst_6 : Fintype m_1]
      (hM : M.BlockTriangular b_1) (hs : image b_1 univ = (image b univ).erase s),
      M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
H : IsEmpty m → M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
H₁ : Nonempty m → M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
cases isEmpty_or_nonempty m

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : DecidableEq α
inst_2 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_3 : DecidableEq m
inst_4 : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst_5 : DecidableEq m_1] [inst_6 : Fintype m_1]
      (hM : M.BlockTriangular b_1) (hs : image b_1 univ = (image b univ).erase s),
      M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h : IsEmpty m
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : DecidableEq α
inst_2 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_3 : DecidableEq m
inst_4 : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst_5 : DecidableEq m_1] [inst_6 : Fintype m_1]
      (hM : M.BlockTriangular b_1) (hs : image b_1 univ = (image b univ).erase s),
      M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h : Nonempty m
k : α := (image b univ).max' ⋯
H :
  det (n := { a : m // b a = k }) (M.toSquareBlockProp fun (i : m) ↦ b i = k) *
      det (n := { a : m // ¬b a = k }) (M.toSquareBlockProp fun (i : m) ↦ ¬b i = k) =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det
H₁ : ∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
rw [twoBlockTriangular_det' M fun i => b i = k]

Premises used: Matrix.twoBlockTriangular_det', Eq
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : DecidableEq α
inst_2 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_3 : DecidableEq m
inst_4 : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ s ∈ image b univ,
    ∀ {m_1 : Type u_3} {M : Matrix m_1 m_1 R} {b_1 : m_1 → α} [inst_5 : DecidableEq m_1] [inst_6 : Fintype m_1]
      (hM : M.BlockTriangular b_1) (hs : image b_1 univ = (image b univ).erase s),
      M.det = ∏ a ∈ (image b univ).erase s, (M.toSquareBlock b_1 a).det
h : Nonempty m
k : α := (image b univ).max' ⋯
rw : k ∈ image b univ
⊢ image b univ = insert k ((image b univ).erase k)

Tactic:
rw [insert_erase]

Premises used: Finset.insert_erase