Theorem: Nat.log2'_mul2_of_pos (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
⊢ n > 0 → log2' (2 * n) = log2' n + 1
Tactic:
intro h
State after:
n : Nat
h : n > 0
⊢ log2' (2 * n) = log2' n + 1

State before:
n : Nat
h : n > 0
⊢ log2' (2 * n) = log2' n + 1
Tactic:
have : n = (n-1) + 1 := Eq.symm $ Nat.sub_add_cancel h
State after:
n : Nat
h : n > 0
this : n = n - 1 + 1
⊢ log2' (2 * n) = log2' n + 1

State before:
n : Nat
h : n > 0
this : n = n - 1 + 1
⊢ log2' (2 * n) = log2' n + 1
Tactic:
rw [this, log2'_mul2]
State after:
no goals