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

State before:
n : Nat
⊢ log2' n = log2 n
Tactic:
unfold log2'
State after:
n : Nat
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) n = log2 n

State before:
n : Nat
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) n = log2 n
Tactic:
induction n using recBase2
State after:
case zero

⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0

case one

⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1

case div2
n✝ : Nat
a✝ : recBase2 0 0 (fun x x_1 => x_1 + 1) (n✝ / 2 + 1) = log2 (n✝ / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n✝ + 2) = log2 (n✝ + 2)

State before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0
Tactic:
case zero => rfl
State after:
no goals

State before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1
Tactic:
case one => rfl
State after:
no goals

State before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
Tactic:
case div2 n h_ind =>
  rw [recBase2_div2, h_ind]
  conv =>
    rhs; unfold log2; rw [if_pos (Nat.le_add_left 2 n), Nat.add_div_right n (Nat.zero_lt_succ 1)]
State after:
no goals

State before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 0 = log2 0
Tactic:
rfl
State after:
no goals

State before:
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) 1 = log2 1
Tactic:
rfl
State after:
no goals

State before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (n + 2) = log2 (n + 2)
Tactic:
rw [recBase2_div2, h_ind]
State after:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ log2 (n / 2 + 1) + 1 = log2 (n + 2)

State before:
n : Nat
h_ind : recBase2 0 0 (fun x x_1 => x_1 + 1) (n / 2 + 1) = log2 (n / 2 + 1)
⊢ log2 (n / 2 + 1) + 1 = log2 (n + 2)
Tactic:
conv =>
  rhs; unfold log2; rw [if_pos (Nat.le_add_left 2 n), Nat.add_div_right n (Nat.zero_lt_succ 1)]
State after:
no goals