Theorem: size_mul_pow (Fl/Lemmas.lean)

State before:
x : ℕ
h : 0 < x
k : ℕ
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k
Tactic:
have nz : x ≠ 0 := by rwa [← Nat.pos_iff_ne_zero]
State after:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k

State before:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x * 2 ^ k) = Nat.size x + k
Tactic:
rewrite [← Nat.shiftLeft_eq_mul_pow x k]
State after:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x <<< k) = Nat.size x + k

State before:
x : ℕ
h : 0 < x
k : ℕ
nz : x ≠ 0
⊢ Nat.size (x <<< k) = Nat.size x + k
Tactic:
rw [Nat.size_shiftLeft nz]
State after:
no goals

State before:
x : ℕ
h : 0 < x
k : ℕ
⊢ x ≠ 0
Tactic:
rwa [← Nat.pos_iff_ne_zero]
State after:
no goals