n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
hbε : 0 < abs b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
have hbε : 0 < abs b • ε := by
  rw [Algebra.smul_def]
  exact mul_pos hb' hε
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
hbε : 0 < abs b • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / abs b • ε⌋
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
hbε : 0 < abs b • ε
⊢ ∃ t, ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abs (A i₁ % b - A i₀ % b)) < abs b • ε
have hfloor : ∀ i, 0 ≤ floor ((A i % b : ℤ) / abs b • ε : ℝ) :=
  fun _ ↦ floor_nonneg.mpr (div_nonneg (cast_nonneg.mpr (emod_nonneg _ hb)) hbε.le)
case refine'_1
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : 0 < ↑(abs b)
hbε : 0 < abs b • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊↑(A i % b) / abs b • ε⌋
i : Fin n
⊢ natAbs ⌊↑(A i % b) / abs b • ε⌋ < ⌈1 / ε⌉₊

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