-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
hbε : 0 < HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
n : ℕ
ih :
  ∀ (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 : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
A : Fin (n + 1) → Fq[X]
anti_archim' :
  ∀ {i j k : Fin (n + 1)} {ε : ℝ},
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A j % b)) : ℝ) < ε →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A j % b - A k % b)) : ℝ) < ε →
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i % b - A k % b)) : ℝ) < ε
t' : Fin n → Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
ht' :
  ∀ (i₀ i₁ : Fin n),
    t' i₀ = t' i₁ ↔
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₁ % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ Fq[X]) A i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj :
  ∀ (i : Fin n),
    t' i = j →
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
pos :
  ∀
    (exists_nonempty_j :
      ∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
        (∃ (i : Fin n), t' i = j) ∧
          ∀ (i : Fin n),
            t' i = j →
              (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
                HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    ∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i : Fin n),
        t' i = j ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
neg :
  ∀
    (exists_nonempty_j :
      ¬∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
          (∃ (i : Fin n), t' i = j) ∧
            ∀ (i : Fin n),
              t' i = j →
                (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
                  HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    ∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
      ∀ (i : Fin n),
        t' i = j ↔
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∀ (i : Fin n),
      t' i = j ↔
        (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
by_cases exists_nonempty_j : ∃ j, (∃ i, t' i = j) ∧
      ∀ i, t' i = j → (cardPowDegree (A 0 % b - A i.succ % b) : ℝ) < cardPowDegree b • ε

Premises used: Exists, Eq