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

State before:
n : Nat
⊢ n > 0 → 2 ^ log2' n ≤ n
Tactic:
intro h
State after:
n : Nat
h : n > 0
⊢ 2 ^ log2' n ≤ n

State before:
n : Nat
h : n > 0
⊢ 2 ^ log2' n ≤ n
Tactic:
induction n using recBase2
State after:
case zero
h : 0 > 0
⊢ 2 ^ log2' 0 ≤ 0

case one
h : 1 > 0
⊢ 2 ^ log2' 1 ≤ 1

case div2
n✝ : Nat
a✝ : n✝ / 2 + 1 > 0 → 2 ^ log2' (n✝ / 2 + 1) ≤ n✝ / 2 + 1
h : n✝ + 2 > 0
⊢ 2 ^ log2' (n✝ + 2) ≤ n✝ + 2

State before:
h : 0 > 0
⊢ 2 ^ log2' 0 ≤ 0
Tactic:
case zero => cases h
State after:
no goals

State before:
h : 1 > 0
⊢ 2 ^ log2' 1 ≤ 1
Tactic:
case one => exact .refl
State after:
no goals

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → 2 ^ log2' (n / 2 + 1) ≤ n / 2 + 1
h : n + 2 > 0
⊢ 2 ^ log2' (n + 2) ≤ n + 2
Tactic:
case div2 n h_ind =>
  rw [log2'_div2]
  show 2^(log2' (n/2+1) + 1) ≤ n+2
  calc
    2^(log2' (n/2+1) + 1)
      = 2^(log2' (n/2+1)) * 2 := Nat.pow_succ 2 _
    _ ≤ (n/2+1) * 2 := Nat.mul_le_mul_right 2 (h_ind $ Nat.zero_lt_succ _)
    _ = n/2*2 + 2 := Nat.add_mul _ 1 2
    _ ≤ n+2 := Nat.add_le_add_right (Nat.div_mul_le_self n 2) 2
State after:
no goals

State before:
h : 0 > 0
⊢ 2 ^ log2' 0 ≤ 0
Tactic:
cases h
State after:
no goals

State before:
h : 1 > 0
⊢ 2 ^ log2' 1 ≤ 1
Tactic:
exact .refl
State after:
no goals

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → 2 ^ log2' (n / 2 + 1) ≤ n / 2 + 1
h : n + 2 > 0
⊢ 2 ^ log2' (n + 2) ≤ n + 2
Tactic:
rw [log2'_div2]
State after:
n : Nat
h_ind : n / 2 + 1 > 0 → 2 ^ log2' (n / 2 + 1) ≤ n / 2 + 1
h : n + 2 > 0
⊢ 2 ^ (log2' (n / 2 + 1) + 1) ≤ n + 2

State before:
n : Nat
h_ind : n / 2 + 1 > 0 → 2 ^ log2' (n / 2 + 1) ≤ n / 2 + 1
h : n + 2 > 0
⊢ 2 ^ (log2' (n / 2 + 1) + 1) ≤ n + 2
Tactic:
calc
  2^(log2' (n/2+1) + 1)
    = 2^(log2' (n/2+1)) * 2 := Nat.pow_succ 2 _
  _ ≤ (n/2+1) * 2 := Nat.mul_le_mul_right 2 (h_ind $ Nat.zero_lt_succ _)
  _ = n/2*2 + 2 := Nat.add_mul _ 1 2
  _ ≤ n+2 := Nat.add_le_add_right (Nat.div_mul_le_self n 2) 2
State after:
no goals