awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have refine_1 : ∀ (i : Fin n), ⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊
Tactic: refine ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
refine_1 : ∀ (i : Fin n), ⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have refine_2 : ∀ (i₀ i₁ : Fin n),
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, sorry⟩ : Fin ⌈1 / ε⌉₊)) i₀)
      ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, sorry⟩ : Fin ⌈1 / ε⌉₊)) i₁) →
    (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
Tactic: refine ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊
have refine_1 : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < (↑(↑⌈1 / ε⌉₊ : ℤ) : ℝ)
Tactic: rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt, Algebra.smul_def, eq_intCast, ← div_div]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < (↑(↑⌈1 / ε⌉₊ : ℤ) : ℝ)
have apply : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < 1 / ε
Tactic: apply lt_of_lt_of_le _ (Nat.le_ceil _)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < 1 / ε
have h : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) < 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) < 1
have h : A i % b < |b|
Tactic: rw [div_lt_one hb', cast_lt]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i₀ i₁ : Fin n
hi :
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
    ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁)
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hi₁ : Eq (α := ℤ) (↑⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋.natAbs : ℤ) (↑⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋.natAbs : ℤ)
Tactic: have hi : (⌊↑(A i₀ % b) / abs b • ε⌋.natAbs : ℤ) = ⌊↑(A i₁ % b) / abs b • ε⌋.natAbs :=
    congr_arg ((↑) : ℕ → ℤ) (Fin.mk_eq_mk.mp hi)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i₀ i₁ : Fin n
hi_1 :
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
    ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁)
hi : Eq (α := ℤ) (↑⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋.natAbs : ℤ) (↑⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋.natAbs : ℤ)
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hi₁ : ⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋ = ⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋
Tactic: rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i₀ i₁ : Fin n
hi_1 :
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
    ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁)
hi : ⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋ = ⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hi₁ : |(↑(A i₀ % b) : ℝ) / |b| • ε - (↑(A i₁ % b) : ℝ) / |b| • ε| < 1
Tactic: have hi := abs_sub_lt_one_of_floor_eq_floor hi
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i₀ i₁ : Fin n
hi_1 :
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
    ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁)
hi_2 : ⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋ = ⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋
hi : |(↑(A i₀ % b) : ℝ) / |b| • ε - (↑(A i₁ % b) : ℝ) / |b| • ε| < 1
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hi₁ : |HSub.hSub (α := ℝ) (↑(A i₁ % b) : ℝ) (↑(A i₀ % b) : ℝ)| < |b| • ε
Tactic: rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff₀ hbε, one_mul] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i₀ i₁ : Fin n
hi_1 :
  Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
    ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁)
hi_2 : ⌊(↑(A i₀ % b) : ℝ) / |b| • ε⌋ = ⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋
hi : |HSub.hSub (α := ℝ) (↑(A i₁ % b) : ℝ) (↑(A i₀ % b) : ℝ)| < |b| • ε
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have refine_2 : |(↑(A i₁ % b - A i₀ % b) : ℝ)| < |b| • ε
Tactic: rwa [Int.cast_abs, Int.cast_sub]
-- 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 : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
⊢ ∃ (t : ι → Fin (h.card ε)),
    ∀ (i₀ i₁ : ι),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have rcases : ∀ (n : ℕ) (e : ι ≃ Fin n),
  ∃ (t : ι → Fin (h.card ε)),
    ∀ (i₀ i₁ : ι),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩
-- 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 : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
⊢ ∃ (t : ι → Fin (h.card ε)),
    ∀ (i₀ i₁ : ι),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have obtain : ∀ (t : Fin n → Fin (h.card ε))
  (ht :
    ∀ (i₀ i₁ : Fin n),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) ((A ∘ (⇑e.symm : (a : Fin n) → ι)) i₁ % b - (A ∘ (⇑e.symm : (a : Fin n) → ι)) i₀ % b)) :
            ℝ) <
          HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε),
  ∃ (t : ι → Fin (h.card ε)),
    ∀ (i₀ i₁ : ι),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: obtain ⟨t, ht⟩ := h.exists_partition' n hε hb (A ∘ e.symm)
