awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
⊢ b i = k ∨ b i < (image b univ).max' ⋯

Tactic:
(le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt

Premises used: Finset.mem_univ, LE.le.eq_or_lt, Finset.le_max', Finset.mem_image_of_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
H : ∀ (hbi : b i = k), M⁻¹ i j = 0
H₁ : ∀ (hi : b i < (image b univ).max' ⋯), M⁻¹ i j = 0
⊢ M⁻¹ i j = 0

Tactic:
obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt

Premises used: Finset.mem_univ, LE.le.eq_or_lt, Finset.le_max', Finset.mem_image_of_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hbi : b i = k
⊢ M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) (fun (i : m) ↦ b i < k)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ k ≤ b i) a) i ⋯)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ b i < k) a) j ⋯) =
    0

Tactic:
simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]

Premises used: Matrix.zero_apply, Matrix.toBlock_inverse_eq_zero
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hbi : b i = k
⊢ M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) (fun (i : m) ↦ b i < k)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ k ≤ b i) a) i ⋯)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ b i < k) a) j ⋯) =
    0

Tactic:
have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
      simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hbi : b i = k
this :
  M⁻¹.toBlock (fun (i : m) ↦ k ≤ b i) (fun (i : m) ↦ b i < k)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ k ≤ b i) a) i ⋯)
      (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ b i < k) a) j ⋯) =
    0
⊢ M⁻¹ i j = 0

Tactic:
simp [this.symm]

Premises used: Eq.symm
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
H : ∀ (this : Invertible A), M⁻¹ i j = 0
⊢ M⁻¹ i j = 0

Tactic:
haveI : Invertible A := hM.invertibleToBlock _
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
⊢ A.BlockTriangular b'

