[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : IsAdmissible abv
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
[PROOFSTEP]
let e := Fintype.equivFin ι
[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : IsAdmissible abv
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
[PROOFSTEP]
obtain ⟨t, ht⟩ := h.exists_partition' (Fintype.card ι) hε hb (A ∘ e.symm)
[GOAL]
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : IsAdmissible abv
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
t : Fin (Fintype.card ι) → Fin (IsAdmissible.card h ε)
ht : ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
[PROOFSTEP]
refine' ⟨t ∘ e, fun i₀ i₁ h ↦ _⟩
[GOAL]
case intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : IsAdmissible abv
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
t : Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)
ht : ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
i₀ i₁ : ι
h : (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁
⊢ ↑(↑abv (A i₁ % b - A i₀ % b)) < ↑abv b • ε
[PROOFSTEP]
convert (config := { transparency := .default }) ht (e i₀) (e i₁) h
[GOAL]
case h.e'_3.h.e'_3.h.e'_6.h.e'_5.h.e'_5.h.e'_1
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : IsAdmissible abv
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
t : Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)
ht : ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
i₀ i₁ : ι
h : (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁
⊢ i₁ = ↑e.symm (↑e i₁)
[PROOFSTEP]
simp only [e.symm_apply_apply]
[GOAL]
case h.e'_3.h.e'_3.h.e'_6.h.e'_6.h.e'_5.h.e'_1
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : IsAdmissible abv
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
t : Fin (Fintype.card ι) → Fin (IsAdmissible.card h✝ ε)
ht : ∀ (i₀ i₁ : Fin (Fintype.card ι)), t i₀ = t i₁ → ↑(↑abv ((A ∘ ↑e.symm) i₁ % b - (A ∘ ↑e.symm) i₀ % b)) < ↑abv b • ε
i₀ i₁ : ι
h : (t ∘ ↑e) i₀ = (t ∘ ↑e) i₁
⊢ i₀ = ↑e.symm (↑e i₀)
[PROOFSTEP]
simp only [e.symm_apply_apply]
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
n : ℕ
h : IsAdmissible abv
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
haveI := Classical.decEq R
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
n : ℕ
h : IsAdmissible abv
this : DecidableEq R
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
intro ε _hε b _hb A
[GOAL]
case zero
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin Nat.zero), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
refine' ⟨0, 1, _, _⟩
[GOAL]
case zero.refine'_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R
⊢ 0 ≠ 1
[PROOFSTEP]
simp
[GOAL]
case zero.refine'_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
ε : ℝ
_hε : 0 < ε
b : R
_hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.zero)) → Fin Nat.zero → R
⊢ ∀ (k : Fin Nat.zero), ↑(↑abv (A 1 k % b - A 0 k % b)) < ↑abv b • ε
[PROOFSTEP]
rintro ⟨i, ⟨⟩⟩
[GOAL]
case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
⊢ ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
intro ε hε b hb A
[GOAL]
case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
let M := h.card ε
[GOAL]
case succ
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
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 _ _ _ _ _ t (M ^ n)
      (by simpa only [Fintype.card_fin, pow_succ] using Nat.lt_succ_self (M ^ n.succ))
  refine' ⟨fun i ↦ (Finset.univ.filter fun x ↦ t x = s).toList.nthLe i _, _, fun i₀ i₁ ↦ ht _ _ _⟩
  · refine' i.2.trans_le _
    rwa [Finset.length_toList]
  · intro i j h
    ext
    exact Fin.mk.inj_iff.mp (List.nodup_iff_injective_get.mp (Finset.nodup_toList _) h)
  have : ∀ i h, (Finset.univ.filter fun x ↦ t x = s).toList.nthLe i h ∈ Finset.univ.filter fun x ↦ t x = s :=
    by
    intro i h
    exact Finset.mem_toList.mp (List.get_mem _ i h)
  obtain ⟨_, h₀⟩ := Finset.mem_filter.mp (this i₀ _)
  obtain ⟨_, h₁⟩ := Finset.mem_filter.mp (this i₁ _)
  exact h₀.trans h₁.symm
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
[PROOFSTEP]
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.
[GOAL]
case intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
[PROOFSTEP]
obtain ⟨s, hs⟩ :=
  @Fintype.exists_lt_card_fiber_of_mul_lt_card _ _ _ _ _ t (M ^ n)
    (by simpa only [Fintype.card_fin, pow_succ] using Nat.lt_succ_self (M ^ n.succ))
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
⊢ Fintype.card (Fin M) * M ^ n < Fintype.card (Fin (Nat.succ (M ^ Nat.succ n)))
[PROOFSTEP]
simpa only [Fintype.card_fin, pow_succ] using Nat.lt_succ_self (M ^ n.succ)
[GOAL]
case intro.intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
⊢ ∃ s, Function.Injective s ∧ ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
[PROOFSTEP]
refine' ⟨fun i ↦ (Finset.univ.filter fun x ↦ t x = s).toList.nthLe i _, _, fun i₀ i₁ ↦ ht _ _ _⟩
[GOAL]
case intro.intro.refine'_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i : Fin (Nat.succ (M ^ n))
⊢ ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
[PROOFSTEP]
refine' i.2.trans_le _
[GOAL]
case intro.intro.refine'_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i : Fin (Nat.succ (M ^ n))
⊢ Nat.succ (M ^ n) ≤ List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
[PROOFSTEP]
rwa [Finset.length_toList]
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
⊢ Function.Injective fun i =>
    List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
      (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)))
