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

State before:
k n : Nat
⊢ k < log2RU n ↔ 2 ^ k < n
Tactic:
cases n
State after:
case zero
k : Nat
⊢ k < log2RU zero ↔ 2 ^ k < zero

case succ
k n✝ : Nat
⊢ k < log2RU (succ n✝) ↔ 2 ^ k < succ n✝

State before:
k : Nat
⊢ k < log2RU zero ↔ 2 ^ k < zero
Tactic:
case zero =>
  conv => lhs; rhs; reduce
  constructor <;> (intro h; cases h)
State after:
no goals

State before:
k n : Nat
⊢ k < log2RU (succ n) ↔ 2 ^ k < succ n
Tactic:
case succ n =>
  dsimp [log2RU]; simp [log2RU]
  cases n
  case zero =>
    conv => lhs; rhs; reduce
    constructor
    . intro h; cases h
    . intro hlt1
      have : 2^k > 0 := Nat.pos_pow_of_pos k (by decide)
      exact absurd hlt1 (Nat.not_lt_of_le this)
  case succ n =>
    rw [log2'_mul2]
    have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
      λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
    rw [this, this]
    exact le_log2'_iff_pow2_le n.zero_lt_succ
State after:
no goals

State before:
k : Nat
⊢ k < log2RU zero ↔ 2 ^ k < zero
Tactic:
conv => lhs; rhs; reduce
State after:
k : Nat
⊢ k < 0 ↔ 2 ^ k < zero

State before:
k : Nat
⊢ k < 0 ↔ 2 ^ k < zero
Tactic:
constructor <;> (intro h; cases h)
State after:
no goals

State before:
case mpr
k : Nat
⊢ 2 ^ k < zero → k < 0
Tactic:
intro h
State after:
case mpr
k : Nat
h : 2 ^ k < zero
⊢ k < 0

State before:
case mpr
k : Nat
h : 2 ^ k < zero
⊢ k < 0
Tactic:
cases h
State after:
no goals

State before:
k n : Nat
⊢ k < log2RU (succ n) ↔ 2 ^ k < succ n
Tactic:
dsimp [log2RU]
State after:
k n : Nat
⊢ k < log2' (2 * (succ n - 1)) ↔ 2 ^ k < succ n

State before:
k n : Nat
⊢ k < log2' (2 * (succ n - 1)) ↔ 2 ^ k < succ n
Tactic:
simp [log2RU]
State after:
k n : Nat
⊢ k < log2' (2 * n) ↔ 2 ^ k < succ n

State before:
k n : Nat
⊢ k < log2' (2 * n) ↔ 2 ^ k < succ n
Tactic:
cases n
State after:
case zero
k : Nat
⊢ k < log2' (2 * zero) ↔ 2 ^ k < succ zero

case succ
k n✝ : Nat
⊢ k < log2' (2 * succ n✝) ↔ 2 ^ k < succ (succ n✝)

State before:
k : Nat
⊢ k < log2' (2 * zero) ↔ 2 ^ k < succ zero
Tactic:
case zero =>
  conv => lhs; rhs; reduce
  constructor
  . intro h; cases h
  . intro hlt1
    have : 2^k > 0 := Nat.pos_pow_of_pos k (by decide)
    exact absurd hlt1 (Nat.not_lt_of_le this)
State after:
no goals

State before:
k n : Nat
⊢ k < log2' (2 * succ n) ↔ 2 ^ k < succ (succ n)
Tactic:
case succ n =>
  rw [log2'_mul2]
  have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
    λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
  rw [this, this]
  exact le_log2'_iff_pow2_le n.zero_lt_succ
State after:
no goals

State before:
k : Nat
⊢ k < log2' (2 * zero) ↔ 2 ^ k < succ zero
Tactic:
conv => lhs; rhs; reduce
State after:
k : Nat
⊢ k < 0 ↔ 2 ^ k < succ zero

State before:
k : Nat
⊢ k < 0 ↔ 2 ^ k < succ zero
Tactic:
constructor
State after:
case mp
k : Nat
⊢ k < 0 → 2 ^ k < succ zero

case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0

State before:
case mp
k : Nat
⊢ k < 0 → 2 ^ k < succ zero

case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Tactic:
. intro h; cases h
State after:
case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0

State before:
case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Tactic:
. intro hlt1
  have : 2^k > 0 := Nat.pos_pow_of_pos k (by decide)
  exact absurd hlt1 (Nat.not_lt_of_le this)
State after:
no goals

State before:
case mp
k : Nat
⊢ k < 0 → 2 ^ k < succ zero
Tactic:
intro h
State after:
case mp
k : Nat
h : k < 0
⊢ 2 ^ k < succ zero

State before:
case mp
k : Nat
h : k < 0
⊢ 2 ^ k < succ zero
Tactic:
cases h
State after:
no goals

State before:
case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Tactic:
intro hlt1
State after:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
⊢ k < 0

State before:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
⊢ k < 0
Tactic:
have : 2^k > 0 := Nat.pos_pow_of_pos k (by decide)
State after:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
this : 2 ^ k > 0
⊢ k < 0

State before:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
this : 2 ^ k > 0
⊢ k < 0
Tactic:
exact absurd hlt1 (Nat.not_lt_of_le this)
State after:
no goals

State before:
k : Nat
hlt1 : 2 ^ k < succ zero
⊢ 0 < 2
Tactic:
decide
State after:
no goals

State before:
k n : Nat
⊢ k < log2' (2 * succ n) ↔ 2 ^ k < succ (succ n)
Tactic:
rw [log2'_mul2]
State after:
k n : Nat
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)

State before:
k n : Nat
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
Tactic:
have : ∀ (a b : Nat), (a < b+1) = (a ≤ b) :=
  λ a b => propext ⟨Nat.le_of_lt_succ, Nat.lt_succ_of_le⟩
State after:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)

State before:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)
Tactic:
rw [this, this]
State after:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k ≤ log2' (succ n) ↔ 2 ^ k ≤ n + 1

State before:
k n : Nat
this : ∀ (a b : Nat), (a < b + 1) = (a ≤ b)
⊢ k ≤ log2' (succ n) ↔ 2 ^ k ≤ n + 1
Tactic:
exact le_log2'_iff_pow2_le n.zero_lt_succ
State after:
no goals