-- Mathlib/NumberTheory/ClassNumber/AdmissibleCardPowDegree.lean
theorem exists_partition_polynomial_aux (n : ℕ) {ε : ℝ} (hε : 0 < ε) {b : Fq[X]} (hb : b ≠ 0)
    (A : Fin n → Fq[X]) : ∃ t : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (Fintype.card Fq)⌉₊),
      ∀ i₀ i₁ : Fin n, t i₀ = t i₁ ↔
        (cardPowDegree (A i₁ % b - A i₀ % b) : ℝ) < cardPowDegree b • ε

Proof state:
case intro.intro.intro
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
⊢ j₀ ≠ j₁ →
    ↑(cardPowDegree
            (Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₁ % b -
              Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₀ % b)) <
        cardPowDegree b • ε →
      False

Tactic:
refine Fin.cases ?_ (fun j₀ => ?_) j₀ <;>
  refine Fin.cases (fun j_ne approx => ?_) (fun j₁ j_ne approx => ?_) j₁

Result:
case intro.intro.intro.refine_1.refine_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b))
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j_ne : 0 ≠ 0
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) 0 % b -
          Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) 0 % b)) <
    cardPowDegree b • ε
⊢ False

case intro.intro.intro.refine_1.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b))
j₀ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : 0 ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) 0 % b)) <
    cardPowDegree b • ε
⊢ False

case intro.intro.intro.refine_2.refine_1
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b))
j₀✝ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ 0
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) 0 % b -
          Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₀.succ % b)) <
    cardPowDegree b • ε
⊢ False

case intro.intro.intro.refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b))
j₀✝ j₁✝ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊).succ
j₀ j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log ↑(Fintype.card Fq)⌉₊)
j_ne : j₀.succ ≠ j₁.succ
approx :
  ↑(cardPowDegree
        (Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₁.succ % b -
          Fin.cons (A 0) (fun j => A (Classical.choose ⋯).succ) j₀.succ % b)) <
    cardPowDegree b • ε
⊢ False

Proof state:
case succ.intro.intro.refine_2.refine_2
Fq : Type u_1
inst✝¹ : Fintype Fq
inst✝ : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
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 (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    ↑(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 i.succ % b)) < cardPowDegree b • ε
i₀✝ i₁✝ : Fin (n + 1)
i₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔ ↑(cardPowDegree (A i₁.succ % b - A i₀.succ % b)) < cardPowDegree b • ε

Tactic:
exact ht' i₀ i₁

Result:
no goals