R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
let e := Fintype.equivFin ι
case intro.intro.intro
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
obtain ⟨i₀, i₁, ne, h⟩ := h.exists_approx_aux (Fintype.card ι) hε hb fun x y ↦ A x (e.symm y)
case intro.intro.intro
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
case intro.intro.intro
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
refine' ⟨i₀, i₁, ne, fun k ↦ _⟩
no goals
case intro.intro.intro
R : Type u_2
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_1
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 • ε
convert h (e k) <;> simp only [e.symm_apply_apply]