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

State before:
k : Nat
⊢ log2' (2 ^ k) = k
Tactic:
induction k
State after:
case zero

⊢ log2' (2 ^ zero) = zero

case succ
n✝ : Nat
n_ih✝ : log2' (2 ^ n✝) = n✝
⊢ log2' (2 ^ succ n✝) = succ n✝

State before:
⊢ log2' (2 ^ zero) = zero
Tactic:
case zero => exact log2'_one
State after:
no goals

State before:
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ log2' (2 ^ succ k) = succ k
Tactic:
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
  ]
State after:
no goals

State before:
⊢ log2' (2 ^ zero) = zero
Tactic:
exact log2'_one
State after:
no goals

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

State before:
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ 0 < 2
Tactic:
decide
State after:
no goals