[PROOFSTEP]
intro i j h
[GOAL]
case intro.intro.refine'_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i j : Fin (Nat.succ (M ^ n))
h :
  (fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i =
    (fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      j
⊢ i = j
[PROOFSTEP]
ext
[GOAL]
case intro.intro.refine'_2.h
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i j : Fin (Nat.succ (M ^ n))
h :
  (fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      i =
    (fun i =>
        List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
          (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
      j
⊢ ↑i = ↑j
[PROOFSTEP]
exact Fin.mk.inj_iff.mp (List.nodup_iff_injective_get.mp (Finset.nodup_toList _) h)
[GOAL]
case intro.intro.refine'_3
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
⊢ t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₀) =
    t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₁)
[PROOFSTEP]
have : ∀ i h, (Finset.univ.filter fun x ↦ t x = s).toList.nthLe i h ∈ Finset.univ.filter fun x ↦ t x = s :=
  by
  intro i h
  exact Finset.mem_toList.mp (List.get_mem _ i h)
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
⊢ ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
    List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈
      Finset.filter (fun x => t x = s) Finset.univ
[PROOFSTEP]
intro i h
[GOAL]
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
i : ℕ
h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))
⊢ List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈
    Finset.filter (fun x => t x = s) Finset.univ
[PROOFSTEP]
exact Finset.mem_toList.mp (List.get_mem _ i h)
[GOAL]
case intro.intro.refine'_3
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
this :
  ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
    List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈
      Finset.filter (fun x => t x = s) Finset.univ
⊢ t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₀) =
    t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₁)
[PROOFSTEP]
obtain ⟨_, h₀⟩ := Finset.mem_filter.mp (this i₀ _)
[GOAL]
case intro.intro.refine'_3.intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
this :
  ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
    List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈
      Finset.filter (fun x => t x = s) Finset.univ
left✝ : List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.22999 ∈ Finset.univ
h₀ : t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.22999) = s
⊢ t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₀) =
    t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₁)
[PROOFSTEP]
obtain ⟨_, h₁⟩ := Finset.mem_filter.mp (this i₁ _)
[GOAL]
case intro.intro.refine'_3.intro.intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this✝ : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
t : Fin (Nat.succ (M ^ Nat.succ n)) → Fin M
ht : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ Nat.succ n))), t i₀ = t i₁ → ↑(↑abv (A i₁ 0 % b - A i₀ 0 % b)) < ↑abv b • ε
s : Fin M
hs : M ^ n < Finset.card (Finset.filter (fun x => t x = s) Finset.univ)
i₀ i₁ : Fin (Nat.succ (M ^ n))
this :
  ∀ (i : ℕ) (h : i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))),
    List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) i h ∈
      Finset.filter (fun x => t x = s) Finset.univ
left✝¹ : List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.22999 ∈ Finset.univ
h₀ : t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₀ ?m.22999) = s
left✝ : List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.23393 ∈ Finset.univ
h₁ : t (List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i₁ ?m.23393) = s
⊢ t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₀) =
    t
      ((fun i =>
          List.nthLe (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ)) ↑i
            (_ : ↑i < List.length (Finset.toList (Finset.filter (fun x => t x = s) Finset.univ))))
        i₁)
