Theorem: interval_shift₁ (Fl.lean)

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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hxy : x ≤ y := Nat.le_trans hxw hwy
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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have ht' : t = y - round (y - z) := by
  rewrite [ht]
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfy hfz hzy
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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have htx' : t ≤ y - round (y - x) := calc
  t = y - round (y - z) := ht'
  _ ≤ y - round (y - x) := tsub_le_tsub_left (hml hfz hfx hfy hzx) _
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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hzy' : round (y - z) ≤ y := by
  trans round (y - 0)
  . exact hml (trunc_zero n) hfz hfy (Nat.zero_le _)
  . rw [tsub_zero, round_eq_of_trunc_eq npos hfaithful₀ hfy]
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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hft : trunc n t = t := ht ▸ trunc_round npos hfaithful₁ _
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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hfx' : round (y - round (y - x)) = y - round (y - x) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfy hfx hxy
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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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)
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hfut {u : ℕ} (hxu : x ≤ u) (hut : u < t) (hfu : trunc n u = u)
  (hux' : u ≤ round (y - round (y - x)))
: trunc n (t - u) = t - u := by
  have hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u := by
    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
    rewrite [← hfx']
    exact s₃ npos hfaithful₀ hfaithful₁ hfy hfx hfu hxy hxu hyxulp hxyx hux'
  rewrite [ht] at hut htx' ⊢
  replace hfx' := trunc_eq_of_round_eq npos hfaithful₁ hfx'
  exact s₁ npos hut.le htx' hfu hfx' (trunc_round npos hfaithful₁ _) hfuxy
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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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 (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hfty : trunc n (y - t) = y - t := by
  rw [ht', tsub_tsub_cancel_of_le hzy', trunc_round npos hfaithful₁]
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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
have hst : s = t := by
  rewrite [← round_eq_of_trunc_eq npos hfaithful₀ hft]
  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]
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
hst : s = t
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w

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
hst : s = t
⊢ trunc n (w - s) = w - s ∧ trunc n (s - w) = s - w
Tactic:
rewrite [hst]
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
hst : s = t
⊢ trunc n (w - t) = w - t ∧ trunc n (t - w) = t - w

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
hst : s = t
⊢ trunc n (w - t) = w - t ∧ trunc n (t - w) = t - w
Tactic:
cases Nat.lt_or_ge w t with
| inl hwt => constructor
  . rw [tsub_eq_zero_of_le hwt.le, trunc_zero]
  . apply hfut hxw hwt hfw
    rewrite [hfx']
    trans t
    . exact hwt.le
    . exact htx'
| inr htw => constructor
  . exact s₁ npos htw hwy hft hfy hfw hfty
  . rw [tsub_eq_zero_of_le htw, trunc_zero]
State after:
no goals

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
⊢ t = y - round (y - z)
Tactic:
rewrite [ht]
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
⊢ round (y - round (y - z)) = y - round (y - z)

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
⊢ round (y - round (y - z)) = y - round (y - z)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
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
⊢ trunc n (y - round (y - z)) = y - round (y - z)

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
⊢ trunc n (y - round (y - z)) = y - round (y - z)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfy hfz hzy
State after:
no goals

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)
⊢ round (y - z) ≤ y
Tactic:
trans round (y - 0)
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)
⊢ round (y - z) ≤ round (y - 0)

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)
⊢ round (y - 0) ≤ y

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)
⊢ round (y - z) ≤ round (y - 0)

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)
⊢ round (y - 0) ≤ y
Tactic:
. exact hml (trunc_zero n) hfz hfy (Nat.zero_le _)
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)
⊢ round (y - 0) ≤ y

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)
⊢ round (y - 0) ≤ y
Tactic:
. rw [tsub_zero, round_eq_of_trunc_eq npos hfaithful₀ hfy]
State after:
no goals

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)
⊢ round (y - z) ≤ round (y - 0)
Tactic:
exact hml (trunc_zero n) hfz hfy (Nat.zero_le _)
State after:
no goals

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)
⊢ round (y - 0) ≤ y
Tactic:
rw [tsub_zero, round_eq_of_trunc_eq npos hfaithful₀ hfy]
State after:
no goals

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
⊢ round (y - round (y - x)) = y - round (y - x)
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
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
⊢ trunc n (y - round (y - x)) = y - round (y - x)

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
⊢ trunc n (y - round (y - x)) = y - round (y - x)
Tactic:
exact s₂ npos hfaithful₀ hfaithful₁ hfy hfx hxy
State after:
no goals

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 (t - u) = t - u
Tactic:
have hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u := by
  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
  rewrite [← hfx']
  exact s₃ npos hfaithful₀ hfaithful₁ hfy hfx hfu hxy hxu hyxulp hxyx hux'
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))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
⊢ trunc n (t - u) = t - u

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))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
⊢ trunc n (t - u) = t - u
Tactic:
rewrite [ht] at hut htx' ⊢
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' : round (y - round (y - z)) ≤ 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 < round (y - round (y - z))
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
⊢ trunc n (round (y - round (y - z)) - u) = round (y - round (y - z)) - u

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' : round (y - round (y - z)) ≤ 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 < round (y - round (y - z))
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
⊢ trunc n (round (y - round (y - z)) - u) = round (y - round (y - z)) - u
Tactic:
replace hfx' := trunc_eq_of_round_eq npos hfaithful₁ hfx'
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' : round (y - round (y - z)) ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
u : ℕ
hxu : x ≤ u
hut : u < round (y - round (y - z))
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
hfx' : trunc n (y - round (y - x)) = y - round (y - x)
⊢ trunc n (round (y - round (y - z)) - u) = round (y - round (y - z)) - u

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' : round (y - round (y - z)) ≤ y - round (y - x)
hzy' : round (y - z) ≤ y
hft : trunc n t = t
u : ℕ
hxu : x ≤ u
hut : u < round (y - round (y - z))
hfu : trunc n u = u
hux' : u ≤ round (y - round (y - x))
hfuxy : trunc n (y - round (y - x) - u) = y - round (y - x) - u
hfx' : trunc n (y - round (y - x)) = y - round (y - x)
⊢ trunc n (round (y - round (y - z)) - u) = round (y - round (y - z)) - u
Tactic:
exact s₁ npos hut.le htx' hfu hfx' (trunc_round npos hfaithful₁ _) hfuxy
State after:
no goals

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
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

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']
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

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'
State after:
no goals

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₁]
State after:
no goals

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]
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

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]
State after:
no goals

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'
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

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]
State after:
no goals

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₀
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

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
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))

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']
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)

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'
State after:
no goals

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
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

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]
State after:
no goals

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₀
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

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 ⊢
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))

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
State after:
no goals

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
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t ∧ trunc n (t - w) = t - w
Tactic:
constructor
State after:
case inl.left
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
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t

