awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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)
rw₂ rw₃ : j = j
⊢ j = b.natDegree - (b.natDegree - j.succ).succ

Tactic:
rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]

Premises used: LT.lt.le, tsub_tsub_cancel_of_le, Nat.succ_sub, Nat.succ_sub_succ
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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

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]
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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_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
this : j = b.natDegree - (b.natDegree - j.succ).succ
⊢ f i₁ (⟨b.natDegree - j.succ, hj⟩ : Fin d) = f i₀ ⟨b.natDegree - j.succ, hj⟩

Tactic:
congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩

Premises used: HSub.hSub, Fin.mk, congr_fun, Polynomial.natDegree, Eq.symm, Nat.succ
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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_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
this : j = b.natDegree - (b.natDegree - j.succ).succ
⊢ (A i₁).coeff j = (A i₀).coeff j

Tactic:
convert! congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩

Premises used: HSub.hSub, Fin.mk, congr_fun, Polynomial.natDegree, Eq.symm, Nat.succ
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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]
rw : 0 < (↑((cardPowDegree : (a : Fq[X]) → ℤ) b) : ℝ) * ε
⊢ 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rw [Algebra.smul_def, eq_intCast]

Premises used: eq_intCast, Algebra.smul_def
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 < (↑((cardPowDegree : (a : Fq[X]) → ℤ) b) : ℝ) * ε

Tactic:
mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε

Premises used: Iff.mpr, AbsoluteValue.pos, mul_pos, Int.cast_pos
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 < (↑((cardPowDegree : (a : Fq[X]) → ℤ) b) : ℝ) * ε

Tactic:
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε

Premises used: mul_pos
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : ℤ) ε

Tactic:
have hbε : 0 < cardPowDegree b • ε := by
    rw [Algebra.smul_def, eq_intCast]
    exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : ℤ) ε
⊢ 1 < Fintype.card Fq

Tactic:
have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (hb : ¬b = 0) (hε : 0 < ε) (hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    1 < Fintype.card Fq
⊢ LT.lt (α := ℝ) 1 (↑(Fintype.card Fq) : ℝ)

Tactic:
assumption_mod_cast
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℝ)

Tactic:
have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℝ)
⊢ 0 < Fintype.card Fq

Tactic:
lia
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℝ)
⊢ 0 < Fintype.card Fq

Tactic:
have q_pos : 0 < Fintype.card Fq := by lia
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ 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
⊢ LT.lt (α := ℝ) 0 (↑(Fintype.card Fq) : ℝ)

Tactic:
assumption_mod_cast
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℝ)

Tactic:
have q_pos' : (0 : ℝ) < Fintype.card Fq := by assumption_mod_cast
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℝ)
pos :
  ∀ (le_b : b.natDegree ≤ ⌈-log ε / log (↑(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 : ℤ) ε
neg :
  ∀ (le_b : ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ < b.natDegree),
    ∃ (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 : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
by_cases! le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊

Premises used: Fintype.card, Nat.cast, Real.log, Polynomial.natDegree
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : b.natDegree ≤ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊
pos :
  ∀ (i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) (i_ne : i₀ ≠ i₁)
    (mod_eq : A i₁ % b = A i₀ % 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 : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
obtain ⟨i₀, i₁, i_ne, mod_eq⟩ :=
      exists_eq_polynomial le_rfl b le_b (fun i => A i % b) fun i => EuclideanDomain.mod_lt (A i) hb

Premises used: le_rfl, EuclideanDomain.mod_lt, HMod.hMod, Polynomial.exists_eq_polynomial
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : b.natDegree ≤ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % 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 : ℤ) ε

Tactic:
⟨i₀, i₁, i_ne, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : b.natDegree ≤ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
pos :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    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 : ℤ) ε

Tactic:
refine ⟨i₀, i₁, i_ne, ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : b.natDegree ≤ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊
i₀ i₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
pos :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₀ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₁ : (↑((cardPowDegree : (a : Fq[X]) → ℤ) 0) : ℝ) < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₂ : (↑0 : ℝ) < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₃ pos₄ pos₅ pos₆ : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rwa [mod_eq, sub_self, map_zero, Int.cast_zero]

Premises used: sub_self, Int.cast_zero, map_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg :
  ∀ (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 ℕ)),
    ∃ (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 : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
obtain ⟨i₀, i₁, i_ne, deg_lt⟩ := exists_approx_polynomial_aux le_rfl b (fun i => A i % b) fun i =>
    EuclideanDomain.mod_lt (A i) hb

Premises used: le_rfl, EuclideanDomain.mod_lt, Polynomial.exists_approx_polynomial_aux, HMod.hMod
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 ℕ)
right :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    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 : ℤ) ε

Tactic:
use i₀, i₁, i_ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 ℕ)
pos :
  ∀ (h : A i₁ % b = A i₀ % b),
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
neg :
  ∀ (h : ¬A i₁ % b = A i₀ % b),
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
by_cases h : A i₁ % b = A i₀ % b
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
pos :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₀ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₁ : (↑((cardPowDegree : (a : Fq[X]) → ℤ) 0) : ℝ) < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₂ : (↑0 : ℝ) < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos₃ pos₄ pos₅ pos₆ : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rwa [h, sub_self, map_zero, Int.cast_zero]

Premises used: sub_self, Int.cast_zero, map_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
⊢ A i₁ % b - A i₀ % b ≠ 0

Tactic:
have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg : (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
suffices (natDegree (A i₁ % b - A i₀ % b) : ℝ) < b.natDegree + log ε / log (Fintype.card Fq) by
    rwa [← Real.log_lt_log_iff (Int.cast_pos.mpr (cardPowDegree.pos h')) hbε,
      cardPowDegree_nonzero _ h', cardPowDegree_nonzero _ hb, Algebra.smul_def, eq_intCast,
      Int.cast_pow, Int.cast_natCast, Int.cast_pow, Int.cast_natCast,
      log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_natCast, ← rpow_natCast, log_rpow q_pos',
      log_rpow q_pos', ← lt_div_iff₀ (log_pos one_lt_q'), add_div,
      mul_div_cancel_right₀ _ (log_pos one_lt_q').ne']