awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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' ⋯
⊢ k ∈ image b univ

Tactic:
apply max'_mem

Premises used: Finset.max'_mem
-- 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' ⋯
⊢ image b univ = insert k ((image b univ).erase k)

Tactic:
have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
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) =
    (M.toSquareBlock b k).det * ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det
⊢ 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

Tactic:
rw [this, prod_insert (notMem_erase _ _)]

Premises used: Finset.prod_insert, Finset.notMem_erase
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
⊢ 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) =
    (M.toSquareBlock b k).det * ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

Tactic:
congr_arg _ ?_

Premises used: congr_arg, Matrix.toSquareBlock
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
H :
  det (n := { a : m // ¬b a = k }) (M.toSquareBlockProp fun (i : m) ↦ ¬b i = k) =
    ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det
⊢ 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) =
    (M.toSquareBlock b k).det * ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

Tactic:
refine congr_arg _ ?_

Premises used: congr_arg
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
⊢ BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'

Tactic:
have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
⊢ image (fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)) univ = (image b univ).erase k

Tactic:
image_subtype_ne_univ_eq_image_erase k b

Premises used: image_subtype_ne_univ_eq_image_erase
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
⊢ image b' univ = (image b univ).erase k

Tactic:
convert! image_subtype_ne_univ_eq_image_erase k b

Premises used: image_subtype_ne_univ_eq_image_erase
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
⊢ image b' univ = (image b univ).erase k