-- 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 : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h.card ε)
ht :
  ∀ (i₀ i₁ : Fin n),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) ((A ∘ (⇑e.symm : (a : Fin n) → ι)) i₁ % b - (A ∘ (⇑e.symm : (a : Fin n) → ι)) i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (t : ι → Fin (h.card ε)),
    ∀ (i₀ i₁ : ι),
      t i₀ = t i₁ →
        (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have refine : ∀ (i₀ i₁ : ι) (h : (t ∘ (⇑e : (a : ι) → Fin n)) i₀ = (t ∘ (⇑e : (a : ι) → Fin n)) i₁),
  (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: refine ⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩
-- 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 : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h_1 : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h_1.card ε)
ht :
  ∀ (i₀ i₁ : Fin n),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) ((A ∘ (⇑e.symm : (a : Fin n) → ι)) i₁ % b - (A ∘ (⇑e.symm : (a : Fin n) → ι)) i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
i₀ i₁ : ι
h : (t ∘ (⇑e : (a : ι) → Fin n)) i₀ = (t ∘ (⇑e : (a : ι) → Fin n)) i₁
⊢ (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have h₁ : i₁ = (e.symm : (a : Fin n) → ι) ((e : (a : ι) → Fin n) i₁ : Fin n)
Tactic: convert! (config := { transparency := .default }) ht (e i₀) (e i₁) h
-- 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 : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h_1 : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h_1.card ε)
ht :
  ∀ (i₀ i₁ : Fin n),
    t i₀ = t i₁ →
      (↑((abv : (a : R) → ℤ) ((A ∘ (⇑e.symm : (a : Fin n) → ι)) i₁ % b - (A ∘ (⇑e.symm : (a : Fin n) → ι)) i₀ % b)) :
          ℝ) <
        HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
i₀ i₁ : ι
h : (t ∘ (⇑e : (a : ι) → Fin n)) i₀ = (t ∘ (⇑e : (a : ι) → Fin n)) i₁
h₁ : i₁ = (e.symm : (a : Fin n) → ι) ((e : (a : ι) → Fin n) i₁ : Fin n)
⊢ (↑((abv : (a : R) → ℤ) (A i₁ % b - A i₀ % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
have h₂ : i₀ = (e.symm : (a : Fin n) → ι) ((e : (a : ι) → Fin n) i₀ : Fin n)
Tactic: convert! (config := { transparency := .default }) ht (e i₀) (e i₁) h
-- 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
⊢ ∀ {ε : ℝ} (_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 haveI : ∀ (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 : ℤ) ε
Tactic: haveI := Classical.decEq R
-- 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
ε : ℝ
_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 : ℤ) ε
have zero : Ne (α := Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ) 0 1
Tactic: refine ⟨0, 1, ?_, ?_⟩
-- 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
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ → Fin 0 → R
zero : Ne (α := Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ) 0 1
⊢ ∃ (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 : ℤ) ε
have zero₁ : ∀ (k : Fin 0), (↑((abv : (a : R) → ℤ) (A 1 k % b - A 0 k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
Tactic: refine ⟨0, 1, ?_, ?_⟩
-- 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),
    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 obtain : ∀ (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 ^ 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 : ℤ) ε
Tactic: 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
-- 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 ε
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 ^ 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 obtain : ∀ (s : Fin M) (hs : M ^ n < Finset.card (α := Fin (M ^ n.succ).succ) {x : Fin (M ^ n.succ).succ | t x = s}),
  ∃ (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 : ℤ) ε
Tactic: 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))
-- 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 ε
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}
⊢ (M ^ n).succ ≤ List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s})
have rwa : (M ^ n).succ ≤ Finset.card (α := Fin (M ^ n.succ).succ) {x : Fin (M ^ n.succ).succ | t x = s}
Tactic: rwa [Finset.length_toList]
-- 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 : 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}
⊢ ∃ (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 this₁ : (M ^ n).succ ≤ List.length (α := Fin (M ^ n.succ).succ) (Finset.toList {x : Fin (M ^ n.succ).succ | t x = s})
Tactic: have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]
-- 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})
⊢ ∃ (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_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) sorry)
        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) sorry)
        j)),
  i = j
Tactic: refine ⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