internlm/Lean-Github huggingface dataset:
Theorem: b₁
Proof state before:
case inr.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
Proof state after:
case inr.inr.inl.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
eq_round : a - b = round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
eq_round : a - b = round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. constructor
  . exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
  . exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
      hfa hfb two_mul_lt.le lt_round
Proof state after:
case inr.inr.inl.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
eq_round : a - b = round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
eq_round : a - b = round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)

case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. exact b₁_of_round_eq eq_round.symm
Proof state after:
case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. constructor
  . cases Nat.lt_or_ge b (ulp n (a - b)) with
    | inl lt_ulp =>
      cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
      | inl ulp_eq_ulp =>
        exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
          npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
          round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
      | inr ulp_lt_ulp =>
        exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
          npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
          round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
    | inr ulp_le =>
      exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
        hfa hfb round_lt.le two_mul_lt.le ulp_le
  . exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
constructor
Proof state after:
case inr.inr.inl.inl.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

case inr.inr.inl.inl.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inl.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

case inr.inr.inl.inl.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
Proof state after:
case inr.inr.inl.inl.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inl.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
    hfa hfb two_mul_lt.le lt_round
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inl.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
exact b₁_lo_of_lt_round npos hfaithful₁ lt_round
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inl.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
lt_round : a - b < round (a - b)
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
exact b₁_hi_of_two_mul_le_of_lt_round npos hfaithful₀ hfaithful₁
  hfa hfb two_mul_lt.le lt_round
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
eq_round : a - b = round (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
exact b₁_of_round_eq eq_round.symm
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b) ∧ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
constructor
Proof state after:
case inr.inr.inl.inr.inr.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

case inr.inr.inl.inr.inr.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)

case inr.inr.inl.inr.inr.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. cases Nat.lt_or_ge b (ulp n (a - b)) with
  | inl lt_ulp =>
    cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
    | inl ulp_eq_ulp =>
      exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
        npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
        round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
    | inr ulp_lt_ulp =>
      exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
        npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
        round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
  | inr ulp_le =>
    exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
      hfa hfb round_lt.le two_mul_lt.le ulp_le
Proof state after:
case inr.inr.inl.inr.inr.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
. exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
cases Nat.lt_or_ge b (ulp n (a - b)) with
| inl lt_ulp =>
  cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
  | inl ulp_eq_ulp =>
    exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
      npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
      round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
  | inr ulp_lt_ulp =>
    exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
      npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
      round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
| inr ulp_le =>
  exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
    hfa hfb round_lt.le two_mul_lt.le ulp_le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
lt_ulp : b < ulp n (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
cases Nat.eq_or_lt_of_le (ulp_le_ulp n tsub_le_self) with
| inl ulp_eq_ulp =>
  exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
    npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
    round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
| inr ulp_lt_ulp =>
  exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
    npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
    round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left.inl.inl
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
lt_ulp : b < ulp n (a - b)
ulp_eq_ulp : ulp n (?m.56812 - ?m.56813) = ulp n ?m.56812
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_eq_ulp_of_two_mul_lt_of_pos_of_le_ulp
  npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
  round_lt no_uflow ulp_eq_ulp bpos (ulp_eq_ulp ▸ lt_ulp.le)
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left.inl.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
lt_ulp : b < ulp n (a - b)
ulp_lt_ulp : ulp n (a - b) < ulp n a
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
exact b₁_lo_of_round_lt_of_no_uflow_of_ulp_lt_ulp_of_two_mul_lt_of_pos_of_le_ulp
  npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
  round_lt no_uflow ulp_lt_ulp two_mul_lt bpos lt_ulp.le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.left.inr
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
ulp_le : b ≥ ulp n (a - b)
⊢ trunc n (a - b - round (a - b)) = a - b - round (a - b)
Tactic:
exact b₁_lo_of_round_le_of_two_mul_le_of_ulp_le npos hfaithful₁
  hfa hfb round_lt.le two_mul_lt.le ulp_le
Proof state after:
no goals
Theorem: b₁
Proof state before:
case inr.inr.inl.inr.inr.right
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
no_uflow : a - b ≥ 2 ^ n
bpos : b > 0
two_mul_lt : 2 * b < a
round_lt : round (a - b) < a - b
⊢ trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
Tactic:
exact b₁_hi_of_round_le npos hfaithful₁ round_lt.le
Proof state after:
no goals
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have ⟨hfr₁, _⟩ := b₁ npos hfaithful₀ hfaithful₁ hcorrect₀ hfa hfb hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have hfe : round (a - round (a - b)) = a - round (a - b) := by
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact s₂ npos hfaithful₀ hfaithful₁ hfa hfb hba
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
have hfr : round (a - b - round (a - b)) = a - b - round (a - b) :=
  round_eq_of_trunc_eq npos hfaithful₀ $ hfr₁
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Theorem: sum_and_error₂_lo
Proof state before:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (round (a - round (a - b)) - b) = a - b
Tactic:
rewrite [hfe]
Proof state after:
round : ℕ → ℕ
n a b : ℕ
npos : 0 < n
hfaithful₀ : faithful₀ n round
hfaithful₁ : faithful₁ n round
hcorrect₀ : correct₀ n round
hfa : trunc n a = a
hfb : trunc n b = b
hba : b ≤ a
round_le : round (a - b) ≤ a - b
hfr₁ : trunc n (a - b - round (a - b)) = a - b - round (a - b)
right✝ : trunc n (round (a - b) - (a - b)) = round (a - b) - (a - b)
hfe : round (a - round (a - b)) = a - round (a - b)
hfr : round (a - b - round (a - b)) = a - b - round (a - b)
⊢ round (a - b) + round (a - round (a - b) - b) = a - b