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_1 : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj_1 :
  ∀ (i : Fin n),
    t' i = j_1 →
      (↑((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) : ℝ)⌉₊)
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 : Fin n
hi : t' i = j
i' : Fin n
hi' :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i'.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
rw :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A i.succ % b - A 0 % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
rw [AbsoluteValue.map_sub]

Premises used: AbsoluteValue.map_sub
-- 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_1 : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj_1 :
  ∀ (i : Fin n),
    t' i = j_1 →
      (↑((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) : ℝ)⌉₊)
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 : Fin n
hi : t' i = j
i' : Fin n
hi' :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i'.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
hj _ hi
-- 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_1 : Fin (Fintype.card Fq ^ ⌈-log ε / log (↑(Fintype.card Fq) : ℝ)⌉₊)
hj_1 :
  ∀ (i : Fin n),
    t' i = j_1 →
      (↑((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) : ℝ)⌉₊)
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 : Fin n
hi : t' i = j
i' : Fin n
hi' :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i'.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε

Tactic:
exact hj _ hi
-- 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 : ℤ) ε
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 : ℤ) ε

Tactic:
⟨j, fun i => ⟨hj i, fun hi => ?_⟩⟩

Premises used: Iff.intro, Exists.intro
-- 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 : ℤ) ε
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 : ℤ) ε
neg :
  ∀ (i : Fin n)
    (hi :
      (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    t' i = j
⊢ ∃ (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:
refine ⟨j, fun i => ⟨hj i, fun hi => ?_⟩⟩
-- 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 : ℤ) ε
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 : ℤ) ε
i : Fin n
hi :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ False

Tactic:
have := exists_nonempty_j ⟨t' i, ⟨i, rfl⟩, fun i' hi' => anti_archim' hi ((ht' _ _).mp hi')⟩
-- 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 : ℤ) ε
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 : ℤ) ε
i : Fin n
hi :
  (↑((cardPowDegree : (a : Fq[X]) → ℤ) (A 0 % b - A i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
this : False
⊢ t' i = j

Tactic:
contradiction
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Field Fq
n : ℕ
ε : ℝ
hε : 0 < ε
b : Fq[X]
hb : b ≠ 0
A : Fin n → Fq[X]
obtain :
  ∀ (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]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
            HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε),
    ∃ (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 : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
obtain ⟨t, ht⟩ := exists_partition_polynomial_aux n hε hb A

Premises used: Polynomial.exists_partition_polynomial_aux
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : 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 : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩

Premises used: Exists.intro, Iff.mp
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : 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 : Fq[X]) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((cardPowDegree : (a : Fq[X]) → ℤ) b : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
exact ⟨t, fun i₀ i₁ hi => (ht i₀ i₁).mp hi⟩
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
by_contra! :
  ∀
    (h :
      ∀ (i j k : ι),
        Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R)
          (0 : R)),
    False
⊢ ∃ (i : ι) (j : ι) (k : ι),
    Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)

Tactic:
by_contra! h
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
obtain : ∀ (i : ι), False
⊢ False

Tactic:
obtain ⟨i⟩ := bS.index_nonempty

Premises used: Module.Basis.index_nonempty
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
apply : Eq.{u_2 + 1} (α := S) ((bS : (a : ι) → S) i : S) (0 : S)
⊢ False

Tactic:
apply bS.ne_zero i

Premises used: Module.Basis.ne_zero
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
a :
  Eq (α := Matrix ι ι R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) : Matrix ι ι R)
    (0 : Matrix ι ι R)
⊢ Eq.{u_2 + 1} (α := S) ((bS : (a : ι) → S) i : S) (0 : S)

Tactic:
apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)

Premises used: Algebra.leftMulMatrix_injective, Algebra.leftMulMatrix, injective_iff_map_eq_zero, Iff.mp
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i : ι
a :
  ∀ (j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R)
      (0 j k : R)
⊢ Eq (α := Matrix ι ι R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) : Matrix ι ι R)
    (0 : Matrix ι ι R)

Tactic:
ext j k
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
h :
  ∀ (i j k : ι),
    Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
i j k : ι
⊢ Eq.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 j k : R)

Tactic:
simp [h]
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
obtain :
  ∀ (i j k : ι)
    (hijk :
      Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R)
        (0 : R)),
    0 < normBound abv bS
⊢ 0 < normBound abv bS

Tactic:
obtain ⟨i, j, k, hijk⟩ : ∃ i j k, Algebra.leftMulMatrix bS (bS i) j k ≠ 0 := by
    by_contra! h
    obtain ⟨i⟩ := bS.index_nonempty
    apply bS.ne_zero i
    apply
      (injective_iff_map_eq_zero (Algebra.leftMulMatrix bS)).mp (Algebra.leftMulMatrix_injective bS)
    ext j k
    simp [h]
-- Module: Mathlib.NumberTheory.ClassNumber.Finite
Goal:
R : Type u_1
S : Type u_2
inst : EuclideanDomain R
inst_1 : CommRing S
inst_2 : IsDomain S
inst_3 : Algebra R S
abv : AbsoluteValue R ℤ
ι : Type u_5
inst_4 : DecidableEq ι
inst_5 : Fintype ι
bS : Basis ι R S
i j k : ι
hijk :
  Ne.{u_1 + 1} (α := R) ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) i) j k : R) (0 : R)
apply :
  0 <
    ((↑(Fintype.card ι) : ℤ) *
        Finset.max'
          (Finset.image
            (fun (ijk : ι × ι × ι) ↦
              (abv : (a : R) → ℤ)
                ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
            Finset.univ)
          ⋯) ^
      Fintype.card ι
⊢ 0 <
    (↑(Fintype.card ι).factorial : ℤ) *
      ((↑(Fintype.card ι) : ℤ) *
          Finset.max'
            (Finset.image
              (fun (ijk : ι × ι × ι) ↦
                (abv : (a : R) → ℤ)
                  ((Algebra.leftMulMatrix bS : (a : S) → Matrix ι ι R) ((bS : (a : ι) → S) ijk.1) ijk.2.1 ijk.2.2 : R))
              Finset.univ)
            ⋯) ^
        Fintype.card ι

Tactic:
apply mul_pos (Int.natCast_pos.mpr (Nat.factorial_pos _))

Premises used: Iff.mpr, mul_pos, Nat.factorial_pos, Int.natCast_pos