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 : 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
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (A i₁ % b - A i₀ % b).degree
have h₁ : (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ)
Tactic: rw [degree_eq_natDegree h']
-- 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
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : ℝ) ≤
    (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
have rw : HSub.hSub (α := ℝ) (↑b.natDegree : ℝ) (↑⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ : ℝ) ≤
  (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)
Tactic: rw [← sub_neg_eq_add, ← neg_div, Nat.cast_sub le_b.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]
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
q_pos' : LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)
le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
deg_lt : (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ HSub.hSub (α := ℝ) (↑b.natDegree : ℝ) (↑⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ : ℝ) ≤
    (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)
have grw : (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ) ≤ (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)
Tactic: grw [← Nat.le_ceil]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have ha : 0 < a
Tactic: have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have pos : ∀ (hxy' : x = y), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hxy' : x = y
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
pos : ∀ (hxy' : x = y), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have neg : ∀ (hxy' : ¬x = y), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hxy' : x = y
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have pos : ∀ (hyz' : y = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hyz' : y = z
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
pos : ∀ (hyz' : y = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have neg : ∀ (hyz' : ¬y = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hyz' : y = z
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have pos : ∀ (hxz' : x = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hxz' : x = z
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
pos : ∀ (hxz' : x = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have neg : ∀ (hxz' : ¬x = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
Tactic: by_cases hxz' : x = z
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have pos : (cardPowDegree : (a : Fq[X]) → ℤ) (z - z) < a
Tactic: rwa [hxz', sub_self, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
pos : (cardPowDegree : (a : Fq[X]) → ℤ) (z - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have pos₁ : (cardPowDegree : (a : Fq[X]) → ℤ) 0 < a
Tactic: rwa [hxz', sub_self, map_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have hxy'₁ : x - y ≠ 0
Tactic: rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'
Cleared hypotheses: hxy', hyz', hxz'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
hxy'₁ : x - y ≠ 0
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have hyz'₁ : y - z ≠ 0
Tactic: rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'
Cleared hypotheses: hxy', hyz', hxz'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
hxy'₁ : x - y ≠ 0
hyz'₁ : y - z ≠ 0
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have hxz'₁ : x - z ≠ 0
Tactic: rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'
Cleared hypotheses: hxy', hyz', hxz'
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
have neg : LE.le (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) (x - z) : ℤ)
  (max ((cardPowDegree : (a : Fq[X]) → ℤ) (x - y)) ((cardPowDegree : (a : Fq[X]) → ℤ) (y - z)) : ℤ)
Tactic: refine lt_of_le_of_lt ?_ (max_lt hxy hyz)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ LE.le (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) (x - z) : ℤ)
    (max ((cardPowDegree : (a : Fq[X]) → ℤ) (x - y)) ((cardPowDegree : (a : Fq[X]) → ℤ) (y - z)) : ℤ)
have neg : HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
  max (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - y).natDegree)
    (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (y - z).natDegree)
Tactic: rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy',
    cardPowDegree_nonzero _ hyz']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
    max (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - y).natDegree)
      (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (y - z).natDegree)
have this : LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
Tactic: have : (1 : ℤ) ≤ Fintype.card Fq := mod_cast (@Fintype.one_lt_card Fq _ _).le
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
    max (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - y).natDegree)
      (HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (y - z).natDegree)
have neg : HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - y).natDegree ∨
  HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (y - z).natDegree
Tactic: simp only [le_max_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
⊢ HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
      HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - y).natDegree ∨
    HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (x - z).natDegree ≤
      HPow.hPow (α := ℤ) (↑(Fintype.card Fq) : ℤ) (y - z).natDegree
have neg : (x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree
Tactic: refine Or.imp (pow_le_pow_right₀ this) (pow_le_pow_right₀ this) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
⊢ (x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree
have neg : (x - z).degree ≤ max (x - y).degree (y - z).degree
Tactic: rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ←
    degree_eq_natDegree hxy', ← degree_eq_natDegree hyz']
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
x y z : Fq[X]
a : ℤ
hxy : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
hyz : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
ha : 0 < a
hxy' : x - y ≠ 0
hyz' : y - z ≠ 0
hxz' : x - z ≠ 0
this : LE.le (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)
⊢ (x - z).degree ≤ max (x - y).degree (y - z).degree
have h : x - z = x - y + (y - z)
Tactic: convert! degree_add_le (x - y) (y - z) using 2
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → 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
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin n),
      t i₀ = t 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 (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε_1 : ℝ
hε : 0 < ε_1
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε_1
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε_1 / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε_1
A : Fin (n + 1) → Fq[X]
i j k : Fin (n + 1)
ε : ℝ
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
have simp_rw : (cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b) < ⌈ε⌉ →
  (cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b) < ⌈ε⌉ →
    (cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b) < ⌈ε⌉
Tactic: simp_rw [← Int.lt_ceil]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
⊢ ∃ (t : Fin (n + 1) → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin (n + 1)),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have anti_archim' : ∀ {i j k : Fin (n + 1)} {ε : ℝ},
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
Tactic: have anti_archim' : ∀ {i j k} {ε : ℝ},
    (cardPowDegree (A i % b - A j % b) : ℝ) < ε →
      (cardPowDegree (A j % b - A k % b) : ℝ) < ε →
        (cardPowDegree (A i % b - A k % b) : ℝ) < ε := by
    intro i j k ε
    simp_rw [← Int.lt_ceil]
    exact cardPowDegree_anti_archimedean
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
⊢ ∃ (t : Fin (n + 1) → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin (n + 1)),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have succ : ∀ (t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
  (ht' :
    ∀ (i₀ i₁ : Fin n),
      t' i₀ = t' i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ)
                (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                  Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
            ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  ∃ (t : Fin (n + 1) → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin (n + 1)),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
Tactic: obtain ⟨t', ht'⟩ := ih (Fin.tail A)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ (t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i₀ i₁ : Fin n),
        t i₀ = t i₁ ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
ht' :
  ∀ (i₀ i₁ : Fin n),
    t' i₀ = t' i₁ ↔
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (t : Fin (n + 1) → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin (n + 1)),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
have succ : ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
  (hj :
    ∀ (i : Fin n),
      t' i = j ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  ∃ (t : Fin (n + 1) → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin (n + 1)),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
Tactic: rsuffices ⟨j, hj⟩ :
    ∃ j, ∀ i, t' i = j ↔ (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε