[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
[PROOFSTEP]
set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff j
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
[PROOFSTEP]
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
  simpa using
    lt_of_le_of_lt hm
      (Nat.lt_succ_self m)
        -- Therefore, the differences have all coefficients higher than `deg b - d` equal.
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
⊢ Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
[PROOFSTEP]
simpa using
  lt_of_le_of_lt hm
    (Nat.lt_succ_self m)
      -- Therefore, the differences have all coefficients higher than `deg b - d` equal.
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
[PROOFSTEP]
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
[GOAL]
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ A i₁ = A i₀
[PROOFSTEP]
use i₀, i₁, i_ne
[GOAL]
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ A i₁ = A i₀
[PROOFSTEP]
ext j
[GOAL]
case right.a
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
by_cases hbj : degree b ≤ j
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj), coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]
  -- So we only need to look for the coefficients between `0` and `deg b`.
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ¬degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
rw [not_le] at hbj
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
apply congr_fun i_eq.symm ⟨j, _⟩
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : natDegree b ≤ d
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) ↑j
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : ↑j < degree b
⊢ j < d
[PROOFSTEP]
exact lt_of_lt_of_le (coe_lt_degree.mp hbj) hb
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
have hb : b ≠ 0 := by
  rintro rfl
  specialize hA 0
  rw [degree_zero] at hA
  exact not_lt_of_le bot_le hA
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
⊢ b ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree 0
⊢ False
[PROOFSTEP]
specialize hA 0
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin (Nat.succ m) → Fq[X]
hA : degree (A 0) < degree 0
⊢ False
[PROOFSTEP]
rw [degree_zero] at hA
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
A : Fin (Nat.succ m) → Fq[X]
hA : degree (A 0) < ⊥
⊢ False
[PROOFSTEP]
exact not_lt_of_le bot_le hA
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
set f : Fin m.succ → Fin d → Fq := fun i j => (A i).coeff (natDegree b - j.succ)
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
  simpa using
    lt_of_le_of_lt hm
      (Nat.lt_succ_self m)
        -- Therefore, the differences have all coefficients higher than `deg b - d` equal.
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
⊢ Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
[PROOFSTEP]
simpa using
  lt_of_le_of_lt hm
    (Nat.lt_succ_self m)
      -- Therefore, the differences have all coefficients higher than `deg b - d` equal.
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
[GOAL]
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
use i₀, i₁, i_ne
[GOAL]
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ degree (A i₁ - A i₀) < ↑(natDegree b - d)
[PROOFSTEP]
refine'
  (degree_lt_iff_coeff_zero _ _).mpr fun j hj =>
    _
      -- The coefficients higher than `deg b` are the same because they are equal to 0.
[GOAL]
case right
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
⊢ coeff (A i₁ - A i₀) j = 0
[PROOFSTEP]
by_cases hbj : degree b ≤ j
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj : degree b ≤ ↑j
⊢ coeff (A i₁ - A i₀) j = 0
[PROOFSTEP]
refine' coeff_eq_zero_of_degree_lt (lt_of_lt_of_le _ hbj)
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj : degree b ≤ ↑j
⊢ degree (A i₁ - A i₀) < degree b
[PROOFSTEP]
exact
  lt_of_le_of_lt (degree_sub_le _ _)
    (max_lt (hA _) (hA _))
      -- So we only need to look for the coefficients between `deg b - d` and `deg b`.
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj : ¬degree b ≤ ↑j
⊢ coeff (A i₁ - A i₀) j = 0
[PROOFSTEP]
rw [coeff_sub, sub_eq_zero]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj : ¬degree b ≤ ↑j
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
rw [not_le, degree_eq_natDegree hb] at hbj
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj : ↑j < ↑(natDegree b)
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
have hbj : j < natDegree b := (@WithBot.coe_lt_coe _ _ _).mp hbj
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
have hj : natDegree b - j.succ < d := by
  by_cases hd : natDegree b < d
  · exact lt_of_le_of_lt tsub_le_self hd
  · rw [not_lt] at hd
    have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
    rwa [tsub_lt_iff_tsub_lt hd hbj] at this
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
⊢ natDegree b - Nat.succ j < d
[PROOFSTEP]
by_cases hd : natDegree b < d
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hd : natDegree b < d
⊢ natDegree b - Nat.succ j < d
[PROOFSTEP]
exact lt_of_le_of_lt tsub_le_self hd
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hd : ¬natDegree b < d
⊢ natDegree b - Nat.succ j < d
[PROOFSTEP]
rw [not_lt] at hd
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hd : d ≤ natDegree b
⊢ natDegree b - Nat.succ j < d
[PROOFSTEP]
have := lt_of_le_of_lt hj (Nat.lt_succ_self j)
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this✝ : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hd : d ≤ natDegree b
this : natDegree b - d < Nat.succ j
⊢ natDegree b - Nat.succ j < d
[PROOFSTEP]
rwa [tsub_lt_iff_tsub_lt hd hbj] at this
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hj : natDegree b - Nat.succ j < d
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
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]
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hj : natDegree b - Nat.succ j < d
⊢ j = natDegree b - Nat.succ (natDegree b - Nat.succ j)
[PROOFSTEP]
rw [← Nat.succ_sub hbj, Nat.succ_sub_succ, tsub_tsub_cancel_of_le hbj.le]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Ring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
A : Fin (Nat.succ m) → Fq[X]
hA : ∀ (i : Fin (Nat.succ m)), degree (A i) < degree b
hb : b ≠ 0
f : Fin (Nat.succ m) → Fin d → Fq := fun i j => coeff (A i) (natDegree b - ↑(Fin.succ j))
this✝ : Fintype.card (Fin d → Fq) < Fintype.card (Fin (Nat.succ m))
i₀ i₁ : Fin (Nat.succ m)
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hj✝ : natDegree b - d ≤ j
hbj✝ : ↑j < ↑(natDegree b)
hbj : j < natDegree b
hj : natDegree b - Nat.succ j < d
this : j = natDegree b - Nat.succ (natDegree b - Nat.succ j)
⊢ coeff (A i₁) j = coeff (A i₀) j
[PROOFSTEP]
convert congr_fun i_eq.symm ⟨natDegree b - j.succ, hj⟩
[GOAL]
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 • ε
[PROOFSTEP]
have hbε : 0 < cardPowDegree b • ε := by
  rw [Algebra.smul_def, eq_intCast]
  exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
[GOAL]
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 • ε
[PROOFSTEP]
rw [Algebra.smul_def, eq_intCast]
[GOAL]
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) * ε
[PROOFSTEP]
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
[GOAL]
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 • ε
[PROOFSTEP]
have one_lt_q : 1 < Fintype.card Fq := Fintype.one_lt_card
[GOAL]
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 • ε
[PROOFSTEP]
have one_lt_q' : (1 : ℝ) < Fintype.card Fq := by assumption_mod_cast
[GOAL]
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)
[PROOFSTEP]
assumption_mod_cast
[GOAL]
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 • ε
[PROOFSTEP]
have q_pos : 0 < Fintype.card Fq := by linarith
[GOAL]
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
[PROOFSTEP]
linarith
[GOAL]
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 • ε
[PROOFSTEP]
have q_pos' : (0 : ℝ) < Fintype.card Fq := by
  assumption_mod_cast
    -- If `b` is already small enough, then the remainders are equal and we are done.
[GOAL]
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)
[PROOFSTEP]
assumption_mod_cast
  -- If `b` is already small enough, then the remainders are equal and we are done.
[GOAL]
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 • ε
[PROOFSTEP]
by_cases le_b : b.natDegree ≤ ⌈-log ε / log (Fintype.card Fq)⌉₊
[GOAL]
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 • ε
[PROOFSTEP]
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
[GOAL]
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 • ε
[PROOFSTEP]
refine' ⟨i₀, i₁, i_ne, _⟩
[GOAL]
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 • ε
[PROOFSTEP]
rwa [mod_eq, sub_self, map_zero, Int.cast_zero]
  -- Otherwise, it suffices to choose two elements whose difference is of small enough degree.
[GOAL]
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 • ε
[PROOFSTEP]
rw [not_le] at le_b
[GOAL]
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 • ε
[PROOFSTEP]
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
[GOAL]
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 • ε
[PROOFSTEP]
use i₀, i₁, i_ne
[GOAL]
case right
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 • ε
[PROOFSTEP]
by_cases h : A i₁ % b = A i₀ % b
[GOAL]
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 • ε
[PROOFSTEP]
rwa [h, sub_self, map_zero, Int.cast_zero]
[GOAL]
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 • ε
[PROOFSTEP]
have h' : A i₁ % b - A i₀ % b ≠ 0 := mt sub_eq_zero.mp h
[GOAL]
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 • ε
[PROOFSTEP]
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']
    -- And that result follows from manipulating the result from `exists_approx_polynomial_aux`
      -- to turn the `-⌈-stuff⌉₊` into `+ stuff`.
[GOAL]
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 • ε
[PROOFSTEP]
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']
  -- And that result follows from manipulating the result from `exists_approx_polynomial_aux`
    -- to turn the `-⌈-stuff⌉₊` into `+ stuff`.
[GOAL]
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)
[PROOFSTEP]
refine' lt_of_lt_of_le (Nat.cast_lt.mpr (WithBot.coe_lt_coe.mp _)) _
[GOAL]
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)
[PROOFSTEP]
swap
[GOAL]
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✝
[PROOFSTEP]
convert deg_lt
[GOAL]
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)
[PROOFSTEP]
rw [degree_eq_natDegree h']
[GOAL]
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))
[PROOFSTEP]
rfl
[GOAL]
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)
[PROOFSTEP]
rw [← sub_neg_eq_add, neg_div]
[GOAL]
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))
[PROOFSTEP]
refine' le_trans _ (sub_le_sub_left (Nat.le_ceil _) (b.natDegree : ℝ))
[GOAL]
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))⌉₊
[PROOFSTEP]
rw [← neg_div]
[GOAL]
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)⌉₊
[PROOFSTEP]
exact le_of_eq (Nat.cast_sub le_b.le)
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
have ha : 0 < a := lt_of_le_of_lt (AbsoluteValue.nonneg _ _) hxy
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
by_cases hxy' : x = y
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : x = y
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
rwa [hxy']
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
by_cases hyz' : y = z
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : y = z
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
rwa [← hyz']
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
by_cases hxz' : x = z
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : x = z
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
rwa [hxz', sub_self, map_zero]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy' : ¬x = y
hyz' : ¬y = z
hxz' : ¬x = z
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
rw [← Ne.def, ← sub_ne_zero] at hxy' hyz' hxz'
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) < a
[PROOFSTEP]
refine' lt_of_le_of_lt _ (max_lt hxy hyz)
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑cardPowDegree (x - z) ≤ max (↑cardPowDegree (x - y)) (↑cardPowDegree (y - z))
[PROOFSTEP]
rw [cardPowDegree_nonzero _ hxz', cardPowDegree_nonzero _ hxy', cardPowDegree_nonzero _ hyz']
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
[PROOFSTEP]
have : (1 : ℤ) ≤ Fintype.card Fq := by exact_mod_cast (@Fintype.one_lt_card Fq _ _).le
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
⊢ 1 ≤ ↑(Fintype.card Fq)
[PROOFSTEP]
exact_mod_cast (@Fintype.one_lt_card Fq _ _).le
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤
    max (↑(Fintype.card Fq) ^ natDegree (x - y)) (↑(Fintype.card Fq) ^ natDegree (y - z))
[PROOFSTEP]
simp only [Int.cast_pow, Int.cast_ofNat, le_max_iff]
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (x - y) ∨
    ↑(Fintype.card Fq) ^ natDegree (x - z) ≤ ↑(Fintype.card Fq) ^ natDegree (y - z)
[PROOFSTEP]
refine' Or.imp (pow_le_pow this) (pow_le_pow this) _
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ natDegree (x - z) ≤ natDegree (x - y) ∨ natDegree (x - z) ≤ natDegree (y - z)
[PROOFSTEP]
rw [natDegree_le_iff_degree_le, natDegree_le_iff_degree_le, ← le_max_iff, ← degree_eq_natDegree hxy', ←
  degree_eq_natDegree hyz']
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ degree (x - z) ≤ max (degree (x - y)) (degree (y - z))
[PROOFSTEP]
convert degree_add_le (x - y) (y - z) using 2
[GOAL]
case h.e'_3.h.e'_3
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
x y z : Fq[X]
a : ℤ
hxy : ↑cardPowDegree (x - y) < a
hyz : ↑cardPowDegree (y - z) < a
ha : 0 < a
hxy'✝ : x ≠ y
hxy' : x - y ≠ 0
hyz'✝ : y ≠ z
hyz' : y - z ≠ 0
hxz'✝ : x ≠ z
hxz' : x - z ≠ 0
this : 1 ≤ ↑(Fintype.card Fq)
⊢ x - z = x - y + (y - z)
[PROOFSTEP]
exact (sub_add_sub_cancel _ _ _).symm
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
have hbε : 0 < cardPowDegree b • ε := by
  rw [Algebra.smul_def, eq_intCast]
  exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑cardPowDegree b • ε
[PROOFSTEP]
rw [Algebra.smul_def, eq_intCast]
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ 0 < ↑(↑cardPowDegree b) * ε
[PROOFSTEP]
exact mul_pos (Int.cast_pos.mpr (AbsoluteValue.pos _ hb)) hε
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
A : Fin Nat.zero → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin Nat.zero), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine'
  ⟨finZeroElim, finZeroElim⟩
    -- Show `anti_archimedean` also holds for real distances.
[GOAL]
case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin (Nat.succ n)), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
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
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
⊢ ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (A i % b - A k % b)) < ε
[PROOFSTEP]
intro i j k ε
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε✝ : ℝ
hε : 0 < ε✝
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε✝
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε✝
A : Fin (Nat.succ n) → Fq[X]
i j k : Fin (Nat.succ n)
ε : ℝ
⊢ ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
    ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (A i % b - A k % b)) < ε