Tactic:
have hA : A.BlockTriangular b' := hM.submatrix
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ image (fun (i : { a : m // (fun (a : α) ↦ a < k) (b a) }) ↦ b (↑i : m)) univ ⊂ image b univ

Tactic:
image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)

Premises used: lt_irrefl, Set.Mem, setOf, LT.lt, image_subtype_univ_ssubset_image_univ
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
convert! : k ∈ image b univ
⊢ image b' univ ⊂ image b univ

Tactic:
convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)

Premises used: lt_irrefl, LT.lt, image_subtype_univ_ssubset_image_univ
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ (image b univ).max' ⋯ ∈ image b univ

Tactic:
max'_mem (α := α) _ _

Premises used: Finset.max'_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ k ∈ image b univ

Tactic:
convert! max'_mem (α := α) _ _

Premises used: Finset.max'_mem
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
⊢ image b' univ ⊂ image b univ

Tactic:
have hb' : image b' univ ⊂ image b univ := by
    convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
    convert! max'_mem (α := α) _ _
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
simp_rw : b j < b i
⊢ b' (Subtype.mk (p := fun (a : m) ↦ b a < k) j ⋯) < b' (Subtype.mk (p := fun (a : m) ↦ b a < k) i hi)

Tactic:
simp_rw [b', hij]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
⊢ b' (Subtype.mk (p := fun (a : m) ↦ b a < k) j ⋯) < b' (Subtype.mk (p := fun (a : m) ↦ b a < k) i hi)

Tactic:
have hij' : b' ⟨j, hij.trans hi⟩ < b' ⟨i, hi⟩ := by simp_rw [b', hij]
-- Module: Mathlib.LinearAlgebra.Matrix.Block
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
m : Type u_3
M : Matrix m m R
b : m → α
inst_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
ih :
  ∀ t ⊂ image b univ,
    ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
      (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b
i j : m
hij : b j < b i
this_1 : Inhabited m
k : α := (image b univ).max' ⋯
b' : (i : { a : m // b a < k }) → α := fun (i : { a : m // b a < k }) ↦ b (↑i : m)
A : Matrix.{u_3, u_3, v} { a : m // b a < k } { a : m // b a < k } R :=
  M.toBlock (fun (i : m) ↦ b i < k) fun (j : m) ↦ b j < k
hi : b i < (image b univ).max' ⋯
this : Invertible A
hA : A.BlockTriangular b'
hb' : image b' univ ⊂ image b univ
hij' : b' (Subtype.mk (p := fun (a : m) ↦ b a < k) j ⋯) < b' (Subtype.mk (p := fun (a : m) ↦ b a < k) i hi)
⊢ M⁻¹ i j = 0

Tactic:
simp [A, hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]

Premises used: Finset.univ, Matrix.BlockTriangular.inv_toBlock, Eq.symm, 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 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
s : Finset α
hs : image b univ = s
H :
  ∀ (s : Finset α)
    (ih :
      ∀ t ⊂ s,
        ∀ {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
          (hM : M.BlockTriangular b) (hs : image b univ = t), M⁻¹.BlockTriangular b)
    {m : Type u_3} {M : Matrix m m R} {b : m → α} [inst_5 : DecidableEq m] [inst_6 : Fintype m] [Invertible M]
    (hM : M.BlockTriangular b) (hs : image b univ = s), M⁻¹.BlockTriangular b
⊢ M⁻¹.BlockTriangular b

Tactic:
induction s using Finset.strongInduction generalizing m with | H s ih =>
  subst hs
  intro i j hij
  haveI : Inhabited m := ⟨i⟩
  let k := (univ.image b).max' (univ_nonempty.image _)
  let b' := fun i : { a // b a < k } => b ↑i
  let A := M.toBlock (fun i => b i < k) fun j => b j < k
  obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
  · have : M⁻¹.toBlock (fun i => k ≤ b i) (fun i => b i < k) ⟨i, hbi.ge⟩ ⟨j, hbi ▸ hij⟩ = 0 := by
      simp only [toBlock_inverse_eq_zero hM k, Matrix.zero_apply]
    simp [this.symm]
  haveI : Invertible A := hM.invertibleToBlock _
  have hA : A.BlockTriangular b' := hM.submatrix
  have hb' : image b' univ ⊂ image b univ := by
    convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
    convert! max'_mem (α := α) _ _
  have hij' : b' ⟨j, hij.trans hi⟩ < b' ⟨i, hi⟩ := by simp_rw [b', hij]
  simp [A, hM.inv_toBlock k, (ih (image b' univ) hb' hA rfl hij').symm]

Premises used: Finset.strongInduction
-- Module: Mathlib.LinearAlgebra.Matrix.CharP
Goal:
n : Type u_1
R : Type u_2
inst : AddMonoidWithOne R
inst_1 : DecidableEq n
inst_2 : Nonempty n
p : ℕ
inst_3 : CharP R p
k : ℕ
simp_rw : Eq (α := Matrix n n R) (diagonal fun (x : n) ↦ (↑k : R)) 0 ↔ p ∣ k
simp_rw₁ : Eq (α := Matrix n n R) (diagonal fun (x : n) ↦ (↑k : R)) (diagonal fun (x : n) ↦ 0) ↔ p ∣ k
simp_rw₂ : (∀ (i : n), Eq.{u_2 + 1} (α := R) (↑k : R) 0) ↔ p ∣ k
simp_rw₃ : (∀ (i : n), p ∣ k) ↔ p ∣ k
⊢ Eq (α := Matrix n n R) (↑k : Matrix n n R) 0 ↔ p ∣ k

Tactic:
simp_rw [← diagonal_natCast, ← diagonal_zero, diagonal_eq_diagonal_iff,
    CharP.cast_eq_zero_iff R p k, forall_const]

Premises used: Matrix.diagonal_natCast, Matrix.diagonal_eq_diagonal_iff, Matrix.diagonal_zero, forall_const, CharP.cast_eq_zero_iff
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
inst_3 : Nontrivial R
i j : n
pos : ∀ (h : i = j), natDegree (M.charmatrix i j) = if i = j then 1 else 0
neg : ∀ (h : ¬i = j), natDegree (M.charmatrix i j) = if i = j then 1 else 0
⊢ natDegree (M.charmatrix i j) = if i = j then 1 else 0

Tactic:
by_cases h : i = j
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
inst_3 : Nontrivial R
i j : n
h : i = j
⊢ natDegree (M.charmatrix i j) = if i = j then 1 else 0

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
inst_3 : Nontrivial R
i j : n
h : ¬i = j
⊢ natDegree (M.charmatrix i j) = if i = j then 1 else 0

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
pos : ∀ (h : i = j), natDegree (M.charmatrix i j) ≤ 1
neg : ∀ (h : ¬i = j), natDegree (M.charmatrix i j) ≤ 0
⊢ natDegree (M.charmatrix i j) ≤ if i = j then 1 else 0

Tactic:
split_ifs with h
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
h : i = j
⊢ natDegree (M.charmatrix i j) ≤ 1

Tactic:
simp [h, natDegree_X_le]

Premises used: Polynomial.natDegree_X_le
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
i j : n
h : ¬i = j
⊢ natDegree (M.charmatrix i j) ≤ 0

Tactic:
simp [h, natDegree_X_le]

Premises used: Polynomial.natDegree_X_le
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
rw :
  (∑ x ∈ Finset.erase univ (Equiv.refl n),
            HMul.hMul (α := R[X])
              (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
              (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i) +
          HMul.hMul (α := R[X])
            (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) (Equiv.refl n)) : ℤ) : R[X])
            (∏ i : n, M.charmatrix ((Equiv.refl n : (a : n) → n) i) i) -
        ∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).degree <
    (↑(Fintype.card n - 1) : WithBot ℕ)
⊢ (HSub.hSub (α := R[X]) M.charpoly
        (∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X]))).degree <
    (↑(Fintype.card n - 1) : WithBot ℕ)

Tactic:
rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)),
    sum_insert (notMem_erase (Equiv.refl n) univ), add_comm]

