awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this_1 : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht :
  ∀ (i₀ i₁ : Fin (M ^ n.succ).succ),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) (A i₁ 0 % b - A i₀ 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
s : Fin M
hs : M ^ n < Finset.card (α := Fin (M ^ n.succ).succ) {x : Fin (M ^ n.succ).succ | t x = s}
this : (M ^ n).succ ≤ List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s})
refine_1 :
  ∀ (i j : Fin (M ^ n).succ)
    (h :
      Eq (α := Fin (M ^ n.succ).succ)
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          i)
        ((fun (i : Fin (M ^ n).succ) ↦
            getElem (valid :=
              fun (xs : List (Fin (M ^ n.succ).succ))
                (i :
                  Fin
                    (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
              (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
          j)),
    i = j
⊢ ∃ (s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ),
    Function.Injective s ∧
      ∀ (i₀ i₁ : Fin (M ^ n).succ),
        (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) <
          HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have refine_2 : ∀ (i₀ i₁ : Fin (M ^ n).succ),
  t
      ((fun (i : Fin (M ^ n).succ) ↦
          getElem (valid :=
            fun (xs : List (Fin (M ^ n.succ).succ))
              (i :
                Fin (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
            (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) sorry)
        i₀) =
    t
      ((fun (i : Fin (M ^ n).succ) ↦
          getElem (valid :=
            fun (xs : List (Fin (M ^ n.succ).succ))
              (i :
                Fin (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
            (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) sorry)
        i₁)
Tactic: refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (hypothesis)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this_1 : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
t : Fin (M ^ n.succ).succ → Fin M
ht :
  ∀ (i₀ i₁ : Fin (M ^ n.succ).succ),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) (A i₁ 0 % b - A i₀ 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
s : Fin M
hs : M ^ n < Finset.card (α := Fin (M ^ n.succ).succ) {x : Fin (M ^ n.succ).succ | t x = s}
this : (M ^ n).succ ≤ List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s})
i₀ i₁ : Fin (M ^ n).succ
⊢ t
      ((fun (i : Fin (M ^ n).succ) ↦
          getElem (valid :=
            fun (xs : List (Fin (M ^ n.succ).succ))
              (i :
                Fin (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
            (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
        i₀) =
    t
      ((fun (i : Fin (M ^ n).succ) ↦
          getElem (valid :=
            fun (xs : List (Fin (M ^ n.succ).succ))
              (i :
                Fin (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
            (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) ⋯)
        i₁)
have this₁ : ∀ (i : Fin (M ^ n).succ),
  t
      (getElem (valid :=
        fun (xs : List (Fin (M ^ n.succ).succ))
          (i : Fin (List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}))) ↦
        (↑i : ℕ) < xs.length) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s}) (Fin.castLE this i) sorry) =
    s
Tactic: have (i : Fin (M ^ n).succ) : t (Finset.toList {x | t x = s})[i.castLE this] = s :=
        (Finset.mem_filter.mp ((Finset.mem_toList (s := {x | t x = s})).mp (List.getElem_mem _))).2
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
⊢ ∃ (i₀ : Fin (h.card ε ^ (n + 1)).succ) (i₁ : Fin (h.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have succ : ∀ (s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ) (s_inj : Function.Injective s)
  (hs :
    ∀ (i₀ i₁ : Fin (M ^ n).succ),
      (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε),
  ∃ (i₀ : Fin (h.card ε ^ (n + 1)).succ) (i₁ : Fin (h.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: obtain ⟨s, s_inj, hs⟩ :
    ∃ s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ,
      Function.Injective s ∧ ∀ i₀ i₁, (abv (A (s i₁) 0 % b - A (s i₀) 0 % b) : ℝ) < abv b • ε := by
    -- We can partition the `A`s into `M` subsets where
    -- the first components lie close together:
    obtain ⟨t, ht⟩ :
      ∃ t : Fin (M ^ n.succ).succ → Fin M,
        ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ 0 % b - A i₀ 0 % b) : ℝ) < abv b • ε :=
      h.exists_partition hε hb fun x ↦ A x 0
    -- Since the `M` subsets contain more than `M * M^n` elements total,
    -- there must be a subset that contains more than `M^n` elements.
    obtain ⟨s, hs⟩ :=
      Fintype.exists_lt_card_fiber_of_mul_lt_card (f := t)
        (by simpa only [Fintype.card_fin, pow_succ'] using Nat.lt_succ_self (M ^ n.succ))
    have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]
    refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩
    · simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h
    · have (i : Fin (M ^ n).succ) : t (Finset.toList {x | t x = s})[i.castLE this] = s :=
        (Finset.mem_filter.mp ((Finset.mem_toList (s := {x | t x = s})).mp (List.getElem_mem _))).2
      simp_rw [this]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs :
  ∀ (i₀ i₁ : Fin (M ^ n).succ),
    (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (i₀ : Fin (h.card ε ^ (n + 1)).succ) (i₁ : Fin (h.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have succ : ∀ (k₀ k₁ : Fin (h.card ε ^ n).succ) (hk : k₀ ≠ k₁)
  (h_1 :
    ∀ (k : Fin n),
      (↑((abv : (a : R) → ℤ)
              (Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₁)) k % b -
                Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₀)) k % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε),
  ∃ (i₀ : Fin (h.card ε ^ (n + 1)).succ) (i₁ : Fin (h.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h_1 : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h_1.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h_1.card ε ^ n).succ) (i₁ : Fin (h_1.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h_1.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h_1.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs :
  ∀ (i₀ i₁ : Fin (M ^ n).succ),
    (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
k₀ k₁ : Fin (h_1.card ε ^ n).succ
hk : k₀ ≠ k₁
h :
  ∀ (k : Fin n),
    (↑((abv : (a : R) → ℤ)
            (Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₁)) k % b -
              Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₀)) k % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (i₀ : Fin (h_1.card ε ^ (n + 1)).succ) (i₁ : Fin (h_1.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have succ : ∀ (i : Fin (n + 1)),
  (↑((abv : (a : R) → ℤ) (A (s k₁) 0 % b - A (s k₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h_1 : abv.IsAdmissible
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h_1.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h_1.card ε ^ n).succ) (i₁ : Fin (h_1.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (h_1.card ε ^ (n + 1)).succ → Fin (n + 1) → R
M : ℕ := h_1.card ε
s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ
s_inj : Function.Injective s
hs :
  ∀ (i₀ i₁ : Fin (M ^ n).succ),
    (↑((abv : (a : R) → ℤ) (A (s i₁) 0 % b - A (s i₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
k₀ k₁ : Fin (h_1.card ε ^ n).succ
hk : k₀ ≠ k₁
h :
  ∀ (k : Fin n),
    (↑((abv : (a : R) → ℤ)
            (Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₁)) k % b -
              Fin.tail (α := fun (i : Fin (n + 1)) ↦ R) (A (s k₀)) k % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
succ :
  ∀ (i : Fin (n + 1)),
    (↑((abv : (a : R) → ℤ) (A (s k₁) 0 % b - A (s k₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (i₀ : Fin (h_1.card ε ^ (n + 1)).succ) (i₁ : Fin (h_1.card ε ^ (n + 1)).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin (n + 1)),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have succ₁ : ∀ (i : Fin (n + 1)) (i : Fin n),
  (↑((abv : (a : R) → ℤ) (A (s k₁) i.succ % b - A (s k₀) i.succ % b)) : ℝ) <
    HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
n : ℕ
h : abv.IsAdmissible
this : DecidableEq R
⊢ ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (h.card ε ^ n).succ → Fin n → R),
    ∃ (i₀ : Fin (h.card ε ^ n).succ) (i₁ : Fin (h.card ε ^ n).succ),
      i₀ ≠ i₁ ∧
        ∀ (k : Fin n),
          (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have zero : ∀ {ε : ℝ} (_hε : 0 < ε) {b : R} (_hb : b ≠ 0) (A : Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ → Fin 0 → R),
  ∃ (i₀ : Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ) (i₁ : Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : Fin 0),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: induction n with
  | zero =>
    intro ε _hε b _hb A
    refine ⟨0, 1, ?_, ?_⟩
    · simp
    rintro ⟨i, ⟨⟩⟩
  | succ n ih =>
  intro ε hε b hb A
  let M := h.card ε
  -- By the "nicer" pigeonhole principle, we can find a collection `s`
  -- of more than `M ^ n` remainders where the first components lie close together:
  obtain ⟨s, s_inj, hs⟩ :
    ∃ s : Fin (M ^ n).succ → Fin (M ^ n.succ).succ,
      Function.Injective s ∧ ∀ i₀ i₁, (abv (A (s i₁) 0 % b - A (s i₀) 0 % b) : ℝ) < abv b • ε := by
    -- We can partition the `A`s into `M` subsets where
    -- the first components lie close together:
    obtain ⟨t, ht⟩ :
      ∃ t : Fin (M ^ n.succ).succ → Fin M,
        ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ 0 % b - A i₀ 0 % b) : ℝ) < abv b • ε :=
      h.exists_partition hε hb fun x ↦ A x 0
    -- Since the `M` subsets contain more than `M * M^n` elements total,
    -- there must be a subset that contains more than `M^n` elements.
    obtain ⟨s, hs⟩ :=
      Fintype.exists_lt_card_fiber_of_mul_lt_card (f := t)
        (by simpa only [Fintype.card_fin, pow_succ'] using Nat.lt_succ_self (M ^ n.succ))
    have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]
    refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩
    · simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h
    · have (i : Fin (M ^ n).succ) : t (Finset.toList {x | t x = s})[i.castLE this] = s :=
        (Finset.mem_filter.mp ((Finset.mem_toList (s := {x | t x = s})).mp (List.getElem_mem _))).2
      simp_rw [this]
  -- Since `s` is large enough, there are two elements of `A ∘ s`
  -- where the second components lie close together.
  obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))
  refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
  · exact hs k₀ k₁
  · exact h i
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst_1 : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : abv.IsAdmissible
A : Fin (h.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ (i₀ : Fin (h.card ε ^ Fintype.card ι).succ) (i₁ : Fin (h.card ε ^ Fintype.card ι).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : ι),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have obtain : ∀ (i₀ i₁ : Fin (h.card ε ^ Fintype.card ι).succ) (ne : i₀ ≠ i₁)
  (h_1 :
    ∀ (k : Fin (Fintype.card ι)),
      (↑((abv : (a : R) → ℤ)
              (A i₁ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b -
                A i₀ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε),
  ∃ (i₀ : Fin (h.card ε ^ Fintype.card ι).succ) (i₁ : Fin (h.card ε ^ Fintype.card ι).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : ι),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: obtain ⟨i₀, i₁, ne, h⟩ := h.exists_approx_aux (Fintype.card ι) hε hb fun x y ↦ A x (e.symm y)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst_1 : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h_1 : abv.IsAdmissible
A : Fin (h_1.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h_1.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h :
  ∀ (k : Fin (Fintype.card ι)),
    (↑((abv : (a : R) → ℤ)
            (A i₁ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b -
              A i₀ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (i₀ : Fin (h_1.card ε ^ Fintype.card ι).succ) (i₁ : Fin (h_1.card ε ^ Fintype.card ι).succ),
    i₀ ≠ i₁ ∧
      ∀ (k : ι),
        (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have refine : ∀ (k : ι), (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: refine ⟨i₀, i₁, ne, fun k ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue (goal)
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst_1 : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h_1 : abv.IsAdmissible
A : Fin (h_1.card ε ^ Fintype.card ι).succ → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (h_1.card ε ^ Fintype.card ι).succ
ne : i₀ ≠ i₁
h :
  ∀ (k : Fin (Fintype.card ι)),
    (↑((abv : (a : R) → ℤ)
            (A i₁ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b -
              A i₀ ((e.symm : (a : Fin (Fintype.card ι)) → ι) k) % b)) :
        ℝ) <
      HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
k : ι
⊢ (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have h₁ : k = (e.symm : (a : Fin (Fintype.card ι)) → ι) ((e : (a : ι) → Fin (Fintype.card ι)) k : Fin (Fintype.card ι))
Tactic: convert! h (e k)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (hypothesis)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀
have this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
Tactic: have : Fintype.card (Fin d → Fq) < Fintype.card (Fin m.succ) := by
    simpa using lt_of_le_of_lt hm (Nat.lt_succ_self m)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀
have obtain : ∀ (i₀ i₁ : Fin m.succ) (i_ne : i₀ ≠ i₁) (i_eq : f i₀ = f i₁),
  ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀
Tactic: obtain ⟨i₀, i₁, i_ne, i_eq⟩ := Fintype.exists_ne_map_eq_of_card_lt f this
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ ∃ (i₀ : Fin m.succ) (i₁ : Fin m.succ), i₀ ≠ i₁ ∧ A i₁ = A i₀
have right : A i₁ = A i₀
Tactic: use i₀, i₁, i_ne
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
⊢ A i₁ = A i₀
have right : ∀ (j : ℕ), (A i₁).coeff j = (A i₀).coeff j
Tactic: ext j
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
⊢ (A i₁).coeff j = (A i₀).coeff j
have pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁).coeff j = (A i₀).coeff j
Tactic: by_cases! hbj : degree b ≤ j
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
pos : ∀ (hbj : b.degree ≤ (↑j : WithBot ℕ)), (A i₁).coeff j = (A i₀).coeff j
⊢ (A i₁).coeff j = (A i₀).coeff j
have neg : ∀ (hbj : (↑j : WithBot ℕ) < b.degree), (A i₁).coeff j = (A i₀).coeff j
Tactic: by_cases! hbj : degree b ≤ j
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleCardPowDegree (goal)
Goal:
Fq : Type u_1
inst : Fintype Fq
inst_1 : Semiring Fq
d m : ℕ
hm : Fintype.card Fq ^ d ≤ m
b : Fq[X]
hb : b.natDegree ≤ d
A : Fin m.succ → Fq[X]
hA : ∀ (i : Fin m.succ), (A i).degree < b.degree
f : Fin m.succ → Fin d → Fq := fun (i : Fin m.succ) (j : Fin d) ↦ (A i).coeff (↑j : ℕ)
this : Fintype.card.{u_1} (Fin d → Fq) < Fintype.card (Fin m.succ)
i₀ i₁ : Fin m.succ
i_ne : i₀ ≠ i₁
i_eq : f i₀ = f i₁
j : ℕ
hbj : b.degree ≤ (↑j : WithBot ℕ)
⊢ (A i₁).coeff j = (A i₀).coeff j
have pos : 0 = (A i₀).coeff j
Tactic: rw [coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj),
      coeff_eq_zero_of_degree_lt (lt_of_lt_of_le (hA _) hbj)]