awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
Goal:
α : Type u_1
R : Type v
inst : CommRing R
inst_1 : LinearOrder α
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_2 : DecidableEq m
inst_3 : Fintype m
inst_4 : Invertible M
hM : M.BlockTriangular b
hs : image b univ = s
⊢ M⁻¹.BlockTriangular b
have 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
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 : 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
⊢ M⁻¹ i j = 0
have H : ∀ (this : Inhabited m), M⁻¹ i j = 0
Tactic: haveI : Inhabited m := ⟨i⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M⁻¹ i j = 0
have H : ∀ (hbi : b i = k), M⁻¹ i j = 0
Tactic: obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
⊢ M⁻¹ i j = 0
have H₁ : ∀ (hi : b i < (image b univ).max' sorry), M⁻¹ i j = 0
Tactic: obtain hbi | hi : b i = k ∨ _ := (le_max' _ (b i) <| mem_image_of_mem _ <| mem_univ _).eq_or_lt
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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⁻¹ i j = 0
have 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 sorry)
    (Subtype.mk (p := fun (a : m) ↦ (fun (i : m) ↦ b i < k) a) j sorry) =
  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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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' ⋯
⊢ M⁻¹ i j = 0
have H : ∀ (this : Invertible A), M⁻¹ i j = 0
Tactic: haveI : Invertible A := hM.invertibleToBlock _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ M⁻¹ i j = 0
have hA : A.BlockTriangular b'
Tactic: have hA : A.BlockTriangular b' := hM.submatrix
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (goal)
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
have convert! : k ∈ image b univ
Tactic: convert! image_subtype_univ_ssubset_image_univ k b _ (fun a => a < k) (lt_irrefl _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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'
⊢ M⁻¹ i j = 0
have hb' : 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 (α := α) _ _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Block (hypothesis)
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
⊢ M⁻¹ i j = 0
have hij' : b' (Subtype.mk (p := fun (a : m) ↦ b a < k) j sorry) < 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]
-- 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 : LinearOrder α
inst_4 : Invertible M
hM : M.BlockTriangular b
s : Finset α
hs : image b univ = s
⊢ M⁻¹.BlockTriangular b
have 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
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]
Cleared hypotheses: m, M, b, inst_1, inst_2, inst_4, hM, s, hs
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.CharP (goal)
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 : ℕ
⊢ Eq (α := Matrix n n R) (↑k : Matrix n n R) 0 ↔ p ∣ k
have simp_rw : Eq (α := Matrix n n R) (diagonal fun (x : n) ↦ (↑k : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.CharP (goal)
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
⊢ Eq (α := Matrix n n R) (↑k : Matrix n n R) 0 ↔ p ∣ k
have simp_rw₁ : Eq (α := Matrix n n R) (diagonal fun (x : n) ↦ (↑k : R)) (diagonal fun (x : n) ↦ 0) ↔ p ∣ k
Tactic: simp_rw [← diagonal_natCast, ← diagonal_zero, diagonal_eq_diagonal_iff,
    CharP.cast_eq_zero_iff R p k, forall_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.CharP (goal)
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
⊢ Eq (α := Matrix n n R) (↑k : Matrix n n R) 0 ↔ p ∣ k
have simp_rw₂ : (∀ (i : n), Eq.{u_2 + 1} (α := R) (↑k : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.CharP (goal)
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
⊢ Eq (α := Matrix n n R) (↑k : Matrix n n R) 0 ↔ p ∣ k
have simp_rw₃ : (∀ (i : n), p ∣ k) ↔ p ∣ k
Tactic: simp_rw [← diagonal_natCast, ← diagonal_zero, diagonal_eq_diagonal_iff,
    CharP.cast_eq_zero_iff R p k, forall_const]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ natDegree (M.charmatrix i j) = if i = j then 1 else 0
have pos : ∀ (h : i = j), natDegree (M.charmatrix i j) = if i = j then 1 else 0
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ natDegree (M.charmatrix i j) = if i = j then 1 else 0
have neg : ∀ (h : ¬i = j), natDegree (M.charmatrix i j) = if i = j then 1 else 0
Tactic: by_cases h : i = j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ natDegree (M.charmatrix i j) ≤ if i = j then 1 else 0
have pos : ∀ (h : i = j), natDegree (M.charmatrix i j) ≤ 1
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
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
⊢ natDegree (M.charmatrix i j) ≤ if i = j then 1 else 0
have neg : ∀ (h : ¬i = j), natDegree (M.charmatrix i j) ≤ 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ (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 ℕ)
have 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 ℕ)
Tactic: rw [charpoly, det_apply', ← insert_erase (mem_univ (Equiv.refl n)),
    sum_insert (notMem_erase (Equiv.refl n) univ), add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n 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) +
          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 ℕ)
have 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 ℕ)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ 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 ℕ)
have 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))
Tactic: rw [← mem_degreeLT]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
⊢ 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))
have 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))
Tactic: apply Submodule.sum_mem (degreeLT R (Fintype.card n - 1))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : 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))
have rw : Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
  (HSMul.hSMul (α := R) (β := R[X]) (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R)
    (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))
