[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hbε : 0 < abs b • ε := by
  rw [Algebra.smul_def]
  exact mul_pos hb' hε
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < |b| • ε
[PROOFSTEP]
rw [Algebra.smul_def]
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
⊢ 0 < ↑(algebraMap ℤ ℝ) |b| * ε
[PROOFSTEP]
exact mul_pos hb' hε
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hfloor : ∀ i, 0 ≤ floor ((A i % b : ℤ) / abs b • ε : ℝ) := fun _ ↦
  floor_nonneg.mpr (div_nonneg (cast_nonneg.mpr (emod_nonneg _ hb)) hbε.le)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
refine' ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), _⟩, _⟩
[GOAL]
case refine'_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊
[PROOFSTEP]
rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt]
[GOAL]
case refine'_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / |b| • ε < ↑↑⌈1 / ε⌉₊
[PROOFSTEP]
apply lt_of_lt_of_le _ (Nat.le_ceil _)
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ ↑(A i % b) / |b| • ε < 1 / ε
[PROOFSTEP]
rw [Algebra.smul_def, eq_intCast, ← div_div, div_lt_div_right hε, div_lt_iff hb', one_mul, cast_lt]
[GOAL]
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|
[PROOFSTEP]
exact Int.emod_lt _ hb
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
⊢ ∀ (i₀ i₁ : Fin n),
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
        (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁ →
      ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
intro i₀ i₁ hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hi : (⌊↑(A i₀ % b) / abs b • ε⌋.natAbs : ℤ) = ⌊↑(A i₁ % b) / abs b • ε⌋.natAbs :=
  congr_arg ((↑) : ℕ → ℤ) (Fin.mk_eq_mk.mp hi)
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi : ↑(natAbs ⌊↑(A i₀ % b) / |b| • ε⌋) = ↑(natAbs ⌊↑(A i₁ % b) / |b| • ε⌋)
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rw [natAbs_of_nonneg (hfloor i₀), natAbs_of_nonneg (hfloor i₁)] at hi 
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
have hi := abs_sub_lt_one_of_floor_eq_floor hi
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₀ % b) / |b| • ε - ↑(A i₁ % b) / |b| • ε| < 1
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rw [abs_sub_comm, ← sub_div, abs_div, abs_of_nonneg hbε.le, div_lt_iff hbε, one_mul] at hi 
[GOAL]
case refine'_2
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑|b|
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / |b| • ε⌋
i₀ i₁ : Fin n
hi✝¹ :
  (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₀ =
    (fun i => { val := natAbs ⌊↑(A i % b) / |b| • ε⌋, isLt := (_ : natAbs ⌊↑(A i % b) / |b| • ε⌋ < ⌈1 / ε⌉₊) }) i₁
hi✝ : ⌊↑(A i₀ % b) / |b| • ε⌋ = ⌊↑(A i₁ % b) / |b| • ε⌋
hi : |↑(A i₁ % b) - ↑(A i₀ % b)| < |b| • ε
⊢ ↑|A i₁ % b - A i₀ % b| < |b| • ε
[PROOFSTEP]
rwa [Int.cast_abs, Int.cast_sub]
