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

State before:
n : Nat
⊢ log2' n ≤ n
Tactic:
induction n using recBase2
State after:
case zero

⊢ log2' 0 ≤ 0

case one

⊢ log2' 1 ≤ 1

case div2
n✝ : Nat
a✝ : log2' (n✝ / 2 + 1) ≤ n✝ / 2 + 1
⊢ log2' (n✝ + 2) ≤ n✝ + 2

State before:
⊢ log2' 0 ≤ 0
Tactic:
case zero => decide
State after:
no goals

State before:
⊢ log2' 1 ≤ 1
Tactic:
case one => decide
State after:
no goals

State before:
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n + 2) ≤ n + 2
Tactic:
case div2 n h_ind =>
  suffices log2' (n/2 + 1) ≤ n+1
    from log2'_div2 n ▸ Nat.succ_le_succ this
  calc
    log2' (n/2 + 1)
      ≤ n/2 + 1 := h_ind
    _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
State after:
no goals

State before:
⊢ log2' 0 ≤ 0
Tactic:
decide
State after:
no goals

State before:
⊢ log2' 1 ≤ 1
Tactic:
decide
State after:
no goals

State before:
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n + 2) ≤ n + 2
Tactic:
suffices log2' (n/2 + 1) ≤ n+1
  from log2'_div2 n ▸ Nat.succ_le_succ this
State after:
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n / 2 + 1) ≤ n + 1

State before:
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n / 2 + 1) ≤ n + 1
Tactic:
calc
  log2' (n/2 + 1)
    ≤ n/2 + 1 := h_ind
  _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
State after:
no goals