Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have hbε : 0 < cardPowDegree b • ε := by
  rw [Algebra.smul_def, eq_intCast]
  exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have q_pos : 0 < Fintype.card Fq := by linarith
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have q_pos' : (0 : ℝ) < Fintype.card Fq := by assumption_mod_cast
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ¬natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
by_cases le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ¬natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
rw [not_le] at le_b
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
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
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
simp only at deg_lt
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
use i₀, i₁, i_ne
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε

case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
by_cases h : A i₁ % b = A i₀ % b
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
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_ofNat, Int.cast_pow, Int.cast_ofNat,
    log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_nat_cast, ← rpow_nat_cast, log_rpow q_pos',
    log_rpow q_pos', ← lt_div_iff (log_pos one_lt_q'), add_div,
    mul_div_cancel _ (log_pos one_lt_q').ne']
case neg.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ℕ

case neg.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑?neg.refine'_1✝

case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑?neg.refine'_1✝ ≤ ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
refine' lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
case neg.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑?neg.refine'_1✝

case neg.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ℕ

case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑?neg.refine'_1✝ ≤ ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
case neg.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ℕ

case neg.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑?neg.refine'_1✝

case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑?neg.refine'_1✝ ≤ ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
swap
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑(natDegree b) - -(log ε / log ↑(Fintype.card Fq))
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
rw [← sub_neg_eq_add, neg_div]
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑(natDegree b) - ↑⌈-(log ε / log ↑(Fintype.card Fq))⌉₊
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑(natDegree b) - -(log ε / log ↑(Fintype.card Fq))
refine' le_trans _ (sub_le_sub_left (Nat.le_ceil _) (b.natDegree : ℝ))
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑(natDegree b) - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-(log ε / log ↑(Fintype.card Fq))⌉₊) ≤ ↑(natDegree b) - ↑⌈-(log ε / log ↑(Fintype.card Fq))⌉₊
rw [← neg_div]
no goals
case neg.refine'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊) ≤ ↑(natDegree b) - ↑⌈-log ε / log ↑(Fintype.card Fq)⌉₊
exact le_of_eq (Nat.cast_sub le_b.le)
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
⊢ 0 < ↑(↑cardPowDegree b) * ε
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
⊢ 0 < ↑cardPowDegree b • ε
rw [Algebra.smul_def, eq_intCast]
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
⊢ 0 < ↑(↑cardPowDegree b) * ε
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
⊢ 1 < ↑(Fintype.card Fq)
assumption_mod_cast
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
⊢ 0 < Fintype.card Fq
linarith
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
⊢ 0 < ↑(Fintype.card Fq)
assumption_mod_cast
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
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
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
refine' ⟨i₀, i₁, i_ne, _⟩
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
simp only at mod_eq
no goals
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : natDegree b ≤ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
mod_eq : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
rwa [mod_eq, sub_self, map_zero, Int.cast_zero]
no goals
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : A i₁ % b = A i₀ % b
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
rwa [h, sub_self, map_zero, Int.cast_zero]
no goals
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
this : ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑(natDegree b) + log ε / log ↑(Fintype.card Fq)
⊢ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
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_ofNat, Int.cast_pow, Int.cast_ofNat,
  log_mul (pow_ne_zero _ q_pos'.ne') hε.ne', ← rpow_nat_cast, ← rpow_nat_cast, log_rpow q_pos',
  log_rpow q_pos', ← lt_div_iff (log_pos one_lt_q'), add_div,
  mul_div_cancel _ (log_pos one_lt_q').ne']
case h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) = degree (A i₁ % b - A i₀ % b)
case neg.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) < ↑?neg.refine'_1✝
convert deg_lt
case h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) = ↑(natDegree (A i₁ % b - A i₀ % b))
case h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) = degree (A i₁ % b - A i₀ % b)
rw [degree_eq_natDegree h']
no goals
case h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
b : Fq[X]
hb : b ≠ 0
ε : ℝ
hε : 0 < ε
A : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)) → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
one_lt_q : 1 < Fintype.card Fq
one_lt_q' : 1 < ↑(Fintype.card Fq)
q_pos : 0 < Fintype.card Fq
q_pos' : 0 < ↑(Fintype.card Fq)
le_b : ⌈-log ε / log ↑(Fintype.card Fq)⌉₊ < natDegree b
i₀ i₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
i_ne : i₀ ≠ i₁
deg_lt : degree (A i₁ % b - A i₀ % b) < ↑(natDegree b - ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
h : ¬A i₁ % b = A i₀ % b
h' : A i₁ % b - A i₀ % b ≠ 0
⊢ ↑(natDegree (A i₁ % b - A i₀ % b)) = ↑(natDegree (A i₁ % b - A i₀ % b))
rfl