awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ (↑j : WithBot ℕ)
pos : 0 = (A i₀).coeff j
⊢ (A i₁).coeff j = (A i₀).coeff j
have pos₁ : Eq.{u_1 + 1} (α := Fq) 0 0
Tactic: rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj),
      coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : (↑j : WithBot ℕ) < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j
have apply : j < d
Tactic: apply congr_fun i_eq.symm ⟨j, _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < degree.{u_1} (R := Fq) 0
⊢ False
have hA₁ : (A 0).degree < degree.{u_1} (R := Fq) 0
Tactic: specialize hA 0
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin m.succ → Fq[X]
hA : (A 0).degree < degree.{u_1} (R := Fq) 0
⊢ False
have hA₁ : (A 0).degree < ⊥
Tactic: rw [degree_zero] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
have hb : b ≠ 0
Tactic: have hb : b ≠ 0 := by
    rintro rfl
    specialize hA 0
    rw [degree_zero] at hA
    exact not_lt_of_ge bot_le hA
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
have this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
Tactic: have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
    simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
have obtain : ∀ (i₀ i₁ : Fin m.succ) (i_ne : i₀ ≠ i₁) (i_eq : f i₀ = f i₁),
  ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
Tactic: obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
have right : (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
Tactic: use i₀, i₁, i_ne
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ (A i₁ - A i₀).degree < (↑(b.natDegree - d) : WithBot ℕ)
have right : ∀ (j : ℕ) (hj : b.natDegree - d ≤ j), (A i₁ - A i₀).coeff j = 0
Tactic: refine (degree_lt_iff_coeff_zero _ _).mpr fun j hj => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
⊢ (A i₁ - A i₀).coeff j = 0
have pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁ - A i₀).coeff j = 0
Tactic: by_cases! hbj : degree b ≤ j
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁ - A i₀).coeff j = 0
⊢ (A i₁ - A i₀).coeff j = 0
have neg : ∀ (hbj : (↑j : WithBot ℕ) < b.degree), (A i₁ - A i₀).coeff j = 0
Tactic: by_cases! hbj : degree b ≤ j
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : b.degree ≤ (↑j : WithBot ℕ)
⊢ (A i₁ - A i₀).coeff j = 0
have pos : (A i₁ - A i₀).degree < b.degree
Tactic: refine coeff_eq_zero_of_degree_lt (lt_of_lt_of_le ?_ hbj)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : (↑j : WithBot ℕ) < b.degree
⊢ (A i₁ - A i₀).coeff j = 0
have neg : (A i₁).coeff j = (A i₀).coeff j
Tactic: rw [coeff_sub, sub_eq_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : (↑j : WithBot ℕ) < b.degree
⊢ (A i₁).coeff j = (A i₀).coeff j
have hbj₁ : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree hb] at hbj
Cleared hypotheses: hbj
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
⊢ (A i₁).coeff j = (A i₀).coeff j
have hbj₁ : j < b.natDegree
Tactic: have hbj : j < natDegree b := (@WithBot.coe_lt_coe _ _ _).mp hbj
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
⊢ b.natDegree - j.succ < d
have pos : ∀ (hd : b.natDegree < d), b.natDegree - j.succ < d
Tactic: by_cases! hd : natDegree b < d
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
pos : ∀ (hd : b.natDegree < d), b.natDegree - j.succ < d
⊢ b.natDegree - j.succ < d
have neg : ∀ (hd : d ≤ b.natDegree), b.natDegree - j.succ < d
Tactic: by_cases! hd : natDegree b < d
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : d ≤ b.natDegree
⊢ b.natDegree - j.succ < d
have this₁ : b.natDegree - d < j.succ
Tactic: have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this_1 : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hd : d ≤ b.natDegree
this : b.natDegree - d < j.succ
⊢ b.natDegree - j.succ < d
have neg : ∀ (this : b.natDegree - j.succ < d), b.natDegree - j.succ < d
Tactic: rwa [tsub_lt_iff_tsub_lt hd hbj] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
⊢ (A i₁).coeff j = (A i₀).coeff j
have hj₁ : b.natDegree - j.succ < d
Tactic: have hj : natDegree b - j.succ < d := by
    by_cases! hd : natDegree b < d
    · exact lt_of_le_of_lt tsub_le_self hd
    · have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
      rwa [tsub_lt_iff_tsub_lt hd hbj] at this
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj_1 : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ j = b.natDegree - (b.natDegree - j.succ).succ
have rw : j = b.natDegree - (b.natDegree.succ - j.succ)
Tactic: rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj_1 : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
rw : j = b.natDegree - (b.natDegree.succ - j.succ)
⊢ j = b.natDegree - (b.natDegree - j.succ).succ
have rw₁ : j = b.natDegree - (b.natDegree - j)
Tactic: rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj_1 : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
rw : j = b.natDegree - (b.natDegree.succ - j.succ)
rw₁ : j = b.natDegree - (b.natDegree - j)
⊢ j = b.natDegree - (b.natDegree - j.succ).succ
have rw₂ : j = j
Tactic: rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
hb : b ≠ 0
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (b.natDegree - (↑j.succ : ℕ))
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj_1 : b.natDegree - d ≤ j
hbj_1 : LT.lt (α := WithBot ℕ) (↑j : WithBot ℕ) (↑b.natDegree : WithBot ℕ)
hbj : j < b.natDegree
hj : b.natDegree - j.succ < d
⊢ (A i₁).coeff j = (A i₀).coeff j
have this₁ : j = b.natDegree - (b.natDegree - j.succ).succ
Tactic: have : j = b.natDegree - (natDegree b - j.succ).succ := by
    rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
⊢ 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have rw : 0 < (↑((cardPowDegree : (a : Fq[X]) → ℤ) b) : ℝ) * ε
Tactic: rw [Algebra.smul_def, eq_intCast]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
⊢ ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i₁ :
    Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ),
    i₀ ≠ i₁ ∧
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
Tactic: have hbε : 0 < cardPowDegree b • ε := by
    rw [Algebra.smul_def, eq_intCast]
    exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i₁ :
    Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ),
    i₀ ≠ i₁ ∧
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have one_lt_q : 1 < Fintype.card Fq
Tactic: have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
⊢ LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
have assumption_mod_cast : ∀ (hb : ¬b = 0) (hε : 0 < ε) (hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  1 < Fintype.card Fq
Tactic: assumption_mod_cast
Cleared hypotheses: hb, hε, hbε
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
⊢ ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i₁ :
    Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ),
    i₀ ≠ i₁ ∧
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
Tactic: have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
⊢ ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i₁ :
    Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ),
    i₀ ≠ i₁ ∧
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have q_pos : 0 < Fintype.card Fq
Tactic: have q_pos : 0 < Fintype.card Fq := by lia
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
⊢ LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
have assumption_mod_cast : ∀ (hb : ¬b = 0) (hε : 0 < ε) (hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε)
  (one_lt_q' : 1 < Fintype.card Fq), 0 < Fintype.card Fq
Tactic: assumption_mod_cast
Cleared hypotheses: hb, hε, hbε, one_lt_q'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ → Fq[X]
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)
q_pos : 0 < Fintype.card Fq
⊢ ∃ (i₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i₁ :
    Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ),
    i₀ ≠ i₁ ∧
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
Tactic: have q_pos' : (0 : ℝ) < Fintype.card Fq := by assumption_mod_cast