internlm/Lean-Github huggingface dataset:
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (∑
      n ∈
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
            weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
            nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
            nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.support,
      if d ∣ n then
        { support := Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊, prodPrimes := primorial ⌊z⌋₊, prodPrimes_squarefree := ⋯,
              weights := fun x => 1, weights_nonneg := primeInterSieve.proof_2, totalMass := y,
              nu := (↑ζ).pdiv ↑ArithmeticFunction.id, nu_mult := primeInterSieve.proof_3, nu_pos_of_prime := ⋯,
              nu_lt_one_of_prime := ⋯, level := z, one_le_level := hz }.weights
          n
      else 0) =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d)
Tactic:
simp only [Finset.sum_boole, Nat.cast_inj]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card = ⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Ioc (⌈x⌉₊ - 1) ⌊x + y⌋₊)).card
Tactic:
rw [←Nat.Icc_succ_left]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Icc (⌈x⌉₊ - 1).succ ⌊x + y⌋₊)).card
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Icc ⌈x⌉₊ ⌊x + y⌋₊)).card =
    (Finset.filter (fun x => d ∣ x) (Finset.Icc (⌈x⌉₊ - 1).succ ⌊x + y⌋₊)).card
Tactic:
congr
Proof state after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = (⌈x⌉₊ - 1).succ
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = (⌈x⌉₊ - 1).succ
Tactic:
rw [←Nat.succ_sub]
Proof state after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = ⌈x⌉₊.succ - 1

case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ⌈x⌉₊ = ⌈x⌉₊.succ - 1

case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Tactic:
rfl
Proof state after:
case e_s.e_s.e_a
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ 1 ≤ ⌈x⌉₊
Theorem: BrunTitchmarsh.multSum_eq
Proof state before:
case e_s.e_s.e_a
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.multSum_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Ioc (⌈x⌉₊ - 1) ⌊x + y⌋₊)).card = ⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d
Tactic:
rw[BrunTitchmarsh.card_Ioc_filter_dvd _ _ _ hd]
Proof state after:
no goals
Theorem: BrunTitchmarsh.rem_eq
Proof 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 = ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
unfold Sieve.rem
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Theorem: BrunTitchmarsh.rem_eq
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (primeInterSieve x y z hz).multSum d - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
rw[multSum_eq x y z hx hz d hd]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Theorem: BrunTitchmarsh.rem_eq
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) - (primeInterSieve x y z hz).nu d * (primeInterSieve x y z hz).totalMass =
    ↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y
Tactic:
simp [primeInterSieve, if_neg hd]
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1
Tactic:
trans Nat.floor x + 1
Proof state after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ ↑⌊x⌋₊ + 1

x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ + 1 ≤ x + 1
Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ + 1 ≤ x + 1
Tactic:
gcongr
Proof state after:
case bc
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x
Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one
Proof state before:
case bc
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ x
Tactic:
apply Nat.floor_le hx
Proof state after:
no goals
Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ ↑⌊x⌋₊ + 1
Tactic:
norm_cast
Proof state after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ⌈x⌉₊ ≤ ⌊x⌋₊ + 1
Theorem: BrunTitchmarsh.Nat.ceil_le_self_add_one
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ⌈x⌉₊ ≤ ⌊x⌋₊ + 1
Tactic:
exact Nat.ceil_le_floor_add_one x
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌊x⌋₊ = x + C
Tactic:
use ↑(Nat.floor x) - x
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1 ∧ ↑⌊x⌋₊ = x + (↑⌊x⌋₊ - x)
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1 ∧ ↑⌊x⌋₊ = x + (↑⌊x⌋₊ - x)
Tactic:
simp only [add_sub_cancel, and_true]
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌊x⌋₊ - x| ≤ 1
Tactic:
rw[abs_le]
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌊x⌋₊ - x ∧ ↑⌊x⌋₊ - x ≤ 1
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌊x⌋₊ - x ∧ ↑⌊x⌋₊ - x ≤ 1
Tactic:
constructor
Proof state after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌊x⌋₊ - x

case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ - x ≤ 1
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌊x⌋₊ - x
Tactic:
simp only [neg_le_sub_iff_le_add]
Proof state after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌊x⌋₊ + 1
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌊x⌋₊ + 1
Tactic:
linarith [Nat.lt_floor_add_one x]
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ - x ≤ 1
Tactic:
simp only [tsub_le_iff_right]
Proof state after:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ 1 + x
Theorem: BrunTitchmarsh.floor_approx
Proof state before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌊x⌋₊ ≤ 1 + x
Tactic:
linarith [Nat.floor_le hx]
Proof state after:
no goals
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌈x⌉₊ = x + C
Tactic:
use ↑(Nat.ceil x) - x
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1 ∧ ↑⌈x⌉₊ = x + (↑⌈x⌉₊ - x)
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1 ∧ ↑⌈x⌉₊ = x + (↑⌈x⌉₊ - x)
Tactic:
simp only [add_sub_cancel, and_true]
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ |↑⌈x⌉₊ - x| ≤ 1
Tactic:
rw[abs_le]
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x ∧ ↑⌈x⌉₊ - x ≤ 1
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x ∧ ↑⌈x⌉₊ - x ≤ 1
Tactic:
constructor
Proof state after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x

