internlm/Lean-Github huggingface dataset:
Theorem: s₁'
Proof state before:
case succ.inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a - ulp n (b - w - 1)
Tactic:
apply Nat.dvd_sub'
Proof state after:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a

case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Theorem: s₁'
Proof state before:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a

case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
. calc ulp n (b - w - a - ulp n (b - w - 1))
    _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
    _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
Proof state after:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Theorem: s₁'
Proof state before:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
. apply ulp_dvd_ulp
  calc b - w - a - ulp n (b - w - 1)
    _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
    _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case succ.inl.h₁
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ b - w - a
Tactic:
calc ulp n (b - w - a - ulp n (b - w - 1))
  _ ∣ ulp n (b - w - a) := ulp_dvd_ulp n tsub_le_self
  _ ∣ b - w - a         := ulp_dvd_of_trunc_eq $ hfb₁ ▸ ih
Proof state after:
no goals
Theorem: s₁'
Proof state before:
case succ.inl.h₂
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ ulp n (b - w - a - ulp n (b - w - 1)) ∣ ulp n (b - w - 1)
Tactic:
apply ulp_dvd_ulp
Proof state after:
case succ.inl.h₂.h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ b - w - a - ulp n (b - w - 1) ≤ b - w - 1
Theorem: s₁'
Proof state before:
case succ.inl.h₂.h
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
hf : trunc n (b - a) = b - a
w : ℕ
h : 2 * a < b - Nat.succ w
ih : trunc n (trunc n (b - w) - a) = trunc n (b - w) - a
hfb₁ : trunc n (b - w) = b - w
bpos : 0 < b - w
⊢ b - w - a - ulp n (b - w - 1) ≤ b - w - 1
Tactic:
calc b - w - a - ulp n (b - w - 1)
  _ ≤ b - w - a - 1 := tsub_le_tsub_left (Nat.one_le_of_lt $ ulp_pos n _) _
  _ ≤ b - w - 1     := tsub_le_tsub_right tsub_le_self _
Proof state after:
no goals
Theorem: s₁
Proof state before:
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
⊢ trunc n (c - a) = c - a
Tactic:
cases le_or_gt c (2 * a) with
| inl hle => exact sterbenz hfc hfa hac hle
| inr hgt =>
  rewrite [← hfc]
  rewrite [← tsub_tsub_cancel_of_le hcb]
  apply s₁' npos hfb hf
  rewrite [tsub_tsub_cancel_of_le hcb]
  exact hgt
Proof state after:
no goals
Theorem: s₁
Proof state before:
case inl
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hle : c ≤ 2 * a
⊢ trunc n (c - a) = c - a
Tactic:
exact sterbenz hfc hfa hac hle
Proof state after:
no goals
Theorem: s₁
Proof state before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (c - a) = c - a
Tactic:
rewrite [← hfc]
Proof state after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n c - a) = trunc n c - a
Theorem: s₁
Proof state before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n c - a) = trunc n c - a
Tactic:
rewrite [← tsub_tsub_cancel_of_le hcb]
Proof state after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n (b - (b - c)) - a) = trunc n (b - (b - c)) - a
Theorem: s₁
Proof state before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ trunc n (trunc n (b - (b - c)) - a) = trunc n (b - (b - c)) - a
Tactic:
apply s₁' npos hfb hf
Proof state after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < b - (b - c)
Theorem: s₁
Proof state before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < b - (b - c)
Tactic:
rewrite [tsub_tsub_cancel_of_le hcb]
Proof state after:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < c
Theorem: s₁
Proof state before:
case inr
n a b c : ℕ
npos : 0 < n
hac : a ≤ c
hcb : c ≤ b
hfa : trunc n a = a
hfb : trunc n b = b
hfc : trunc n c = c
hf : trunc n (b - a) = b - a
hgt : c > 2 * a
⊢ 2 * a < c
Tactic:
exact hgt
Proof state after:
no goals
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
cases Nat.le_total (2 * b) a with
| inr hba' => have hf : round (a - b) = a - b := by
    apply hfaithful₀
    exact sterbenz hfa hfb hba hba'
  rewrite [hf, tsub_tsub_cancel_of_le hba]
  exact hfb
| inl hab' => apply sterbenz
  . exact hfa
  . exact trunc_round npos hfaithful₁ (a - b)
  . exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
  . have h : a ≤ 2 * (a - b) := by
      rewrite [Nat.mul_sub_left_distrib]
      rewrite [Nat.two_mul]
      rewrite [add_tsub_assoc_of_le hab']
      exact Nat.le_add_right _ _
    calc
      a = trunc n a             := by rw [hfa]
      _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
      _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
      _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
have hf : round (a - b) = a - b := by
  apply hfaithful₀
  exact sterbenz hfa hfb hba hba'
Proof state after:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Theorem: s₂
Proof state before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
rewrite [hf, tsub_tsub_cancel_of_le hba]
Proof state after:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n b = b
Theorem: s₂
Proof state before:
case inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
hf : round (a - b) = a - b
⊢ trunc n b = b
Tactic:
exact hfb
Proof state after:
no goals
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ round (a - b) = a - b
Tactic:
apply hfaithful₀
Proof state after:
case a
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
Theorem: s₂
Proof state before:
case a
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hba' : a ≤ 2 * b
⊢ trunc n (a - b) = a - b
Tactic:
exact sterbenz hfa hfb hba hba'
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (a - round (a - b)) = a - round (a - b)
Tactic:
apply sterbenz
Proof state after:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a

case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Theorem: s₂
Proof state before:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a

case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact hfa
Proof state after:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Theorem: s₂
Proof state before:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)

