-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem BlockTriangular.det [DecidableEq α] [LinearOrder α] (hM : BlockTriangular M b) :
    M.det = ∏ a ∈ univ.image b, (M.toSquareBlock b a).det

Proof state:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : (M.toSquareBlockProp fun i => b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ (of fun i j => M.toSquareBlockProp (fun i => b i ≠ k) ↑i ↑j).det = ((reindex he.symm he.symm) fun i j => M ↑i ↑j).det

Tactic:
rfl

Result:
no goals

Proof state:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : (M.toSquareBlockProp fun i => b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
⊢ ((M.toSquareBlockProp fun i => b i ≠ k).toSquareBlock b' l).det = (M.toSquareBlock b l).det

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

Result:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : (M.toSquareBlockProp fun i => b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
l : α
hl : l ∈ (image b univ).erase k
he : { a // b' a = l } ≃ { a // b a = l } := Equiv.subtypeSubtypeEquivSubtype ⋯
⊢ ((M.toSquareBlockProp fun i => b i ≠ k).toSquareBlock b' l).det = (M.toSquareBlock b l).det

Proof state:
case H
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Tactic:
cases isEmpty_or_nonempty m

Result:
case H.inl
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : IsEmpty m
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
⊢ M.det = ∏ a ∈ image b univ, (M.toSquareBlock b a).det

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : M.BlockTriangular b
⊢ ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det

Tactic:
intro s hs

Result:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : M.BlockTriangular b
s : Finset α
hs : image b univ = s
⊢ M.det = ∏ a ∈ s, (M.toSquareBlock b a).det

Proof state:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : M.BlockTriangular b
⊢ 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

Result:
α : Type u_1
m : Type u_3
R : Type v
M : Matrix m m R
b : m → α
inst✝⁴ : CommRing R
inst✝³ : DecidableEq m
inst✝² : Fintype m
inst✝¹ : DecidableEq α
inst✝ : LinearOrder α
hM : M.BlockTriangular b
⊢ ∀ (hs : Finset α), image b univ = hs → M.det = ∏ a ∈ hs, (M.toSquareBlock b a).det

Proof state:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : (M.toSquareBlockProp fun i => b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
⊢ (M.toSquareBlockProp fun i => ¬b i = k).det = ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det

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

Result:
case H.inr
α : Type u_1
R : Type v
inst✝⁴ : CommRing R
inst✝³ : DecidableEq α
inst✝² : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst✝¹ : DecidableEq m
inst✝ : Fintype m
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst : DecidableEq m] [inst_1 : Fintype m],
      M.BlockTriangular b → image b univ = t → M.det = ∏ a ∈ t, (M.toSquareBlock b a).det
h✝ : Nonempty m
k : α := (image b univ).max' ⋯
this : image b univ = insert k ((image b univ).erase k)
b' : { a // b a ≠ k } → α := fun i => b ↑i
h' : (M.toSquareBlockProp fun i => b i ≠ k).BlockTriangular b'
hb' : image b' univ = (image b univ).erase k
⊢ ∏ a ∈ (image b univ).erase ((image b univ).max' ⋯), ((M.toSquareBlockProp fun i => b i ≠ k).toSquareBlock b' a).det =
    ∏ x ∈ (image b univ).erase k, (M.toSquareBlock b x).det