case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ - x ≤ 1
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ -1 ≤ ↑⌈x⌉₊ - x
Tactic:
simp only [neg_le_sub_iff_le_add]
Proof state after:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌈x⌉₊ + 1
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h.left
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ x ≤ ↑⌈x⌉₊ + 1
Tactic:
linarith [Nat.le_ceil x]
Proof state after:
no goals
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ - x ≤ 1
Tactic:
simp only [tsub_le_iff_right]
Proof state after:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ 1 + x
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ 1 + x
Tactic:
rw[add_comm]
Proof state after:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1
Theorem: BrunTitchmarsh.ceil_approx
Proof state before:
case h.right
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
⊢ ↑⌈x⌉₊ ≤ x + 1
Tactic:
exact Nat.ceil_le_self_add_one x hx
Proof state after:
no goals
Theorem: BrunTitchmarsh.nat_div_approx
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑(a / b) = ↑a / ↑b + C
Tactic:
rw[←Nat.floor_div_eq_div (α:=ℝ)]
Proof state after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌊↑a / ↑b⌋₊ = ↑a / ↑b + C
Theorem: BrunTitchmarsh.nat_div_approx
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ ∃ C, |C| ≤ 1 ∧ ↑⌊↑a / ↑b⌋₊ = ↑a / ↑b + C
Tactic:
apply floor_approx (a/b:ℝ) (by positivity)
Proof state after:
no goals
Theorem: BrunTitchmarsh.nat_div_approx
Proof state before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
a b : ℕ
⊢ 0 ≤ ↑a / ↑b
Tactic:
positivity
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
by_cases hd : d = 0
Proof state after:
case pos
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C

case neg
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case neg
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
obtain ⟨C₁, hC₁_le, hC₁⟩ := nat_div_approx (Nat.floor x) d
Proof state after:
case neg.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case neg.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
obtain ⟨C₂, hC₂_le, hC₂⟩ := floor_approx x hx
Proof state after:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
rw[hC₁, hC₂]
Proof state after:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + C
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case neg.intro.intro.intro.intro
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ ∃ C, |C| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + C
Tactic:
use  C₁ + C₂/d
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2 ∧ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)
Tactic:
refine ⟨?_, by ring⟩
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ |C₁ + C₂ / ↑d| ≤ 2
Tactic:
have : |C₁ + C₂/d| ≤ |C₁| + |C₂/d| := abs_add C₁ (C₂ / ↑d)
Proof state after:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₁ + C₂ / ↑d| ≤ 2
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case h
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this✝ : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
this : |C₂ / ↑d| ≤ |C₂|
⊢ |C₁ + C₂ / ↑d| ≤ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case pos
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : d = 0
⊢ ∃ C, |C| ≤ 2 ∧ ↑(⌊x⌋₊ / d) = x / ↑d + C
Tactic:
simp [hd]
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
⊢ (x + C₂) / ↑d + C₁ = x / ↑d + (C₁ + C₂ / ↑d)
Tactic:
ring
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₂ / ↑d| ≤ |C₂|
Tactic:
rw[abs_div]
Proof state after:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |C₂| / |↑d| ≤ |C₂|
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ |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
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 0 ≤ |C₂|

case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ |↑d|
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case ha
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 0 ≤ |C₂|
Tactic:
exact abs_nonneg C₂
Proof state after:
no goals
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 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
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ d
Theorem: BrunTitchmarsh.floor_div_approx
Proof state before:
case hb
x✝ y z : ℝ
hx✝ : 0 < x✝
hy : 0 < y
hz : 1 ≤ z
x : ℝ
hx : 0 ≤ x
d : ℕ
hd : ¬d = 0
C₁ : ℝ
hC₁_le : |C₁| ≤ 1
hC₁ : ↑(⌊x⌋₊ / d) = ↑⌊x⌋₊ / ↑d + C₁
C₂ : ℝ
hC₂_le : |C₂| ≤ 1
hC₂ : ↑⌊x⌋₊ = x + C₂
this : |C₁ + C₂ / ↑d| ≤ |C₁| + |C₂ / ↑d|
⊢ 1 ≤ d
Tactic:
omega
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
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
rw[rem_eq _ _ _ hx hz _ hd]
Proof 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
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) - (↑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
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)
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
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)
⊢ |↑(⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
rw[hpush]
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)
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
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)
⊢ |↑(⌊x + y⌋₊ / d) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5
Tactic:
obtain ⟨C₁, hC₁_le, hC₁⟩ := floor_div_approx (x + y) (by linarith) d
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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
Proof 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
Theorem: BrunTitchmarsh.abs_rem_le
Proof 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)
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) - ↑((⌈x⌉₊ - 1) / d) - (↑d)⁻¹ * y| ≤ 5