case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact trunc_round npos hfaithful₁ (a - b)
Proof state after:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Theorem: s₂
Proof state before:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a

case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
Proof state after:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Theorem: s₂
Proof state before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
. have h : a ≤ 2 * (a - b) := by
    rewrite [Nat.mul_sub_left_distrib]
    rewrite [Nat.two_mul]
    rewrite [add_tsub_assoc_of_le hab']
    exact Nat.le_add_right _ _
  calc
    a = trunc n a             := by rw [hfa]
    _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
    _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
    _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inl.hfa
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n a = a
Tactic:
exact hfa
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inl.hfb
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ trunc n (round (a - b)) = round (a - b)
Tactic:
exact trunc_round npos hfaithful₁ (a - b)
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inl.hba
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ round (a - b) ≤ a
Tactic:
exact round_sub_le npos hfaithful₀ hfaithful₁ b hfa
Proof state after:
no goals
Theorem: s₂
Proof state before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * round (a - b)
Tactic:
have h : a ≤ 2 * (a - b) := by
  rewrite [Nat.mul_sub_left_distrib]
  rewrite [Nat.two_mul]
  rewrite [add_tsub_assoc_of_le hab']
  exact Nat.le_add_right _ _
Proof state after:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)
Theorem: s₂
Proof state before:
case inl.hab
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a ≤ 2 * round (a - b)
Tactic:
calc
  a = trunc n a             := by rw [hfa]
  _ ≤ trunc n (2 * (a - b)) := trunc_le_trunc npos h
  _ = 2 * trunc n (a - b)   := by rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
  _ ≤ 2 * round (a - b)     := Nat.mul_le_mul_left _ (trunc_le_round n _ hfaithful₁)
Proof state after:
no goals
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * (a - b)
Tactic:
rewrite [Nat.mul_sub_left_distrib]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * a - 2 * b
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ 2 * a - 2 * b
Tactic:
rewrite [Nat.two_mul]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + a - 2 * b
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + a - 2 * b
Tactic:
rewrite [add_tsub_assoc_of_le hab']
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + (a - 2 * b)
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
⊢ a ≤ a + (a - 2 * b)
Tactic:
exact Nat.le_add_right _ _
Proof state after:
no goals
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ a = trunc n a
Tactic:
rw [hfa]
Proof state after:
no goals
Theorem: s₂
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
hab' : 2 * b ≤ a
h : a ≤ 2 * (a - b)
⊢ trunc n (2 * (a - b)) = 2 * trunc n (a - b)
Tactic:
rw [← pow_one 2, ← trunc_pow_mul npos, pow_one]
Proof state after:
no goals
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
cases Nat.le_total a (ulp n b) with
| inl le_ulp => trans ulp n b
  . rewrite [tsub_le_iff_tsub_le]
    calc
      b - ulp n b
      _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
      _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
  . exact h
| inr ulp_le => rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
  calc
    b - a ≤ next n (trunc n (b - a))    := Nat.le_of_lt $ lt_next_trunc npos _
    _ = trunc n (b - a) + ulp n (b - a) := by unfold next ; rw [ulp_trunc npos _]
    _ ≤ trunc n (b - a) + ulp n b       := Nat.add_le_add_left (ulp_le_ulp n tsub_le_self) _
    _ ≤ trunc n (b - a) + a             := Nat.add_le_add_left ulp_le _
Proof state after:
no goals
Theorem: s₃'
Proof state before:
case inl
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
trans ulp n b
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b

n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b

n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
. rewrite [tsub_le_iff_tsub_le]
  calc
    b - ulp n b
    _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
    _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
. exact h
Proof state after:
no goals
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - trunc n (b - a) ≤ ulp n b
Tactic:
rewrite [tsub_le_iff_tsub_le]
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - ulp n b ≤ trunc n (b - a)
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ b - ulp n b ≤ trunc n (b - a)
Tactic:
calc
  b - ulp n b
  _ = trunc n (b - ulp n b) := Eq.symm $ trunc_sub_ulp_eq_of_trunc_eq npos hfb
  _ ≤ trunc n (b - a)       := trunc_le_trunc npos $ tsub_le_tsub_left le_ulp _
Proof state after:
no goals
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
le_ulp : a ≤ ulp n b
⊢ ulp n b ≤ 2 * a
Tactic:
exact h
Proof state after:
no goals
Theorem: s₃'
Proof state before:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - trunc n (b - a) ≤ 2 * a
Tactic:
rewrite [Nat.two_mul, ← tsub_le_iff_right, tsub_right_comm, tsub_le_iff_left]
Proof state after:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - a ≤ trunc n (b - a) + a
Theorem: s₃'
Proof state before:
case inr
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ b - a ≤ trunc n (b - a) + a
Tactic:
calc
  b - a ≤ next n (trunc n (b - a))    := Nat.le_of_lt $ lt_next_trunc npos _
  _ = trunc n (b - a) + ulp n (b - a) := by unfold next ; rw [ulp_trunc npos _]
  _ ≤ trunc n (b - a) + ulp n b       := Nat.add_le_add_left (ulp_le_ulp n tsub_le_self) _
  _ ≤ trunc n (b - a) + a             := Nat.add_le_add_left ulp_le _
Proof state after:
no goals
Theorem: s₃'
Proof state before:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ next n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)
Tactic:
unfold next
Proof state after:
n a b : ℕ
npos : 0 < n
hfb : trunc n b = b
h : ulp n b ≤ 2 * a
ulp_le : ulp n b ≤ a
⊢ trunc n (b - a) + ulp n (trunc n (b - a)) = trunc n (b - a) + ulp n (b - a)