-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
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 : ℤ) ε
hg :
  ∀ (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)),
    ∃ (i : Fin n),
      t' i = j ∧
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
          (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ)
j₀_1 j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ
j₀ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
refine_2 :
  ∀ (j_ne : j₀.succ ≠ 0)
    (approx :
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (HMod.hMod (α := Fq[X])
                  (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦
                      Fq[X]) (A 0)
                      (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                        A
                          (Classical.choose (p := fun (x : Fin n) ↦
                              t' x = j ∧
                                HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                              ⋯).succ)
                      0 :
                    Fq[X])
                  b -
                HMod.hMod (α := Fq[X])
                  (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦
                      Fq[X]) (A 0)
                      (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                        A
                          (Classical.choose (p := fun (x : Fin n) ↦
                              t' x = j ∧
                                HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                              ⋯).succ)
                      j₀.succ :
                    Fq[X])
                  b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    False
⊢ ∀ (j_ne : j₀.succ ≠ j₁)
    (approx :
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
              (HMod.hMod (α := Fq[X])
                  (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦
                      Fq[X]) (A 0)
                      (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                        A
                          (Classical.choose (p := fun (x : Fin n) ↦
                              t' x = j ∧
                                HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                              ⋯).succ)
                      j₁ :
                    Fq[X])
                  b -
                HMod.hMod (α := Fq[X])
                  (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦
                      Fq[X]) (A 0)
                      (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                        A
                          (Classical.choose (p := fun (x : Fin n) ↦
                              t' x = j ∧
                                HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                              ⋯).succ)
                      j₀.succ :
                    Fq[X])
                  b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    False
have refine_2₁ : ∀ (j₁ : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) (j_ne : j₀.succ ≠ j₁.succ)
  (approx :
    (↑((cardPowDegree : (a : Fq[X]) → ℤ)
            (HMod.hMod (α := Fq[X])
                (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦ Fq[X])
                    (A 0)
                    (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                      A
                        (Classical.choose (p := fun (x : Fin n) ↦
                            t' x = j ∧
                              HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                            sorry).succ)
                    j₁.succ :
                  Fq[X])
                b -
              HMod.hMod (α := Fq[X])
                (Fin.cons (α := fun (a : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊).succ) ↦ Fq[X])
                    (A 0)
                    (fun (j : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↦
                      A
                        (Classical.choose (p := fun (x : Fin n) ↦
                            t' x = j ∧
                              HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
                                (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A x.succ % b)) : ℝ))
                            sorry).succ)
                    j₀.succ :
                  Fq[X])
                b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
  False
Tactic: refine Fin.cases (fun j_ne approx => ?_) (fun j₁ j_ne approx => ?_) j₁