Theorem: size_trunc_eq_size (Fl/Trunc.lean)

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (trunc n x) = Nat.size x
Tactic:
unfold trunc ulp expt
State after:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x

State before:
n : ℕ
npos : 0 < n
x : ℕ
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
cases Nat.eq_zero_or_pos x with
| inl zero => rw [zero, Nat.zero_div, Nat.zero_mul]
| inr pos =>
  apply size_div_mul
  rewrite [← Nat.lt_size]
  exact tsub_lt_self (Nat.size_pos.mpr pos) npos
State after:
no goals

State before:
case inl
n : ℕ
npos : 0 < n
x : ℕ
zero : x = 0
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
rw [zero, Nat.zero_div, Nat.zero_mul]
State after:
no goals

State before:
case inr
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size (x / 2 ^ (Nat.size x - n) * 2 ^ (Nat.size x - n)) = Nat.size x
Tactic:
apply size_div_mul
State after:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ 2 ^ (Nat.size x - n) ≤ x

State before:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ 2 ^ (Nat.size x - n) ≤ x
Tactic:
rewrite [← Nat.lt_size]
State after:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size x - n < Nat.size x

State before:
case inr.h
n : ℕ
npos : 0 < n
x : ℕ
pos : x > 0
⊢ Nat.size x - n < Nat.size x
Tactic:
exact tsub_lt_self (Nat.size_pos.mpr pos) npos
State after:
no goals