awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
apply : ℕ
apply₁ :
  (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) <
    (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)
apply₂ :
  (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : ℝ) ≤
    (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : ℝ) < (↑b.natDegree : ℝ) + log ε / log (↑(Fintype.card Fq) : ℝ)

Tactic:
apply lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _

Premises used: Iff.mpr, WithBot.coe_lt_coe, Iff.mp, Nat.cast_lt, lt_of_lt_of_le
-- 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
⊢ (A i₁ % b - A i₀ % b).degree < (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)

Tactic:
deg_lt
-- 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
h₁ : (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (A i₁ % b - A i₀ % b).degree
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) <
    (↑(b.natDegree - ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊) : WithBot ℕ)

Tactic:
convert! deg_lt
-- 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
h₁ : (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ)
⊢ (↑(A i₁ % b - A i₀ % b).natDegree : WithBot ℕ) = (A i₁ % b - A i₀ % b).degree

Tactic:
rw [degree_eq_natDegree h']

Premises used: Polynomial.degree_eq_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 : ⌈-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).natDegree : WithBot ℕ)

Tactic:
rfl
-- 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
rw :
  HSub.hSub (α := ℝ) (↑b.natDegree : ℝ) (↑⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ : ℝ) ≤
    (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)
⊢ (↑(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]

Premises used: neg_div, Nat.cast_sub, LT.lt.le, sub_neg_eq_add
-- 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
grw grw₁ :
  (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ) ≤
    (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)
⊢ HSub.hSub (α := ℝ) (↑b.natDegree : ℝ) (↑⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊ : ℝ) ≤
    (↑b.natDegree : ℝ) - -log ε / log (↑(Fintype.card Fq) : ℝ)

Tactic:
grw [← Nat.le_ceil]

Premises used: Nat.le_ceil
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
⊢ 0 < a

Tactic:
have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg : ∀ (hxy' : ¬x = y), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
by_cases hxy' : x = y
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 pos₁ pos₂ pos₃ : (cardPowDegree : (a : Fq[X]) → ℤ) (y - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
rwa [hxy']
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg : ∀ (hyz' : ¬y = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
by_cases hyz' : y = z
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 pos₁ pos₂ pos₃ : (cardPowDegree : (a : Fq[X]) → ℤ) (x - y) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
rwa [← hyz']
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg : ∀ (hxz' : ¬x = z), (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
by_cases hxz' : x = z
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
pos₁ : (cardPowDegree : (a : Fq[X]) → ℤ) 0 < a
pos₂ pos₃ pos₄ pos₅ : 0 < a
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
rwa [hxz', sub_self, map_zero]

Premises used: sub_self, map_zero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
⊢ x - y ≠ 0

Tactic:
rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'

Premises used: sub_ne_zero, Ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
⊢ y - z ≠ 0

Tactic:
rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'

Premises used: sub_ne_zero, Ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
⊢ x - z ≠ 0

Tactic:
rw [← Ne, ← sub_ne_zero] at hxy' hyz' hxz'

Premises used: sub_ne_zero, Ne
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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

Tactic:
lt_of_le_of_lt ?_ (max_lt hxy hyz)

Premises used: lt_of_le_of_lt, max_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
neg :
  LE.le (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) (x - z) : ℤ)
    (max ((cardPowDegree : (a : Fq[X]) → ℤ) (x - y)) ((cardPowDegree : (a : Fq[X]) → ℤ) (y - z)) : ℤ)
⊢ (cardPowDegree : (a : Fq[X]) → ℤ) (x - z) < a

Tactic:
refine lt_of_le_of_lt ?_ (max_lt hxy hyz)

Premises used: lt_of_le_of_lt, max_lt
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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
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)
⊢ LE.le (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) (x - z) : ℤ)
    (max ((cardPowDegree : (a : Fq[X]) → ℤ) (x - y)) ((cardPowDegree : (a : Fq[X]) → ℤ) (y - z)) : ℤ)

Tactic:
rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy',
    cardPowDegree_nonzero _ hyz']

Premises used: Polynomial.cardPowDegree_nonzero
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 (α := ℤ) 1 (↑(Fintype.card Fq) : ℤ)

Tactic:
have : (1 : ℤ) ≤ Fintype.card Fq := mod_cast (@Fintype.one_lt_card Fq _ _).le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℤ)
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
⊢ 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:
simp only [le_max_iff]

Premises used: le_max_iff
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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

Tactic:
Or.imp (pow_le_pow_right₀ this) (pow_le_pow_right₀ this) ?_

Premises used: pow_le_pow_right₀, Or.imp
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℤ)
neg : (x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree
⊢ 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:
refine Or.imp (pow_le_pow_right₀ this) (pow_le_pow_right₀ this) ?_

Premises used: pow_le_pow_right₀, Or.imp
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℤ)
neg : (x - z).degree ≤ max (x - y).degree (y - z).degree
⊢ (x - z).natDegree ≤ (x - y).natDegree ∨ (x - z).natDegree ≤ (y - z).natDegree

Tactic:
rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ←
    degree_eq_natDegree hxy', ← degree_eq_natDegree hyz']

Premises used: Polynomial.degree_eq_natDegree, le_max_iff, Polynomial.natDegree_le_iff_degree_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 - y + (y - z)).degree ≤ max (x - y).degree (y - z).degree

Tactic:
degree_add_le (x - y) (y - z)

Premises used: HSub.hSub, Polynomial.degree_add_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) : ℤ)
h : x - z = x - y + (y - z)
⊢ (x - z).degree ≤ max (x - y).degree (y - z).degree

Tactic:
convert! degree_add_le (x - y) (y - z) using 2

Premises used: HSub.hSub, Polynomial.degree_add_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 = x - y + (y - z)

Tactic:
(sub_add_sub_cancel _ _ _).symm

Premises used: sub_add_sub_cancel, Eq.symm
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 = x - y + (y - z)

Tactic:
exact (sub_add_sub_cancel _ _ _).symm

Premises used: sub_add_sub_cancel, Eq.symm
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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]
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
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → 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
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → 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
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → 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
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin 0 → Fq[X]
⊢ ∃ (t : Fin 0 → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin 0),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
⟨finZeroElim, finZeroElim⟩

Premises used: finZeroElim, Exists.intro
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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 : ℤ) ε
A : Fin 0 → Fq[X]
⊢ ∃ (t : Fin 0 → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i₀ i₁ : Fin 0),
      t i₀ = t i₁ ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
refine ⟨finZeroElim, finZeroElim⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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)
ε : ℝ
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) < ⌈ε⌉
⊢ (↑((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]

Premises used: Int.lt_ceil
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
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) < ⌈ε⌉

Tactic:
cardPowDegree_anti_archimedean

Premises used: Polynomial.cardPowDegree_anti_archimedean