Theorem: b₁ (Fl.lean)

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
⊢ 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:
cases Nat.lt_or_ge (a - b) (2 ^ n) with
| inl uflow =>
  apply b₁_of_round_eq
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact trunc_eq_self_of_uflow uflow
| inr no_uflow =>
  cases Nat.eq_zero_or_pos b with
  | inl bzero =>
    apply b₁_of_round_eq
    rewrite [bzero, tsub_zero]
    exact round_eq_of_trunc_eq npos hfaithful₀ hfa
  | inr bpos =>
    cases Nat.lt_or_ge (2 * b) a with
    | inr le_two_mul =>
      apply b₁_of_round_eq
      apply round_eq_of_trunc_eq npos hfaithful₀
      exact sterbenz hfa hfb hba le_two_mul
    | inl two_mul_lt =>
      rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
      . 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
      . exact b₁_of_round_eq eq_round.symm
      . 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
State after:
no goals

State before:
case 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
uflow : a - b < 2 ^ n
⊢ 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:
apply b₁_of_round_eq
State after:
case inl.round_eq
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
uflow : a - b < 2 ^ n
⊢ round (a - b) = a - b

State before:
case inl.round_eq
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
uflow : a - b < 2 ^ n
⊢ round (a - b) = a - b
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
State after:
case inl.round_eq
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
uflow : a - b < 2 ^ n
⊢ trunc n (a - b) = a - b

State before:
case inl.round_eq
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
uflow : a - b < 2 ^ n
⊢ trunc n (a - b) = a - b
Tactic:
exact trunc_eq_self_of_uflow uflow
State after:
no goals

State before:
case 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
⊢ 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:
cases Nat.eq_zero_or_pos b with
| inl bzero =>
  apply b₁_of_round_eq
  rewrite [bzero, tsub_zero]
  exact round_eq_of_trunc_eq npos hfaithful₀ hfa
| inr bpos =>
  cases Nat.lt_or_ge (2 * b) a with
  | inr le_two_mul =>
    apply b₁_of_round_eq
    apply round_eq_of_trunc_eq npos hfaithful₀
    exact sterbenz hfa hfb hba le_two_mul
  | inl two_mul_lt =>
    rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
    . 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
    . exact b₁_of_round_eq eq_round.symm
    . 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
State after:
no goals

State before:
case 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
bzero : b = 0
⊢ 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:
apply b₁_of_round_eq
State after:
case inr.inl.round_eq
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
bzero : b = 0
⊢ round (a - b) = a - b

State before:
case inr.inl.round_eq
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
bzero : b = 0
⊢ round (a - b) = a - b
Tactic:
rewrite [bzero, tsub_zero]
State after:
case inr.inl.round_eq
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
bzero : b = 0
⊢ round a = a

State before:
case inr.inl.round_eq
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
bzero : b = 0
⊢ round a = a
Tactic:
exact round_eq_of_trunc_eq npos hfaithful₀ hfa
State after:
no goals

State before:
case 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
⊢ 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:
cases Nat.lt_or_ge (2 * b) a with
| inr le_two_mul =>
  apply b₁_of_round_eq
  apply round_eq_of_trunc_eq npos hfaithful₀
  exact sterbenz hfa hfb hba le_two_mul
| inl two_mul_lt =>
  rcases Nat.lt_trichotomy (a - b) (round (a - b)) with (lt_round | eq_round | round_lt)
  . 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
  . exact b₁_of_round_eq eq_round.symm
  . 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
State after:
no goals

State before:
case inr.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
le_two_mul : 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:
apply b₁_of_round_eq
State after:
case inr.inr.inr.round_eq
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
le_two_mul : 2 * b ≥ a
⊢ round (a - b) = a - b

State before:
case inr.inr.inr.round_eq
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
le_two_mul : 2 * b ≥ a
⊢ round (a - b) = a - b
Tactic:
apply round_eq_of_trunc_eq npos hfaithful₀
State after:
case inr.inr.inr.round_eq
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
le_two_mul : 2 * b ≥ a
⊢ trunc n (a - b) = a - b

State before:
case inr.inr.inr.round_eq
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
le_two_mul : 2 * b ≥ a
⊢ trunc n (a - b) = a - b
Tactic:
exact sterbenz hfa hfb hba le_two_mul
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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