case inl.right
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
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w

State before:
case inl.left
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
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t

case inl.right
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
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w
Tactic:
. rw [tsub_eq_zero_of_le hwt.le, trunc_zero]
State after:
case inl.right
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
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w

State before:
case inl.right
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
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w
Tactic:
. apply hfut hxw hwt hfw
  rewrite [hfx']
  trans t
  . exact hwt.le
  . exact htx'
State after:
no goals

State before:
case inl.left
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
hst : s = t
hwt : w < t
⊢ trunc n (w - t) = w - t
Tactic:
rw [tsub_eq_zero_of_le hwt.le, trunc_zero]
State after:
no goals

State before:
case inl.right
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
hst : s = t
hwt : w < t
⊢ trunc n (t - w) = t - w
Tactic:
apply hfut hxw hwt hfw
State after:
case inl.right
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
hst : s = t
hwt : w < t
⊢ w ≤ round (y - round (y - x))

State before:
case inl.right
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
hst : s = t
hwt : w < t
⊢ w ≤ round (y - round (y - x))
Tactic:
rewrite [hfx']
State after:
case inl.right
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
hst : s = t
hwt : w < t
⊢ w ≤ y - round (y - x)

State before:
case inl.right
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
hst : s = t
hwt : w < t
⊢ w ≤ y - round (y - x)
Tactic:
trans t
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
hst : s = t
hwt : w < t
⊢ w ≤ t

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
hst : s = t
hwt : w < t
⊢ t ≤ y - round (y - x)

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
hst : s = t
hwt : w < t
⊢ w ≤ t

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
hst : s = t
hwt : w < t
⊢ t ≤ y - round (y - x)
Tactic:
. exact hwt.le
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
hst : s = t
hwt : w < t
⊢ t ≤ y - round (y - x)

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
hst : s = t
hwt : w < t
⊢ t ≤ y - round (y - x)
Tactic:
. exact htx'
State after:
no goals

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
hst : s = t
hwt : w < t
⊢ w ≤ t
Tactic:
exact hwt.le
State after:
no goals

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
hst : s = t
hwt : w < t
⊢ t ≤ y - round (y - x)
Tactic:
exact htx'
State after:
no goals

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
hst : s = t
htw : w ≥ t
⊢ trunc n (w - t) = w - t ∧ trunc n (t - w) = t - w
Tactic:
constructor
State after:
case inr.left
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
hst : s = t
htw : w ≥ t
⊢ trunc n (w - t) = w - t

case inr.right
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
hst : s = t
htw : w ≥ t
⊢ trunc n (t - w) = t - w

State before:
case inr.left
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
hst : s = t
htw : w ≥ t
⊢ trunc n (w - t) = w - t

case inr.right
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
hst : s = t
htw : w ≥ t
⊢ trunc n (t - w) = t - w
Tactic:
. exact s₁ npos htw hwy hft hfy hfw hfty
State after:
case inr.right
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
hst : s = t
htw : w ≥ t
⊢ trunc n (t - w) = t - w

State before:
case inr.right
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
hst : s = t
htw : w ≥ t
⊢ trunc n (t - w) = t - w
Tactic:
. rw [tsub_eq_zero_of_le htw, trunc_zero]
State after:
no goals

State before:
case inr.left
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
hst : s = t
htw : w ≥ t
⊢ trunc n (w - t) = w - t
Tactic:
exact s₁ npos htw hwy hft hfy hfw hfty
State after:
no goals

State before:
case inr.right
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
hst : s = t
htw : w ≥ t
⊢ trunc n (t - w) = t - w
Tactic:
rw [tsub_eq_zero_of_le htw, trunc_zero]
State after:
no goals