internlm/Lean-Github huggingface dataset:
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
u : ℕ
hxu : x ≤ u
hut : u < t
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
⊢ trunc n (y - round (y - x) - u) = y - round (y - x) - u
Tactic:
have hxyx : x < round (y - round (y - x)) := calc
  x ≤ u                         := hxu
  _ < t                         := hut
  _ ≤ y - round (y - x)         := htx'
  _ = round (y - round (y - x)) := hfx'.symm
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
u : ℕ
hxu : x ≤ u
hut : u < t
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hxyx : x < round (y - round (y - x))
⊢ trunc n (y - round (y - x) - u) = y - round (y - x) - u
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
u : ℕ
hxu : x ≤ u
hut : u < t
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hxyx : x < round (y - round (y - x))
⊢ trunc n (y - round (y - x) - u) = y - round (y - x) - u
Tactic:
rewrite [← hfx']
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
u : ℕ
hxu : x ≤ u
hut : u < t
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hxyx : x < round (y - round (y - x))
⊢ trunc n (round (y - round (y - x)) - u) = round (y - round (y - x)) - u
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
u : ℕ
hxu : x ≤ u
hut : u < t
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hxyx : x < round (y - round (y - x))
⊢ trunc n (round (y - round (y - x)) - u) = round (y - round (y - x)) - u
Tactic:
exact s₃ npos hfaithful₀ hfaithful₁ hfy hfx hfu hxy hxu hyxulp hxyx hux'
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
⊢ trunc n (y - t) = y - t
Tactic:
rw [ht', tsub_tsub_cancel_of_le hzy', trunc_round npos hfaithful₁]
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
⊢ s = t
Tactic:
rewrite [← round_eq_of_trunc_eq npos hfaithful₀ hft]
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
⊢ s = round t
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
⊢ s = round t
Tactic:
cases Nat.lt_or_ge x t with
| inl hxt => have hfxt : round (t - x) = t - x := by
    apply round_eq_of_trunc_eq npos hfaithful₀
    apply hfut le_rfl hxt hfx
    rewrite [hfx']
    exact Nat.le_trans hxt.le htx'
  rw [hs₁ hxt, hfxt, add_tsub_cancel_of_le hxt.le]
| inr htx => have hftx : round (x - t) = x - t := by
    apply round_eq_of_trunc_eq npos hfaithful₀
    rewrite [ht] at htx hfty ⊢
    exact s₁ npos htx hxy (trunc_round npos hfaithful₁ _) hfy hfx hfty
  rw [hs₂ htx, hftx, tsub_tsub_cancel_of_le htx]
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
case inl
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ s = round t
Tactic:
have hfxt : round (t - x) = t - x := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  apply hfut le_rfl hxt hfx
  rewrite [hfx']
  exact Nat.le_trans hxt.le htx'
Proof state after:
case inl
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
hfxt : round (t - x) = t - x
⊢ s = round t
Theorem: interval_shift₁
Proof state before:
case inl
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
hfxt : round (t - x) = t - x
⊢ s = round t
Tactic:
rw [hs₁ hxt, hfxt, add_tsub_cancel_of_le hxt.le]
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ round (t - x) = t - x
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ trunc n (t - x) = t - x
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ trunc n (t - x) = t - x
Tactic:
apply hfut le_rfl hxt hfx
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ x ≤ round (y - round (y - x))
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ x ≤ round (y - round (y - x))
Tactic:
rewrite [hfx']
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ x ≤ y - round (y - x)
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
hxt : x < t
⊢ x ≤ y - round (y - x)
Tactic:
exact Nat.le_trans hxt.le htx'
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
case inr
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
⊢ s = round t
Tactic:
have hftx : round (x - t) = x - t := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  rewrite [ht] at htx hfty ⊢
  exact s₁ npos htx hxy (trunc_round npos hfaithful₁ _) hfy hfx hfty
Proof state after:
case inr
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
hftx : round (x - t) = x - t
⊢ s = round t
Theorem: interval_shift₁
Proof state before:
case inr
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
hftx : round (x - t) = x - t
⊢ s = round t
Tactic:
rw [hs₂ htx, hftx, tsub_tsub_cancel_of_le htx]
Proof state after:
no goals
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
⊢ round (x - t) = x - t
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
⊢ trunc n (x - t) = x - t
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - t) = y - t
htx : x ≥ t
⊢ trunc n (x - t) = x - t
Tactic:
rewrite [ht] at htx hfty ⊢
Proof state after:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - round (y - round (y - z))) = y - round (y - round (y - z))
htx : x ≥ round (y - round (y - z))
⊢ trunc n (x - round (y - round (y - z))) = x - round (y - round (y - z))
Theorem: interval_shift₁
Proof state before:
round : ℕ → ℕ
x y z w s t n : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hml : sub_left_monotonic n round
hfx : trunc n x = x
hfy : trunc n y = y
hfz : trunc n z = z
hfw : trunc n w = w
hzx : z ≤ x
hzy : z ≤ y
hyxulp : ulp n y ≤ 2 * x
ht : t = round (y - round (y - z))
hs₁ : x < t → s = round (x + round (t - x))
hs₂ : t ≤ x → s = round (x - round (x - t))
hxw : x ≤ w
hwy : w ≤ y
hxy : x ≤ y
ht' : t = y - round (y - z)
htx' : t ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
hfx' : round (y - round (y - x)) = y - round (y - x)
hfut : ∀ {u : ℕ}, x ≤ u → u < t → trunc n u = u → u ≤ round (y - round (y - x)) → trunc n (t - u) = t - u
hfty : trunc n (y - round (y - round (y - z))) = y - round (y - round (y - z))
htx : x ≥ round (y - round (y - z))
⊢ trunc n (x - round (y - round (y - z))) = x - round (y - round (y - z))
Tactic:
exact s₁ npos htx hxy (trunc_round npos hfaithful₁ _) hfy hfx hfty
Proof state after:
no goals