awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
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₁)
⊢ 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)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
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) : ℝ) / |b| • ε⌋ = ⌊(↑(A i₁ % b) : ℝ) / |b| • ε⌋

Tactic:
rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi

Premises used: Int.natAbs_of_nonneg
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
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) : ℝ) / |b| • ε - (↑(A i₁ % b) : ℝ) / |b| • ε| < 1

Tactic:
have hi := abs_sub_lt_one_of_floor_eq_floor hi
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
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
⊢ |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

Premises used: abs_div, LT.lt.le, sub_div, div_lt_iff₀, abs_of_nonneg, abs_sub_comm, one_mul
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
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| • ε
refine_2 : |(↑(A i₁ % b - A i₀ % b) : ℝ)| < |b| • ε
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : |HSub.hSub (α := ℝ) (↑(A i₁ % b) : ℝ) (↑(A i₀ % b) : ℝ)| < |b| • ε
⊢ (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε

Tactic:
rwa [Int.cast_abs, Int.cast_sub]

Premises used: Int.cast_abs, Int.cast_sub
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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
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 : ℤ) ε
⊢ ∃ (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⟩⟩

Premises used: Finite.exists_equiv_fin
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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
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 : ℤ) ε
⊢ ∃ (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)

Premises used: Function.comp, AbsoluteValue.IsAdmissible.exists_partition', Equiv.symm, DFunLike.coe
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε

Tactic:
⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩

Premises used: Function.comp, Exists.intro, DFunLike.coe
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε
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 : ℤ) ε
⊢ ∃ (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:
refine ⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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) → ℤ)
          (Function.comp (α := Fin n) A ((⇑e.symm : (a : Fin n) → ι) : (a : Fin n) → ι)
                ((e : (a : ι) → Fin n) i₁ : Fin n) %
              b -
            Function.comp (α := Fin n) A ((⇑e.symm : (a : Fin n) → ι) : (a : Fin n) → ι)
                ((e : (a : ι) → Fin n) i₀ : Fin n) %
              b)) :
      ℝ) <
    HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
ht (e i₀) (e i₁) h

Premises used: DFunLike.coe
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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)
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 : ℤ) ε

Tactic:
convert! (config := { transparency := .default }) ht (e i₀) (e i₁) h

Premises used: DFunLike.coe
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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₁
⊢ i₁ = (e.symm : (a : Fin n) → ι) ((e : (a : ι) → Fin n) i₁ : Fin n)

Tactic:
simp only [e.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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₁
⊢ i₀ = (e.symm : (a : Fin n) → ι) ((e : (a : ι) → Fin n) i₀ : Fin n)

Tactic:
simp only [e.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
n : ℕ
h : abv.IsAdmissible
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 : ℤ) ε
⊢ ∀ {ε : ℝ} (_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
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε

Tactic:
⟨0, 1, ?_, ?_⟩

Premises used: And.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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
zero₁ :
  ∀ (k : Fin 0),
    (↑((abv : (a : R) → ℤ) (A 1 k % b - A 0 k % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε
⊢ ∃ (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:
refine ⟨0, 1, ?_, ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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
⊢ Ne (α := Fin (HPow.hPow (β := ℕ) (h.card ε) 0).succ) 0 1

Tactic:
simp
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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),
    ∀ (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 : ℤ) ε

Tactic:
h.exists_partition hε hb fun x ↦ A x 0

Premises used: AbsoluteValue.IsAdmissible.exists_partition, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 ε
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 : ℤ) ε
⊢ ∃ (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

Premises used: AbsoluteValue.IsAdmissible.exists_partition, OfNat.ofNat
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε
⊢ Fintype.card (Fin M) * M ^ n < Fintype.card (Fin (M ^ n.succ).succ)

Tactic:
simpa only [Fintype.card_fin, pow_succ'] using Nat.lt_succ_self (M ^ n.succ)

Premises used: Fintype.card_fin, Nat.lt_succ_self, HPow.hPow, Nat.succ, pow_succ'
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε
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 : ℤ) ε
⊢ ∃ (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))

Premises used: Fintype.exists_lt_card_fiber_of_mul_lt_card
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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}
rwa rwa₁ rwa₂ rwa₃ : (M ^ n).succ ≤ 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})

Tactic:
rwa [Finset.length_toList]

Premises used: Finset.length_toList
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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})

Tactic:
have : (M ^ n).succ ≤ (Finset.toList {x | t x = s}).length := by
      rwa [Finset.length_toList]
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε

Tactic:
⟨fun i ↦ (Finset.toList {x | t x = s})[i.castLE this], fun i j h ↦ ?_,
      fun i₀ i₁ ↦ ht _ _ ?_⟩

Premises used: Finset.univ, Fin.castLE, Finset.toList, GetElem.getElem, And.intro, Exists.intro, Finset.filter, Eq