Premises used: Finset.mem_univ, Finset.univ, add_comm, Finset.notMem_erase, Finset.sum_insert, Matrix.det_apply', Finset.insert_erase, Equiv.refl, Matrix.charpoly
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
simp :
  degree.{u} (R := R)
      (∑ x ∈ Finset.erase univ (Equiv.refl n),
        HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
          (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i)) <
    (↑(Fintype.card n - 1) : WithBot ℕ)
⊢ (∑ x ∈ Finset.erase univ (Equiv.refl n),
            HMul.hMul (α := R[X])
              (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
              (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i) +
          HMul.hMul (α := R[X])
            (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) (Equiv.refl n)) : ℤ) : R[X])
            (∏ i : n, M.charmatrix ((Equiv.refl n : (a : n) → n) i) i) -
        ∏ i : n, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (M i i) : R[X])).degree <
    (↑(Fintype.card n - 1) : WithBot ℕ)

Tactic:
simp only [charmatrix_apply_eq, one_mul, Equiv.Perm.sign_refl, id, Int.cast_one,
    Units.val_one, add_sub_cancel_right, Equiv.coe_refl]

Premises used: Matrix.charmatrix_apply_eq, id, Equiv.Perm.sign_refl, Equiv.coe_refl, Units.val_one, add_sub_cancel_right, one_mul, Int.cast_one
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
rw :
  Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (∑ x ∈ Finset.erase univ (Equiv.refl n),
      HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
        (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i))
⊢ degree.{u} (R := R)
      (∑ x ∈ Finset.erase univ (Equiv.refl n),
        HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
          (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i)) <
    (↑(Fintype.card n - 1) : WithBot ℕ)

Tactic:
rw [← mem_degreeLT]

Premises used: Polynomial.mem_degreeLT
-- Module: Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
apply :
  ∀ c ∈ Finset.erase univ (Equiv.refl n),
    Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
      (HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R[X])
        (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (∑ x ∈ Finset.erase univ (Equiv.refl n),
      HMul.hMul (α := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) x) : ℤ) : R[X])
        (∏ i : n, M.charmatrix ((x : (a : n) → n) i) i))

Tactic:
apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))

Premises used: Polynomial.degreeLT, Submodule.sum_mem, HSub.hSub, Fintype.card, OfNat.ofNat