[PROOFSTEP]
simp_rw [← Int.lt_ceil]
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε✝ : ℝ
hε : 0 < ε✝
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε✝
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε✝
A : Fin (Nat.succ n) → Fq[X]
i j k : Fin (Nat.succ n)
ε : ℝ
⊢ ↑cardPowDegree (A i % b - A j % b) < ⌈ε⌉ →
    ↑cardPowDegree (A j % b - A k % b) < ⌈ε⌉ → ↑cardPowDegree (A i % b - A k % b) < ⌈ε⌉
[PROOFSTEP]
exact cardPowDegree_anti_archimedean
[GOAL]
case succ
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (A i % b - A k % b)) < ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (Nat.succ n)), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
obtain ⟨t', ht'⟩ :=
  ih
    (Fin.tail A)
      -- We got rid of `A 0`, so determine the index `j` of the partition we'll re-add it to.
[GOAL]
case succ.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (Nat.succ n)), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
rsuffices ⟨j, hj⟩ : ∃ j, ∀ i, t' i = j ↔ (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε
[GOAL]
case succ.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin (Nat.succ n)), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' ⟨Fin.cons j t', fun i₀ i₁ => _⟩
[GOAL]
case succ.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀ i₁ : Fin (Nat.succ n)
⊢ Fin.cons j t' i₀ = Fin.cons j t' i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' Fin.cases _ (fun i₀ => _) i₀
[GOAL]
case succ.intro.intro.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀ i₁ : Fin (Nat.succ n)
⊢ Fin.cons j t' 0 = Fin.cons j t' i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A 0 % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' Fin.cases _ (fun i₁ => _) i₁
[GOAL]
case succ.intro.intro.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀✝ i₁ : Fin (Nat.succ n)
i₀ : Fin n
⊢ Fin.cons j t' (Fin.succ i₀) = Fin.cons j t' i₁ ↔
    ↑(↑cardPowDegree (A i₁ % b - A (Fin.succ i₀) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' Fin.cases _ (fun i₁ => _) i₁
[GOAL]
case succ.intro.intro.refine'_1.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀ i₁ : Fin (Nat.succ n)
⊢ Fin.cons j t' 0 = Fin.cons j t' 0 ↔ ↑(↑cardPowDegree (A 0 % b - A 0 % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
simpa using hbε
[GOAL]
case succ.intro.intro.refine'_1.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀ i₁✝ : Fin (Nat.succ n)
i₁ : Fin n
⊢ Fin.cons j t' 0 = Fin.cons j t' (Fin.succ i₁) ↔
    ↑(↑cardPowDegree (A (Fin.succ i₁) % b - A 0 % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_zero, eq_comm, AbsoluteValue.map_sub]
[GOAL]
case succ.intro.intro.refine'_1.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀ i₁✝ : Fin (Nat.succ n)
i₁ : Fin n
⊢ t' i₁ = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i₁) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
exact hj i₁
[GOAL]
case succ.intro.intro.refine'_2.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀✝ i₁ : Fin (Nat.succ n)
i₀ : Fin n
⊢ Fin.cons j t' (Fin.succ i₀) = Fin.cons j t' 0 ↔
    ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i₀) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_zero]
[GOAL]
case succ.intro.intro.refine'_2.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀✝ i₁ : Fin (Nat.succ n)
i₀ : Fin n
⊢ t' i₀ = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i₀) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
exact hj i₀
[GOAL]
case succ.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀✝ i₁✝ : Fin (Nat.succ n)
i₀ i₁ : Fin n
⊢ Fin.cons j t' (Fin.succ i₀) = Fin.cons j t' (Fin.succ i₁) ↔
    ↑(↑cardPowDegree (A (Fin.succ i₁) % b - A (Fin.succ i₀) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_succ]
[GOAL]
case succ.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i₀✝ i₁✝ : Fin (Nat.succ n)
i₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔ ↑(↑cardPowDegree (A (Fin.succ i₁) % b - A (Fin.succ i₀) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
exact ht' i₀ i₁
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
obtain ⟨j, hj⟩ : ∃ j, ∀ i : Fin n, t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε :=
  by
  by_contra hg
  push_neg at hg
  obtain ⟨j₀, j₁, j_ne, approx⟩ :=
    exists_approx_polynomial hb hε (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
  revert j_ne approx
  refine' Fin.cases _ (fun j₀ => _) j₀ <;> refine' Fin.cases (fun j_ne approx => _) (fun j₁ j_ne approx => _) j₁
  · exact absurd rfl j_ne
  · rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
    have := (Classical.choose_spec (hg j₁)).2
    contradiction
  · rw [Fin.cons_succ, Fin.cons_zero, ← not_le] at approx
    have := (Classical.choose_spec (hg j₀)).2
    contradiction
  · rw [Fin.cons_succ, Fin.cons_succ] at approx
    rw [Ne.def, Fin.succ_inj] at j_ne
    have : j₀ = j₁ :=
      (Classical.choose_spec (hg j₀)).1.symm.trans
        (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans
          (Classical.choose_spec (hg j₁)).1)
    contradiction
      -- However, if one of those partitions `j` is inhabited by some `i`, then this `j` works.
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
by_contra hg
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg : ¬∃ j, ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
push_neg at hg
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
⊢ False
[PROOFSTEP]
obtain ⟨j₀, j₁, j_ne, approx⟩ :=
  exists_approx_polynomial hb hε (Fin.cons (A 0) fun j => A (Fin.succ (Classical.choose (hg j))))
[GOAL]
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j_ne : j₀ ≠ j₁
approx :
  ↑(↑cardPowDegree
        (Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              j₁ %
            b -
          Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              j₀ %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
revert j_ne approx
[GOAL]
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
⊢ j₀ ≠ j₁ →
    ↑(↑cardPowDegree
            (Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  j₁ %
                b -
              Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  j₀ %
                b)) <
        ↑cardPowDegree b • ε →
      False
[PROOFSTEP]
refine' Fin.cases _ (fun j₀ => _) j₀
[GOAL]
case intro.intro.intro.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
⊢ 0 ≠ j₁ →
    ↑(↑cardPowDegree
            (Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  j₁ %
                b -
              Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  0 %
                b)) <
        ↑cardPowDegree b • ε →
      False
[PROOFSTEP]
refine' Fin.cases (fun j_ne approx => _) (fun j₁ j_ne approx => _) j₁
[GOAL]
case intro.intro.intro.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
⊢ Fin.succ j₀ ≠ j₁ →
    ↑(↑cardPowDegree
            (Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  j₁ %
                b -
              Fin.cons (A 0)
                  (fun j =>
                    A
                      (Fin.succ
                        (Classical.choose
                          (_ :
                            ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
                  (Fin.succ j₀) %
                b)) <
        ↑cardPowDegree b • ε →
      False
[PROOFSTEP]
refine' Fin.cases (fun j_ne approx => _) (fun j₁ j_ne approx => _) j₁
[GOAL]
case intro.intro.intro.refine'_1.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j_ne : 0 ≠ 0
approx :
  ↑(↑cardPowDegree
        (Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              0 %
            b -
          Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              0 %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
exact absurd rfl j_ne
[GOAL]
case intro.intro.intro.refine'_1.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ Fin.succ j₁
approx :
  ↑(↑cardPowDegree
        (Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              (Fin.succ j₁) %
            b -
          Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              0 %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_zero, ← not_le, AbsoluteValue.map_sub] at approx
[GOAL]
case intro.intro.intro.refine'_1.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ Fin.succ j₁
approx :
  ¬↑cardPowDegree b • ε ≤
      ↑(↑cardPowDegree
          (A 0 % b -
            A
                (Fin.succ
                  (Classical.choose
                    (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
              b))
⊢ False
[PROOFSTEP]
have := (Classical.choose_spec (hg j₁)).2
[GOAL]
case intro.intro.intro.refine'_1.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ Fin.succ j₁
approx :
  ¬↑cardPowDegree b • ε ≤
      ↑(↑cardPowDegree
          (A 0 % b -
            A
                (Fin.succ
                  (Classical.choose
                    (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
              b))
this :
  ↑cardPowDegree b • ε ≤
    ↑(↑cardPowDegree
        (A 0 % b -
          A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b))
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.intro.refine'_2.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : Fin.succ j₀ ≠ 0
approx :
  ↑(↑cardPowDegree
        (Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              0 %
            b -
          Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              (Fin.succ j₀) %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_zero, ← not_le] at approx
[GOAL]
case intro.intro.intro.refine'_2.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : Fin.succ j₀ ≠ 0
approx :
  ¬↑cardPowDegree b • ε ≤
      ↑(↑cardPowDegree
          (A 0 % b -
            A
                (Fin.succ
                  (Classical.choose
                    (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
              b))
⊢ False
[PROOFSTEP]
have := (Classical.choose_spec (hg j₀)).2
[GOAL]
case intro.intro.intro.refine'_2.refine'_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : Fin.succ j₀ ≠ 0
approx :
  ¬↑cardPowDegree b • ε ≤
      ↑(↑cardPowDegree
          (A 0 % b -
            A
                (Fin.succ
                  (Classical.choose
                    (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
              b))
this :
  ↑cardPowDegree b • ε ≤
    ↑(↑cardPowDegree
        (A 0 % b -
          A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b))
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
case intro.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : Fin.succ j₀ ≠ Fin.succ j₁
approx :
  ↑(↑cardPowDegree
        (Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              (Fin.succ j₁) %
            b -
          Fin.cons (A 0)
              (fun j =>
                A
                  (Fin.succ
                    (Classical.choose
                      (_ : ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))))
              (Fin.succ j₀) %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
rw [Fin.cons_succ, Fin.cons_succ] at approx
[GOAL]
case intro.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : Fin.succ j₀ ≠ Fin.succ j₁
approx :
  ↑(↑cardPowDegree
        (A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b -
          A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
rw [Ne.def, Fin.succ_inj] at j_ne
[GOAL]
case intro.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : ¬j₀ = j₁
approx :
  ↑(↑cardPowDegree
        (A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b -
          A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b)) <
    ↑cardPowDegree b • ε
⊢ False
[PROOFSTEP]
have : j₀ = j₁ :=
  (Classical.choose_spec (hg j₀)).1.symm.trans
    (((ht' (Classical.choose (hg j₀)) (Classical.choose (hg j₁))).mpr approx).trans (Classical.choose_spec (hg j₁)).1)
[GOAL]
case intro.intro.intro.refine'_2.refine'_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)),
    ∃ i, t' i = j ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))
j₀✝ j₁✝ : Fin (Nat.succ (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : ¬j₀ = j₁
approx :
  ↑(↑cardPowDegree
        (A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₁ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b -
          A
              (Fin.succ
                (Classical.choose
                  (_ : ∃ i, t' i = j₀ ∧ ↑cardPowDegree b • ε ≤ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b))))) %
            b)) <
    ↑cardPowDegree b • ε
this : j₀ = j₁
⊢ False
[PROOFSTEP]
contradiction
  -- However, if one of those partitions `j` is inhabited by some `i`, then this `j` works.
[GOAL]
case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
by_cases exists_nonempty_j :
  ∃ j, (∃ i, t' i = j) ∧ ∀ i, t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε
[GOAL]
case pos
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
exists_nonempty_j :
  ∃ j,
    (∃ i, t' i = j) ∧ ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
obtain ⟨j, ⟨i, hi⟩, hj⟩ := exists_nonempty_j
[GOAL]
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : t' i = j
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' ⟨j, fun i' => ⟨hj i', fun hi' => _root_.trans ((ht' _ _).mpr _) hi⟩⟩
[GOAL]
case pos.intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i') % b)) < ↑cardPowDegree b • ε
⊢ ↑(↑cardPowDegree (Fin.tail A i % b - Fin.tail A i' % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
apply anti_archim' _ hi'
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i') % b)) < ↑cardPowDegree b • ε
⊢ ↑(↑cardPowDegree (A (Fin.succ i) % b - A 0 % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
rw [AbsoluteValue.map_sub]
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj✝ : ∀ (i : Fin n), t' i = j✝ → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : t' i = j
i' : Fin n
hi' : ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i') % b)) < ↑cardPowDegree b • ε
⊢ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
exact hj _ hi
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
exists_nonempty_j :
  ¬∃ j,
      (∃ i, t' i = j) ∧
        ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ ∃ j, ∀ (i : Fin n), t' i = j ↔ ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
refine' ⟨j, fun i => ⟨hj i, fun hi => _⟩⟩
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
exists_nonempty_j :
  ¬∃ j,
      (∃ i, t' i = j) ∧
        ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
⊢ t' i = j
[PROOFSTEP]
have := exists_nonempty_j ⟨t' i, ⟨i, rfl⟩, fun i' hi' => anti_archim' hi ((ht' _ _).mp hi')⟩
[GOAL]
case neg
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n✝ : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A✝ : Fin n✝ → Fq[X]
hbε : 0 < ↑cardPowDegree b • ε
n : ℕ
ih :
  ∀ (A : Fin n → Fq[X]),
    ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
A : Fin (Nat.succ n) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (Nat.succ n)} {ε : ℝ},
    ↑(↑cardPowDegree (A i % b - A j % b)) < ε →
      ↑(↑cardPowDegree (A j % b - A k % b)) < ε → ↑(↑cardPowDegree (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 (Fin.tail A i₁ % b - Fin.tail A i₀ % b)) < ↑cardPowDegree b • ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
hj : ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
exists_nonempty_j :
  ¬∃ j,
      (∃ i, t' i = j) ∧
        ∀ (i : Fin n), t' i = j → ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
i : Fin n
hi : ↑(↑cardPowDegree (A 0 % b - A (Fin.succ i) % b)) < ↑cardPowDegree b • ε
this : False
⊢ t' i = j
[PROOFSTEP]
contradiction
[GOAL]
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A
[GOAL]
case intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : 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)⌉₊)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ ↔ ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(↑cardPowDegree (A i₁ % b - A i₀ % b)) < ↑cardPowDegree b • ε
[PROOFSTEP]
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