Tactic:
have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
hb' : image b' univ = (image b univ).erase k
H :
  Eq.{v + 1} (α := R)
    (∏ a ∈ (image b univ).erase ((image b univ).max' ⋯),
      (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' a).det)
    (∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det)
⊢ det (n := { a : m // ¬b a = k }) (M.toSquareBlockProp fun (i : m) ↦ ¬b i = k) =
    ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

Tactic:
rw [ih _ (max'_mem _ _) h' hb']

Premises used: Finset.max'_mem
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
hb' : image b' univ = (image b univ).erase k
⊢ Eq.{v + 1} (α := R)
    (∏ a ∈ (image b univ).erase ((image b univ).max' ⋯),
      (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' a).det)
    (∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det)

Tactic:
Finset.prod_congr rfl fun l hl => ?_

Premises used: Finset.prod_congr, rfl
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
hb' : image b' univ = (image b univ).erase k
H :
  ∀ (l : α) (hl : l ∈ (image b univ).erase k),
    (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' l).det = (M.toSquareBlock b l).det
⊢ Eq.{v + 1} (α := R)
    (∏ a ∈ (image b univ).erase ((image b univ).max' ⋯),
      (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' a).det)
    (∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det)

Tactic:
refine Finset.prod_congr rfl fun l hl => ?_

Premises used: Finset.prod_congr, rfl
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a : { a : m // b a ≠ k } // b' a = l } ≃ { a : m // b a = l } :=
  Equiv.subtypeSubtypeEquivSubtype (p := fun (x : m) ↦ b x ≠ k) (q := fun (x : m) ↦ b x = l) ⋯
H :
  Eq.{v + 1} (α := R)
    (det.{v, u_3} (n := { a : { a : m // b a ≠ k } // b' a = l })
      ((of :
          (a : { a : { a : m // b a ≠ k } // b' a = l } → { a : { a : m // b a ≠ k } // b' a = l } → R) →
            Matrix { a : { a : m // b a ≠ k } // b' a = l } { a : { a : m // b a ≠ k } // b' a = l } R)
        fun (i j : { a : { a : m // b a ≠ k } // b' a = l }) ↦
        M.toSquareBlockProp (fun (i : m) ↦ b i ≠ k) (↑i : { a : m // b a ≠ k }) (↑j : { a : m // b a ≠ k })))
    (det.{v, u_3} (n := { a : { a : m // b a ≠ k } // b' a = l })
      ((reindex he.symm he.symm :
          (a : Matrix { a : m // b a = l } { a : m // b a = l } R) →
            Matrix { a : { a : m // b a ≠ k } // b' a = l } { a : { a : m // b a ≠ k } // b' a = l } R)
        (M.toSquareBlock b l)))
⊢ (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' l).det = (M.toSquareBlock b l).det

Tactic:
rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]

Premises used: Matrix.toSquareBlock_def, Matrix.det_reindex_self, Equiv.symm
-- 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' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : (i : { a : m // b a ≠ k }) → α := fun (i : { a : m // b a ≠ k }) ↦ b (↑i : m)
h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a : { a : m // b a ≠ k } // b' a = l } ≃ { a : m // b a = l } :=
  Equiv.subtypeSubtypeEquivSubtype (p := fun (x : m) ↦ b x ≠ k) (q := fun (x : m) ↦ b x = l) ⋯
⊢ Eq.{v + 1} (α := R)
    (det.{v, u_3} (n := { a : { a : m // b a ≠ k } // b' a = l })
      ((of :
          (a : { a : { a : m // b a ≠ k } // b' a = l } → { a : { a : m // b a ≠ k } // b' a = l } → R) →
            Matrix { a : { a : m // b a ≠ k } // b' a = l } { a : { a : m // b a ≠ k } // b' a = l } R)
        fun (i j : { a : { a : m // b a ≠ k } // b' a = l }) ↦
        M.toSquareBlockProp (fun (i : m) ↦ b i ≠ k) (↑i : { a : m // b a ≠ k }) (↑j : { a : m // b a ≠ k })))
    (det.{v, u_3} (n := { a : { a : m // b a ≠ k } // b' a = l })
      ((reindex he.symm he.symm :
          (a : Matrix { a : m // b a = l } { a : m // b a = l } R) →
            Matrix { a : { a : m // b a ≠ k } // b' a = l } { a : { a : m // b a ≠ k } // b' a = l } R)
        (M.toSquareBlock b l)))

Tactic:
rfl
-- 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
H : b j < b i
⊢ M i j = 0

Tactic:
apply hM
-- 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
H : b j < k
⊢ b j < b i

Tactic:
rw [hi]
-- 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
apply : b j ≤ k
⊢ b j < k

Tactic:
apply lt_of_le_of_ne _ hj

Premises used: lt_of_le_of_ne
-- 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j ≤ k

Tactic:
Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

Premises used: Finset.mem_univ, Finset.univ, Finset.le_max', Finset.mem_image_of_mem, Finset.image
-- 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' ⋯
i : m
hi : b i = k
j : m
hj : ¬b j = k
⊢ b j ≤ k

Tactic:
exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

Premises used: Finset.mem_univ, Finset.univ, Finset.le_max', Finset.mem_image_of_mem, Finset.image
-- 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
s : Finset α
hs : image b univ = s
H :
  ∀ (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_5 : DecidableEq m] [inst_6 : Fintype m]
    (hM : M.BlockTriangular b) (hs : image b univ = s), M.det = ∏ a ∈ s, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det

Tactic:
induction s using Finset.eraseInduction generalizing m with | H s ih =>
  subst hs
  cases isEmpty_or_nonempty m
  · simp
  let k := (univ.image b).max' (univ_nonempty.image _)
  rw [twoBlockTriangular_det' M fun i => b i = k]
  · have : univ.image b = insert k ((univ.image b).erase k) := by
      rw [insert_erase]
      apply max'_mem
    rw [this, prod_insert (notMem_erase _ _)]
    refine congr_arg _ ?_
    let b' := fun i : { a // b a ≠ k } => b ↑i
    have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
    have hb' : image b' univ = (image b univ).erase k := by
      convert! image_subtype_ne_univ_eq_image_erase k b
    rw [ih _ (max'_mem _ _) h' hb']
    refine Finset.prod_congr rfl fun l hl => ?_
    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
    rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
    rfl
  · intro i hi j hj
    apply hM
    rw [hi]
    apply lt_of_le_of_ne _ hj
    exact Finset.le_max' (univ.image b) _ (mem_image_of_mem _ (mem_univ _))

Premises used: Finset.mem_univ, Matrix.toSquareBlock_def, Finset.prod_insert, Finset.univ, isEmpty_or_nonempty, Finset.prod_congr, congr_arg, Finset.le_max', Finset.eraseInduction, Finset.notMem_erase, Finset.mem_image_of_mem, Finset.image, 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 : Fintype α
inst_5 : LinearOrder α
h : M.BlockTriangular b
⊢ M.det = ∏ k : α, (M.toSquareBlock b k).det

Tactic:
h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)

Premises used: Finset.prod_subset, Matrix.BlockTriangular.det, Finset.subset_univ, Eq.trans
-- 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 : Fintype α
inst_5 : LinearOrder α
h : M.BlockTriangular b
refine : ∀ (a : α), Membership.mem (γ := Finset α) univ a → ∀ (ha : a ∉ image b univ), (M.toSquareBlock b a).det = 1
⊢ M.det = ∏ k : α, (M.toSquareBlock b k).det

Tactic:
refine h.det.trans (prod_subset (subset_univ _) fun a _ ha => ?_)

Premises used: Finset.prod_subset, Matrix.BlockTriangular.det, Finset.subset_univ, Eq.trans
-- 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 : Fintype α
inst_5 : LinearOrder α
h : M.BlockTriangular b
a : α
h_1 : Membership.mem (γ := Finset α) univ a
ha : a ∉ image b univ
⊢ IsEmpty.{max 1 (u_3 + 1)} { i : m // b i = a }

Tactic:
have : IsEmpty { i // b i = a } := ⟨fun i => ha <| mem_image.2 ⟨i, mem_univ _, i.2⟩⟩
-- 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 : Fintype α
inst_5 : LinearOrder α
h : M.BlockTriangular b
a : α
h_1 : Membership.mem (γ := Finset α) univ a
ha : a ∉ image b univ
this : IsEmpty.{max 1 (u_3 + 1)} { i : m // b i = a }
⊢ (M.toSquareBlock b a).det = 1

Tactic:
det_isEmpty

Premises used: Matrix.det_isEmpty