awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
⊢ (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)
have 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)
Tactic: cases y
Cleared hypotheses: y, hy
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)
have 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)
Tactic: rw [det_toBlock M p]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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) (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)
have 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
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)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have h₁ : ∀ (i : { a : m // ¬p a }) (j : { a : m // p a }), M.toBlock (fun (j : m) ↦ ¬p j) p i j = 0 i j
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)
have 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)
Tactic: rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
⊢ M.det = (M.toSquareBlockProp p).det * det (n := { a : m // ¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬p i)
have rw₁ : ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0
Tactic: rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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) *
      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)
have e_a : det (n := { a : m // ¬¬p a }) (M.toSquareBlockProp fun (i : m) ↦ ¬¬p i) = (M.toSquareBlockProp p).det
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have suffices : ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det
have 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
Tactic: subst hs
Cleared hypotheses: s, ih, hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have H : IsEmpty m → M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have H₁ : Nonempty m → M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
Tactic: cases isEmpty_or_nonempty m
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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' ⋯
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have 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
Tactic: rw [twoBlockTriangular_det' M fun i => b i = k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have H₁ : ∀ (i : m), b i = k → ∀ (j : m), ¬b j = k → M i j = 0
Tactic: rw [twoBlockTriangular_det' M fun i => b i = k]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
have rw : k ∈ image b univ
Tactic: rw [insert_erase]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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' ⋯
⊢ 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
have this : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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) =
    ∏ a ∈ image b univ, (M.toSquareBlock b a).det
have 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
Tactic: rw [this, prod_insert (notMem_erase _ _)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have 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
Tactic: refine congr_arg _ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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)
⊢ 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
have h' : BlockTriangular (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b'
Tactic: have h' : BlockTriangular (M.toSquareBlockProp fun i => b i ≠ k) b' := hM.submatrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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'
⊢ 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
have hb' : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ 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
have H : Eq.{v + 1} (α := R)
  (∏ a ∈ (image b univ).erase ((image b univ).max' sorry),
    (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' a).det)
  (∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det)
Tactic: rw [ih _ (max'_mem _ _) h' hb']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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)
have 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
Tactic: refine Finset.prod_congr rfl fun l hl => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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) ⋯
⊢ (toSquareBlock (M.toSquareBlockProp fun (i : m) ↦ b i ≠ k) b' l).det = (M.toSquareBlock b l).det
have 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)))
Tactic: rw [toSquareBlock_def, ← Matrix.det_reindex_self he.symm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M i j = 0
have H : b j < b i
Tactic: apply hM
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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 < b i
have H : b j < k
Tactic: rw [hi]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have apply : b j ≤ k
Tactic: apply lt_of_le_of_ne _ hj