[PROOFSTEP]
exact h₀.trans h₁.symm
[GOAL]
case succ.intro.intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h ε
s : Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
obtain ⟨k₀, k₁, hk, h⟩ := ih hε hb fun x ↦ Fin.tail (A (s x))
[GOAL]
case succ.intro.intro.intro.intro.intro
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
s : Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
k₀ k₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin (Nat.succ n)), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
refine' ⟨s k₀, s k₁, fun h ↦ hk (s_inj h), fun i ↦ Fin.cases _ (fun i ↦ _) i⟩
[GOAL]
case succ.intro.intro.intro.intro.intro.refine'_1
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
s : Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
k₀ k₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
i : Fin (Nat.succ n)
⊢ ↑(↑abv (A (s k₁) 0 % b - A (s k₀) 0 % b)) < ↑abv b • ε
[PROOFSTEP]
exact hs k₀ k₁
[GOAL]
case succ.intro.intro.intro.intro.intro.refine'_2
R : Type u_1
inst✝ : EuclideanDomain R
abv : AbsoluteValue R ℤ
h✝ : IsAdmissible abv
this : DecidableEq R
n : ℕ
ih :
  ∀ {ε : ℝ},
    0 < ε →
      ∀ {b : R},
        b ≠ 0 →
          ∀ (A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n)) → Fin n → R),
            ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Nat.succ n)) → Fin (Nat.succ n) → R
M : ℕ := IsAdmissible.card h✝ ε
s : Fin (Nat.succ (M ^ n)) → Fin (Nat.succ (M ^ Nat.succ n))
s_inj : Function.Injective s
hs : ∀ (i₀ i₁ : Fin (Nat.succ (M ^ n))), ↑(↑abv (A (s i₁) 0 % b - A (s i₀) 0 % b)) < ↑abv b • ε
k₀ k₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ n))
hk : k₀ ≠ k₁
h : ∀ (k : Fin n), ↑(↑abv (Fin.tail (A (s k₁)) k % b - Fin.tail (A (s k₀)) k % b)) < ↑abv b • ε
i✝ : Fin (Nat.succ n)
i : Fin n
⊢ ↑(↑abv (A (s k₁) (Fin.succ i) % b - A (s k₀) (Fin.succ i) % b)) < ↑abv b • ε
[PROOFSTEP]
exact h i
[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Fintype.card ι)) → ι → R
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
let e := Fintype.equivFin ι
[GOAL]
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h ε ^ Fintype.card ι)) → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
obtain ⟨i₀, i₁, ne, h⟩ := h.exists_approx_aux (Fintype.card ι) hε hb fun x y ↦ A x (e.symm y)
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι)) → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι))
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(↑abv (A i₁ (↑e.symm k) % b - A i₀ (↑e.symm k) % b)) < ↑abv b • ε
⊢ ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : ι), ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
refine' ⟨i₀, i₁, ne, fun k ↦ _⟩
[GOAL]
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι)) → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι))
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(↑abv (A i₁ (↑e.symm k) % b - A i₀ (↑e.symm k) % b)) < ↑abv b • ε
k : ι
⊢ ↑(↑abv (A i₁ k % b - A i₀ k % b)) < ↑abv b • ε
[PROOFSTEP]
convert h (e k)
[GOAL]
case h.e'_3.h.e'_3.h.e'_6.h.e'_5.h.e'_5.h.e'_2
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι)) → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι))
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(↑abv (A i₁ (↑e.symm k) % b - A i₀ (↑e.symm k) % b)) < ↑abv b • ε
k : ι
⊢ k = ↑e.symm (↑e k)
[PROOFSTEP]
simp only [e.symm_apply_apply]
[GOAL]
case h.e'_3.h.e'_3.h.e'_6.h.e'_6.h.e'_5.h.e'_2
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Fintype ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
h✝ : IsAdmissible abv
A : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι)) → ι → R
e : ι ≃ Fin (Fintype.card ι) := Fintype.equivFin ι
i₀ i₁ : Fin (Nat.succ (IsAdmissible.card h✝ ε ^ Fintype.card ι))
ne : i₀ ≠ i₁
h : ∀ (k : Fin (Fintype.card ι)), ↑(↑abv (A i₁ (↑e.symm k) % b - A i₀ (↑e.symm k) % b)) < ↑abv b • ε
k : ι
⊢ k = ↑e.symm (↑e k)
[PROOFSTEP]
simp only [e.symm_apply_apply]