case succ k h_ind =>
  rw [
    Nat.pow_succ, Nat.mul_comm,
    log2'_mul2_of_pos (Nat.pos_pow_of_pos k (by decide)),
    h_ind
  ]
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ log2' (2 ^ succ k) = succ k
no goals