internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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₃]
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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 _ _)
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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 _ _
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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 _ _
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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⌉₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (⌈x⌉₊ - 1) / d ≤ ⌊x + y⌋₊ / d
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ - 1 ≤ ⌊x + y⌋₊
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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])]
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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)]
Proof state after:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 0 ≤ x + y
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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 _ _)
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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₃|
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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|
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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 _
Proof state after:
no goals
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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]
Proof 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