Theorem: trunc_next_of_carry (Fl/Trunc.lean)

State before:
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ trunc n (next n x) = 2 ^ Nat.size x
Tactic:
apply div_mul_eq_of_le_of_lt
State after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. unfold expt
  rewrite [size_next_eq_succ_size_of_carry carry]
  rewrite [tsub_le_iff_tsub_le]
  rewrite [add_tsub_cancel_left]
  exact Nat.one_le_of_lt npos
State after:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)

State before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x

case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. exact carry
State after:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)

State before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
. apply add_lt_add_of_lt_of_le
  . exact Nat.lt_size_self x
  . apply ulp_le_ulp
    exact Nat.le_add_right x (2 ^ expt n x)
State after:
no goals

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ expt n (next n x) ≤ Nat.size x
Tactic:
unfold expt
State after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) - n ≤ Nat.size x

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size (next n x) - n ≤ Nat.size x
Tactic:
rewrite [size_next_eq_succ_size_of_carry carry]
State after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - n ≤ Nat.size x

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - n ≤ Nat.size x
Tactic:
rewrite [tsub_le_iff_tsub_le]
State after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - Nat.size x ≤ n

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ Nat.size x + 1 - Nat.size x ≤ n
Tactic:
rewrite [add_tsub_cancel_left]
State after:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 1 ≤ n

State before:
case h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 1 ≤ n
Tactic:
exact Nat.one_le_of_lt npos
State after:
no goals

State before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ 2 ^ Nat.size x ≤ next n x
Tactic:
exact carry
State after:
no goals

State before:
case a
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ next n x < 2 ^ Nat.size x + 2 ^ expt n (next n x)
Tactic:
apply add_lt_add_of_lt_of_le
State after:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x

case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)

State before:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x

case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
. exact Nat.lt_size_self x
State after:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)

State before:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
. apply ulp_le_ulp
  exact Nat.le_add_right x (2 ^ expt n x)
State after:
no goals

State before:
case a.h₁
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x < 2 ^ Nat.size x
Tactic:
exact Nat.lt_size_self x
State after:
no goals

State before:
case a.h₂
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ ulp n x ≤ 2 ^ expt n (next n x)
Tactic:
apply ulp_le_ulp
State after:
case a.h₂.h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x ≤ next n x

State before:
case a.h₂.h
n x : ℕ
npos : 0 < n
carry : 2 ^ Nat.size x ≤ next n x
⊢ x ≤ next n x
Tactic:
exact Nat.le_add_right x (2 ^ expt n x)
State after:
no goals