Theorem: ulp_pow_mul (Fl/Trunc.lean)

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

State before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Tactic:
have pos : 0 < x := by
  rewrite [← Nat.size_pos]
  exact Nat.lt_of_lt_of_le npos h
State after:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)

State before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
pos : 0 < x
⊢ 2 ^ (Nat.size (2 ^ k * x) - n) = 2 ^ k * 2 ^ (Nat.size x - n)
Tactic:
rw [← pow_add, size_pow_mul pos, ← tsub_add_eq_add_tsub h, Nat.add_comm]
State after:
no goals

State before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < x
Tactic:
rewrite [← Nat.size_pos]
State after:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < Nat.size x

State before:
n x : ℕ
npos : 0 < n
h : n ≤ Nat.size x
k : ℕ
⊢ 0 < Nat.size x
Tactic:
exact Nat.lt_of_lt_of_le npos h
State after:
no goals