Theorem: BrunTitchmarsh.abs_rem_le (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
rw[rem_eq _ _ _ hx hz _ hd]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
have hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ( ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) : ℝ) := by
  rw [Nat.cast_sub]
  gcongr
  rw[Nat.le_floor_iff]
  rw[←add_le_add_iff_right 1]
  norm_cast
  rw [Nat.sub_add_cancel (by simp [hx])]
  linarith [Nat.ceil_le_self_add_one x (le_of_lt hx)]
  linarith
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
rw[hpush]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
obtain ⟨C₁, hC₁_le, hC₁⟩ := floor_div_approx (x + y) (by linarith) d
State after:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
case intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
obtain ⟨C₂, hC₂_le, hC₂⟩ := nat_div_approx (Nat.ceil x - 1) d
State after:
case intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
case intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
obtain ⟨C₃, hC₃_le, hC₃⟩ := ceil_approx (x) (by linarith)
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
rw[hC₁, hC₂, Nat.cast_sub, hC₃]
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |(x + y) / ↑d + C₁ - ((x + C₃ - ↑1) / ↑d + C₂) - (↑d)⁻¹ * y| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |(x + y) / ↑d + C₁ - ((x + C₃ - ↑1) / ↑d + C₂) - (↑d)⁻¹ * y| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
ring_nf
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
have : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹*C₃| + |C₁ - C₂| := by
  apply (abs_add _ _)
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
have : |(↑d)⁻¹ - (↑d)⁻¹*C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹*C₃| := abs_sub _ _
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
have : |C₁ - C₂| ≤ |C₁| + |C₂| := abs_sub _ _
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
have : |(d:ℝ)⁻¹| ≤ 1 := by
  rw[abs_inv]
  simp only [Nat.abs_cast]
  apply Nat.cast_inv_le_one
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝³ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝¹ : |C₁ - C₂| ≤ |C₁| + |C₂|
this✝ : |(↑d)⁻¹| ≤ 1
this : |(↑d)⁻¹ * C₃| ≤ |C₃|
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ 5

case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
linarith
State after:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
Tactic:
rw [Nat.cast_sub]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (⌈x⌉₊ - 1) / d ≤ ⌊x + y⌋₊ / d

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (⌈x⌉₊ - 1) / d ≤ ⌊x + y⌋₊ / d
Tactic:
gcongr
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ - 1 ≤ ⌊x + y⌋₊

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ - 1 ≤ ⌊x + y⌋₊
Tactic:
rw[Nat.le_floor_iff]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) ≤ x + y

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) ≤ x + y

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Tactic:
rw[←add_le_add_iff_right 1]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) + 1 ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1) + 1 ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Tactic:
norm_cast
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1 + 1) ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌈x⌉₊ - 1 + 1) ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Tactic:
rw [Nat.sub_add_cancel (by simp [hx])]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑⌈x⌉₊ ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑⌈x⌉₊ ≤ x + y + 1

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Tactic:
linarith [Nat.ceil_le_self_add_one x (le_of_lt hx)]
State after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Tactic:
simp [hx]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
⊢ 0 ≤ x + y
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
⊢ 0 ≤ x
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
Tactic:
apply (abs_add _ _)
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ |(↑d)⁻¹| ≤ 1
Tactic:
rw[abs_inv]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ |↑d|⁻¹ ≤ 1

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ |↑d|⁻¹ ≤ 1
Tactic:
simp only [Nat.abs_cast]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ (↑d)⁻¹ ≤ 1

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this : |C₁ - C₂| ≤ |C₁| + |C₂|
⊢ (↑d)⁻¹ ≤ 1
Tactic:
apply Nat.cast_inv_le_one
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ |(↑d)⁻¹ * C₃| ≤ |C₃|
Tactic:
rw[inv_mul_eq_div, abs_div]
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ |C₃| / |↑d| ≤ |C₃|

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ |C₃| / |↑d| ≤ |C₃|
Tactic:
apply div_le_self
State after:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 0 ≤ |C₃|

case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 1 ≤ |↑d|

State before:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 0 ≤ |C₃|
Tactic:
exact abs_nonneg _
State after:
no goals

State before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 1 ≤ |↑d|
Tactic:
simp only [Nat.abs_cast, Nat.one_le_cast]
State after:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 1 ≤ d

State before:
case hb
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
this✝² : |(↑d)⁻¹ - (↑d)⁻¹ * C₃ + (C₁ - C₂)| ≤ |(↑d)⁻¹ - (↑d)⁻¹ * C₃| + |C₁ - C₂|
this✝¹ : |(↑d)⁻¹ - (↑d)⁻¹ * C₃| ≤ |(↑d)⁻¹| + |(↑d)⁻¹ * C₃|
this✝ : |C₁ - C₂| ≤ |C₁| + |C₂|
this : |(↑d)⁻¹| ≤ 1
⊢ 1 ≤ d
Tactic:
omega
State after:
no goals

State before:
case intro.intro.intro.intro.intro.intro
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
hpush : ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) = ↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d)
C₁ : ℝ
hC₁_le : |C₁| ≤ 2
hC₁ : ↑(⌊x + y⌋₊ / d) = (x + y) / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑((⌈x⌉₊ - 1) / d) = ↑(⌈x⌉₊ - 1) / ↑d + C₂
C₃ : ℝ
hC₃_le : |C₃| ≤ 1
hC₃ : ↑⌈x⌉₊ = x + C₃
⊢ 1 ≤ ⌈x⌉₊
Tactic:
simp [hx]
State after:
no goals