Tactic: rw [← C_eq_intCast, C_mul']
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (HSMul.hSMul (α := R) (β := R[X])
      (↑(↑(((Equiv.Perm.sign : Equiv.Perm n →* ℤˣ) : (a : Equiv.Perm n) → ℤˣ) c) : ℤ) : R)
      (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i))
have apply : Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1)) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)
Tactic: apply Submodule.smul_mem (degreeLT R (Fintype.card n - 1)) ↑↑(Equiv.Perm.sign c)
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ Membership.mem (γ := Submodule R R[X]) (degreeLT R (Fintype.card n - 1))
    (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)
have rw : degree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < (↑(Fintype.card n - 1) : WithBot ℕ)
Tactic: rw [mem_degreeLT]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ degree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < (↑(Fintype.card n - 1) : WithBot ℕ)
have apply : LT.lt (α := WithBot ℕ) (↑(natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)) : WithBot ℕ)
  (↑(Fintype.card n - 1) : WithBot ℕ)
Tactic: apply lt_of_le_of_lt degree_le_natDegree _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ LT.lt (α := WithBot ℕ) (↑(natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i)) : WithBot ℕ)
    (↑(Fintype.card n - 1) : WithBot ℕ)
have rw : natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < Fintype.card n - 1
Tactic: rw [Nat.cast_lt]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) < Fintype.card n - 1
have apply : natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) ≤
  card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
Tactic: apply lt_of_le_of_lt _ (Equiv.Perm.fixed_point_card_lt_of_ne_one (ne_of_mem_erase hc))
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ natDegree.{u} (R := R) (∏ i : n, M.charmatrix ((c : (a : n) → n) i) i) ≤
    card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
have apply : ∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i) ≤ card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
Tactic: apply le_trans (Polynomial.natDegree_prod_le univ fun i : n => charmatrix M (c i) i) _
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ ∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i) ≤ card.{v} (α := n) {x : n | (c : (a : n) → n) x = x}
have rw : LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i)) (∑ x : n with (c : (a : n) → n) x = x, 1)
Tactic: rw [card_eq_sum_ones]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff (goal)
Goal:
R : Type u
inst : CommRing R
n : Type v
inst_1 : DecidableEq n
inst_2 : Fintype n
M : Matrix n n R
c : n ≃ n
hc : c ∈ Finset.erase univ (Equiv.refl n)
⊢ LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i)) (∑ x : n with (c : (a : n) → n) x = x, 1)
have rw : LE.le (α := ℕ) (∑ i : n, natDegree (M.charmatrix ((c : (a : n) → n) i) i))
  (∑ a : n, if (c : (a : n) → n) a = a then 1 else 0)
Tactic: rw [sum_filter]