awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
Goal:
R : Type u_1
inst : EuclideanDomain R
abv : AbsoluteValue R ℤ
h_1 : abv.IsAdmissible
this_1 : 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 ε
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 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

Tactic:
simpa [(Finset.nodup_toList _).getElem_inj_iff, Fin.val_inj] using h

Premises used: Finset.nodup_toList, List.Nodup.getElem_inj_iff, Fin.val_inj
-- 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})
i₀ i₁ : Fin (M ^ n).succ
⊢ ∀ (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) ⋯) =
      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
-- 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_2 : (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
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_2 i) ⋯) =
      s
refine_2 refine_2₁ :
  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_2 i₀) ⋯) =
    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_2 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_2 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_2 i) ⋯)
        i₁)

Tactic:
simp_rw [this]
-- 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 ε
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 : ℤ) ε
⊢ ∃ (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]
-- 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 ε
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 : ℤ) ε
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 : ℤ) ε
⊢ ∃ (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))

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

Tactic:
⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩

Premises used: And.intro, Exists.intro, Fin.cases
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε
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 : ℤ) ε
⊢ ∃ (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 : ℤ) ε

Tactic:
refine ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases ?_ (fun i ↦ ?_) i⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 (n + 1)
⊢ (↑((abv : (a : R) → ℤ) (A (s k₁) 0 % b - A (s k₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
hs k₀ k₁
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 (n + 1)
⊢ (↑((abv : (a : R) → ℤ) (A (s k₁) 0 % b - A (s k₀) 0 % b)) : ℝ) < HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
exact hs k₀ k₁
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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_1 : 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:
h i

Premises used: Fin.tail
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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_1 : 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:
exact h i
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 ι
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 : ℤ) ε
⊢ ∃ (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)

Premises used: Fintype.card, AbsoluteValue.IsAdmissible.exists_approx_aux, 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 : 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 : ℤ) ε

Tactic:
⟨i₀, i₁, ne, fun k ↦ ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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 : ℤ) ε
refine :
  ∀ (k : ι), (↑((abv : (a : R) → ℤ) (A i₁ k % b - A i₀ 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 : ℤ) ε

Tactic:
refine ⟨i₀, i₁, ne, fun k ↦ ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
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₁
                ((e.symm : (a : Fin (Fintype.card ι)) → ι)
                  ((e : (a : ι) → Fin (Fintype.card ι)) k : Fin (Fintype.card ι))) %
              b -
            A i₀
                ((e.symm : (a : Fin (Fintype.card ι)) → ι)
                  ((e : (a : ι) → Fin (Fintype.card ι)) k : Fin (Fintype.card ι))) %
              b)) :
      ℝ) <
    HSMul.hSMul (α := ℤ) ((abv : (a : R) → ℤ) b : ℤ) ε

Tactic:
h (e k)

Premises used: DFunLike.coe