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