Theorem: Nat.le_log2'_iff_pow2_le (Algdata/Data/Nat/Bits.lean)

State before:
k n : Nat
⊢ n > 0 → (k ≤ log2' n ↔ 2 ^ k ≤ n)
Tactic:
intros
State after:
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n ↔ 2 ^ k ≤ n

State before:
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n ↔ 2 ^ k ≤ n
Tactic:
constructor
State after:
case mp
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n → 2 ^ k ≤ n

case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n

State before:
case mp
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n → 2 ^ k ≤ n

case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n
Tactic:
. intro h
  calc
    2^k ≤ 2^n.log2' := Nat.pow_le_pow_of_le_right (by decide) h
    _   ≤ n         := Nat.pow2_log2'_le_self ‹n>0›
State after:
case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n

State before:
case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n
Tactic:
. intro h
  calc
    k = log2' (2^k) := Eq.symm (log2'_pow2 k)
    _ ≤ log2' n     := log2'_le_log2' h
State after:
no goals

State before:
case mp
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n → 2 ^ k ≤ n
Tactic:
intro h
State after:
case mp
k n : Nat
a✝ : n > 0
h : k ≤ log2' n
⊢ 2 ^ k ≤ n

State before:
case mp
k n : Nat
a✝ : n > 0
h : k ≤ log2' n
⊢ 2 ^ k ≤ n
Tactic:
calc
  2^k ≤ 2^n.log2' := Nat.pow_le_pow_of_le_right (by decide) h
  _   ≤ n         := Nat.pow2_log2'_le_self ‹n>0›
State after:
no goals

State before:
k n : Nat
a✝ : n > 0
h : k ≤ log2' n
⊢ 2 > 0
Tactic:
decide
State after:
no goals

State before:
case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n
Tactic:
intro h
State after:
case mpr
k n : Nat
a✝ : n > 0
h : 2 ^ k ≤ n
⊢ k ≤ log2' n

State before:
case mpr
k n : Nat
a✝ : n > 0
h : 2 ^ k ≤ n
⊢ k ≤ log2' n
Tactic:
calc
  k = log2' (2^k) := Eq.symm (log2'_pow2 k)
  _ ≤ log2' n     := log2'_le_log2' h
State after:
no goals