awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ℤ) ε
i₀ i₁_1 : Fin (n + 1)
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:
exact hj i₁
-- 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 : ℤ) ε
i₀_1 i₁ : Fin (n + 1)
i₀ : Fin n
succ :
  t' i₀ = j ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ Eq (α := Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) j t'
          i₀.succ :
        Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) j t' 0 :
        Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rw [Fin.cons_succ, Fin.cons_zero]

Premises used: Fin.cons_succ, Fin.cons_zero
-- 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 : ℤ) ε
i₀_1 i₁ : Fin (n + 1)
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:
hj i₀
-- 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 : ℤ) ε
i₀_1 i₁ : Fin (n + 1)
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:
exact hj i₀
-- 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 : ℤ) ε
i₀_1 i₁_1 : Fin (n + 1)
i₀ i₁ : Fin n
succ :
  t' i₀ = t' i₁ ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁.succ % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ Eq (α := Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) j t'
          i₀.succ :
        Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊))
      (Fin.cons (α := fun (a : Fin (n + 1)) ↦ Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) j t'
          i₁.succ :
        Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)) ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁.succ % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rw [Fin.cons_succ, Fin.cons_succ]

Premises used: Fin.cons_succ
-- 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 : ℤ) ε
i₀_1 i₁_1 : Fin (n + 1)
i₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁.succ % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
ht' i₀ i₁

Premises used: Fin.tail
-- 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 : ℤ) ε
i₀_1 i₁_1 : Fin (n + 1)
i₀ i₁ : Fin n
⊢ t' i₀ = t' i₁ ↔
    (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i₁.succ % b - A i₀.succ % b)) : ℝ) <
      HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
exact ht' i₀ i₁
-- 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 : ℤ) ε
by_contra! :
  ∀
    (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)) : ℝ)),
    False
⊢ ∃ (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_contra! hg
-- 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 : ℤ) ε
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₀ j₁_1 : 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 :
  ¬HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
            (A 0 % b -
              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 %
                b)) :
        ℝ)
⊢ HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
    (↑((cardPowDegree : (a : Fq[X]) → ℤ)
          (A 0 % b -
            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 %
              b)) :
      ℝ)

Tactic:
have := (Classical.choose_spec (hg j₁)).2
-- 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 : ℤ) ε
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₀ j₁_1 : 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 :
  ¬HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
            (A 0 % b -
              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 %
                b)) :
        ℝ)
this :
  HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
    (↑((cardPowDegree : (a : Fq[X]) → ℤ)
          (A 0 % b -
            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 %
              b)) :
      ℝ)
⊢ False

Tactic:
contradiction
-- 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 : ℤ) ε
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) : ℝ)⌉₊)
j_ne : j₀.succ ≠ 0
approx :
  ¬HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
      (↑((cardPowDegree : (a : Fq[X]) → ℤ)
            (A 0 % b -
              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 %
                b)) :
        ℝ)
⊢ HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε ≤
    (↑((cardPowDegree : (a : Fq[X]) → ℤ)
          (A 0 % b -
            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 %
              b)) :
      ℝ)

Tactic:
have := (Classical.choose_spec (hg j₀)).2