Theorem: Nat.le_pow2_log2RU_self (Algdata/Data/Nat/Bits.lean)

State before:
n : Nat
⊢ n ≤ 2 ^ log2RU n
Tactic:
cases Nat.lt_or_ge (2^log2RU n) n
State after:
case inl
n : Nat
h✝ : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n

case inr
n : Nat
h✝ : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n

State before:
n : Nat
hge : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n
Tactic:
case inr hge => exact hge
State after:
no goals

State before:
n : Nat
hlt : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n
Tactic:
case inl hlt =>
  have : n.log2RU < n.log2RU := Nat.lt_log2RU_iff_pow2_lt.mpr hlt
  exact absurd this (Nat.lt_irrefl _)
State after:
no goals

State before:
n : Nat
hge : 2 ^ log2RU n ≥ n
⊢ n ≤ 2 ^ log2RU n
Tactic:
exact hge
State after:
no goals

State before:
n : Nat
hlt : 2 ^ log2RU n < n
⊢ n ≤ 2 ^ log2RU n
Tactic:
have : n.log2RU < n.log2RU := Nat.lt_log2RU_iff_pow2_lt.mpr hlt
State after:
n : Nat
hlt : 2 ^ log2RU n < n
this : log2RU n < log2RU n
⊢ n ≤ 2 ^ log2RU n

State before:
n : Nat
hlt : 2 ^ log2RU n < n
this : log2RU n < log2RU n
⊢ n ≤ 2 ^ log2RU n
Tactic:
exact absurd this (Nat.lt_irrefl _)
State after:
no goals