internlm/Lean-Github huggingface dataset:
Theorem: Nat.log2'_mul2
Proof state before:
n : Nat
⊢ log2' (2 * succ n) = log2' (succ n) + 1
Tactic:
conv =>
  lhs; rw [Nat.mul_succ 2 n]; unfold log2'; rw [recBase2_div2]
  change log2' (2*n/2 + 1) + 1
  rw [Nat.mul_div_right n (Nat.zero_lt_succ 1)]
Proof state after:
no goals
Theorem: Nat.log2'_mul2_of_pos
Proof state before:
n : Nat
⊢ n > 0 → log2' (2 * n) = log2' n + 1
Tactic:
intro h
Proof state after:
n : Nat
h : n > 0
⊢ log2' (2 * n) = log2' n + 1
Theorem: Nat.log2'_mul2_of_pos
Proof state before:
n : Nat
h : n > 0
⊢ log2' (2 * n) = log2' n + 1
Tactic:
have : n = (n-1) + 1 := Eq.symm $ Nat.sub_add_cancel h
Proof state after:
n : Nat
h : n > 0
this : n = n - 1 + 1
⊢ log2' (2 * n) = log2' n + 1
Theorem: Nat.log2'_mul2_of_pos
Proof state before:
n : Nat
h : n > 0
this : n = n - 1 + 1
⊢ log2' (2 * n) = log2' n + 1
Tactic:
rw [this, log2'_mul2]
Proof state after:
no goals
Theorem: Nat.log2'_pow2
Proof state before:
k : Nat
⊢ log2' (2 ^ k) = k
Tactic:
induction k
Proof state after:
case zero

⊢ log2' (2 ^ zero) = zero

case succ
n✝ : Nat
n_ih✝ : log2' (2 ^ n✝) = n✝
⊢ log2' (2 ^ succ n✝) = succ n✝
Theorem: Nat.log2'_pow2
Proof state before:
⊢ log2' (2 ^ zero) = zero
Tactic:
case zero => exact log2'_one
Proof state after:
no goals
Theorem: Nat.log2'_pow2
Proof state before:
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ log2' (2 ^ succ k) = succ k
Tactic:
case succ k h_ind =>
  rw [
    Nat.pow_succ, Nat.mul_comm,
    log2'_mul2_of_pos (Nat.pos_pow_of_pos k (by decide)),
    h_ind
  ]
Proof state after:
no goals
Theorem: Nat.log2'_pow2
Proof state before:
⊢ log2' (2 ^ zero) = zero
Tactic:
exact log2'_one
Proof state after:
no goals
Theorem: Nat.log2'_pow2
Proof state before:
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ log2' (2 ^ succ k) = succ k
Tactic:
rw [
  Nat.pow_succ, Nat.mul_comm,
  log2'_mul2_of_pos (Nat.pos_pow_of_pos k (by decide)),
  h_ind
]
Proof state after:
no goals
Theorem: Nat.log2'_pow2
Proof state before:
k : Nat
h_ind : log2' (2 ^ k) = k
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.zero_or_one_of_log2'
Proof state before:
n✝ : Nat
h : log2' (n✝ + 2) = 0
⊢ n✝ + 2 = 0 ∨ n✝ + 2 = 1
Tactic:
cases log2'_div2 _ ▸ h
Proof state after:
no goals
Theorem: Nat.ge_two_of_log2'
Proof state before:
h : log2' 0 > 0
⊢ 0 ≥ 2
Tactic:
cases log2'_zero ▸ h
Proof state after:
no goals
Theorem: Nat.ge_two_of_log2'
Proof state before:
h : log2' 1 > 0
⊢ 1 ≥ 2
Tactic:
cases log2'_one ▸ h
Proof state after:
no goals
Theorem: Nat.ge_two_of_log2'
Proof state before:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ n✝ + 2 ≥ 2
Tactic:
rw [Nat.add_comm]
Proof state after:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ 2 + n✝ ≥ 2
Theorem: Nat.ge_two_of_log2'
Proof state before:
n✝ : Nat
x✝ : log2' (n✝ + 2) > 0
⊢ 2 + n✝ ≥ 2
Tactic:
exact Nat.le.intro rfl
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof state before:
n : Nat
⊢ log2' n ≤ n
Tactic:
induction n using recBase2
Proof 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
Theorem: Nat.log2'_le_self
Proof state before:
⊢ log2' 0 ≤ 0
Tactic:
case zero => decide
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof state before:
⊢ log2' 1 ≤ 1
Tactic:
case one => decide
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof 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)
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof state before:
⊢ log2' 0 ≤ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof state before:
⊢ log2' 1 ≤ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2'_le_self
Proof 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
Proof state after:
n : Nat
h_ind : log2' (n / 2 + 1) ≤ n / 2 + 1
⊢ log2' (n / 2 + 1) ≤ n + 1
Theorem: Nat.log2'_le_self
Proof 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)
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
n : Nat
⊢ n > 0 → log2' n < n
Tactic:
intro hpos
Proof state after:
n : Nat
hpos : n > 0
⊢ log2' n < n
Theorem: Nat.log2'_lt_self
Proof state before:
n : Nat
hpos : n > 0
⊢ log2' n < n
Tactic:
induction n using recBase2
Proof state after:
case zero
hpos : 0 > 0
⊢ log2' 0 < 0

case one
hpos : 1 > 0
⊢ log2' 1 < 1

case div2
n✝ : Nat
a✝ : n✝ / 2 + 1 > 0 → log2' (n✝ / 2 + 1) < n✝ / 2 + 1
hpos : n✝ + 2 > 0
⊢ log2' (n✝ + 2) < n✝ + 2
Theorem: Nat.log2'_lt_self
Proof state before:
hpos : 0 > 0
⊢ log2' 0 < 0
Tactic:
case zero => cases hpos
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
hpos : 1 > 0
⊢ log2' 1 < 1
Tactic:
case one => decide
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n + 2) < n + 2
Tactic:
case div2 n h_ind =>
  suffices log2' (n/2 + 1) < n+1
    from log2'_div2 n ▸ Nat.succ_lt_succ this
  calc
    log2' (n/2 + 1)
      < n/2 + 1 := h_ind (Nat.zero_lt_succ ..)
    _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
hpos : 0 > 0
⊢ log2' 0 < 0
Tactic:
cases hpos
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
hpos : 1 > 0
⊢ log2' 1 < 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2'_lt_self
Proof state before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n + 2) < n + 2
Tactic:
suffices log2' (n/2 + 1) < n+1
  from log2'_div2 n ▸ Nat.succ_lt_succ this
Proof state after:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n / 2 + 1) < n + 1
Theorem: Nat.log2'_lt_self
Proof state before:
n : Nat
h_ind : n / 2 + 1 > 0 → log2' (n / 2 + 1) < n / 2 + 1
hpos : n + 2 > 0
⊢ log2' (n / 2 + 1) < n + 1
Tactic:
calc
  log2' (n/2 + 1)
    < n/2 + 1 := h_ind (Nat.zero_lt_succ ..)
  _ ≤ n + 1 := Nat.succ_le_succ (Nat.div_le_self n 2)
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof state before:
n : Nat
⊢ n > 0 → 2 ^ log2' n ≤ n
Tactic:
intro h
Proof state after:
n : Nat
h : n > 0
⊢ 2 ^ log2' n ≤ n
Theorem: Nat.pow2_log2'_le_self
Proof state before:
n : Nat
h : n > 0
⊢ 2 ^ log2' n ≤ n
Tactic:
induction n using recBase2
Proof 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
Theorem: Nat.pow2_log2'_le_self
Proof state before:
h : 0 > 0
⊢ 2 ^ log2' 0 ≤ 0
Tactic:
case zero => cases h
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof state before:
h : 1 > 0
⊢ 2 ^ log2' 1 ≤ 1
Tactic:
case one => exact .refl
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof 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
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof state before:
h : 0 > 0
⊢ 2 ^ log2' 0 ≤ 0
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof state before:
h : 1 > 0
⊢ 2 ^ log2' 1 ≤ 1
Tactic:
exact .refl
Proof state after:
no goals
Theorem: Nat.pow2_log2'_le_self
Proof 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]
Proof 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
Theorem: Nat.pow2_log2'_le_self
Proof 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
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
m n : Nat
⊢ m ≤ n → log2' m ≤ log2' n
Tactic:
induction m using recBase2 generalizing n
Proof state after:
case zero
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n

case one
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n

case div2
n✝ : Nat
a✝ : ∀ {n : Nat}, n✝ / 2 + 1 ≤ n → log2' (n✝ / 2 + 1) ≤ log2' n
n : Nat
⊢ n✝ + 2 ≤ n → log2' (n✝ + 2) ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n
Tactic:
case zero => intros; exact Nat.zero_le _
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n
Tactic:
case one => intros; exact Nat.zero_le _
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
⊢ m + 2 ≤ n → log2' (m + 2) ≤ log2' n
Tactic:
case div2 m h_ind =>
  intro h
  let k := n-2
  have : n = k+2 := Eq.symm $ Nat.sub_add_cancel $ calc
    2 ≤ m+2 := Nat.le_add_left 2 m
    _ ≤ n := h
  rw [this]; unfold log2'; simp [recBase2_div2]
  conv => change (m/2+1).log2' + 1 ≤ (k/2+1).log2' + 1
  suffices m/2+1 ≤ k/2+1
    from Nat.succ_le_succ (h_ind this)
  suffices m ≤ k
    from Nat.succ_le_succ (div_le_div this)
  show m ≤ k;
    exact Nat.le_of_add_le_add_right (‹n=k+2› ▸ h)
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
⊢ 0 ≤ n → log2' 0 ≤ log2' n
Tactic:
intros
Proof state after:
n : Nat
a✝ : 0 ≤ n
⊢ log2' 0 ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
a✝ : 0 ≤ n
⊢ log2' 0 ≤ log2' n
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
⊢ 1 ≤ n → log2' 1 ≤ log2' n
Tactic:
intros
Proof state after:
n : Nat
a✝ : 1 ≤ n
⊢ log2' 1 ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
n : Nat
a✝ : 1 ≤ n
⊢ log2' 1 ≤ log2' n
Tactic:
exact Nat.zero_le _
Proof state after:
no goals
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
⊢ m + 2 ≤ n → log2' (m + 2) ≤ log2' n
Tactic:
intro h
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
⊢ log2' (m + 2) ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
⊢ log2' (m + 2) ≤ log2' n
Tactic:
let k := n-2
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
⊢ log2' (m + 2) ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
⊢ log2' (m + 2) ≤ log2' n
Tactic:
have : n = k+2 := Eq.symm $ Nat.sub_add_cancel $ calc
  2 ≤ m+2 := Nat.le_add_left 2 m
  _ ≤ n := h
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' n
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' n
Tactic:
rw [this]
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' (k + 2)
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m + 2) ≤ log2' (k + 2)
Tactic:
unfold log2'
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m + 2) ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) (k + 2)
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m + 2) ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) (k + 2)
Tactic:
simp [recBase2_div2]
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m / 2 + 1) + 1 ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) ((n - 2) / 2 + 1) + 1
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ recBase2 0 0 (fun x x_1 => x_1 + 1) (m / 2 + 1) + 1 ≤ recBase2 0 0 (fun x x_1 => x_1 + 1) ((n - 2) / 2 + 1) + 1
Tactic:
conv => change (m/2+1).log2' + 1 ≤ (k/2+1).log2' + 1
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m / 2 + 1) + 1 ≤ log2' (k / 2 + 1) + 1
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ log2' (m / 2 + 1) + 1 ≤ log2' (k / 2 + 1) + 1
Tactic:
suffices m/2+1 ≤ k/2+1
  from Nat.succ_le_succ (h_ind this)
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m / 2 + 1 ≤ k / 2 + 1
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m / 2 + 1 ≤ k / 2 + 1
Tactic:
suffices m ≤ k
  from Nat.succ_le_succ (div_le_div this)
Proof state after:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m ≤ k
Theorem: Nat.log2'_le_log2'
Proof state before:
m : Nat
h_ind : ∀ {n : Nat}, m / 2 + 1 ≤ n → log2' (m / 2 + 1) ≤ log2' n
n : Nat
h : m + 2 ≤ n
k : Nat := n - 2
this : n = k + 2
⊢ m ≤ k
Tactic:
exact Nat.le_of_add_le_add_right (‹n=k+2› ▸ h)
Proof state after:
no goals
Theorem: Nat.le_log2'_iff_pow2_le
Proof state before:
k n : Nat
⊢ n > 0 → (k ≤ log2' n ↔ 2 ^ k ≤ n)
Tactic:
intros
Proof state after:
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n ↔ 2 ^ k ≤ n
Theorem: Nat.le_log2'_iff_pow2_le
Proof state before:
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n ↔ 2 ^ k ≤ n
Tactic:
constructor
Proof 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
Theorem: Nat.le_log2'_iff_pow2_le
Proof 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›
Proof state after:
case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n
Theorem: Nat.le_log2'_iff_pow2_le
Proof 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
Proof state after:
no goals
Theorem: Nat.le_log2'_iff_pow2_le
Proof state before:
case mp
k n : Nat
a✝ : n > 0
⊢ k ≤ log2' n → 2 ^ k ≤ n
Tactic:
intro h
Proof state after:
case mp
k n : Nat
a✝ : n > 0
h : k ≤ log2' n
⊢ 2 ^ k ≤ n
Theorem: Nat.le_log2'_iff_pow2_le
Proof 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›
Proof state after:
no goals
Theorem: Nat.le_log2'_iff_pow2_le
Proof state before:
k n : Nat
a✝ : n > 0
h : k ≤ log2' n
⊢ 2 > 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.le_log2'_iff_pow2_le
Proof state before:
case mpr
k n : Nat
a✝ : n > 0
⊢ 2 ^ k ≤ n → k ≤ log2' n
Tactic:
intro h
Proof state after:
case mpr
k n : Nat
a✝ : n > 0
h : 2 ^ k ≤ n
⊢ k ≤ log2' n
Theorem: Nat.le_log2'_iff_pow2_le
Proof 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
Proof state after:
no goals
Theorem: Nat.log2RU_le_self
Proof state before:
⊢ log2RU 0 ≤ 0
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2RU_le_self
Proof state before:
⊢ log2RU 1 ≤ 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2RU_le_self
Proof state before:
n : Nat
⊢ log2RU (n + 2) ≤ n + 2
Tactic:
dsimp [log2RU]
Proof state after:
n : Nat
⊢ log2' (2 * (n + 2 - 1)) ≤ n + 2
Theorem: Nat.log2RU_le_self
Proof state before:
n : Nat
⊢ log2' (2 * (n + 2 - 1)) ≤ n + 2
Tactic:
simp [Nat.mul_add, log2'_div2]
Proof state after:
n : Nat
⊢ log2' (n + 1) + 1 ≤ n + 2
Theorem: Nat.log2RU_le_self
Proof state before:
n : Nat
⊢ log2' (n + 1) + 1 ≤ n + 2
Tactic:
suffices log2' (n+1) ≤ n+1
  from Nat.succ_le_succ this
Proof state after:
n : Nat
⊢ log2' (n + 1) ≤ n + 1
Theorem: Nat.log2RU_le_self
Proof state before:
n : Nat
⊢ log2' (n + 1) ≤ n + 1
Tactic:
exact Nat.log2'_le_self _
Proof state after:
no goals
Theorem: Nat.log2RU_lt_self
Proof state before:
x✝ : 1 > 0
⊢ log2RU 1 < 1
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.log2RU_lt_self
Proof state before:
n : Nat
x✝ : n + 2 > 0
⊢ log2RU (n + 2) < n + 2
Tactic:
dsimp [log2RU]
Proof state after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (2 * (n + 2 - 1)) < n + 2
Theorem: Nat.log2RU_lt_self
Proof state before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (2 * (n + 2 - 1)) < n + 2
Tactic:
simp [Nat.mul_add, log2'_div2]
Proof state after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) + 1 < n + 2
Theorem: Nat.log2RU_lt_self
Proof state before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) + 1 < n + 2
Tactic:
suffices log2' (n+1) < n+1
  from Nat.succ_lt_succ this
Proof state after:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) < n + 1
Theorem: Nat.log2RU_lt_self
Proof state before:
n : Nat
x✝ : n + 2 > 0
⊢ log2' (n + 1) < n + 1
Tactic:
exact Nat.log2'_lt_self (n+1) n.zero_lt_succ
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2RU n ↔ 2 ^ k < n
Tactic:
cases n
Proof 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✝
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
⊢ k < log2RU zero ↔ 2 ^ k < zero
Tactic:
case zero =>
  conv => lhs; rhs; reduce
  constructor <;> (intro h; cases h)
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
⊢ k < log2RU zero ↔ 2 ^ k < zero
Tactic:
conv => lhs; rhs; reduce
Proof state after:
k : Nat
⊢ k < 0 ↔ 2 ^ k < zero
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
⊢ k < 0 ↔ 2 ^ k < zero
Tactic:
constructor <;> (intro h; cases h)
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
case mpr
k : Nat
⊢ 2 ^ k < zero → k < 0
Tactic:
intro h
Proof state after:
case mpr
k : Nat
h : 2 ^ k < zero
⊢ k < 0
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
case mpr
k : Nat
h : 2 ^ k < zero
⊢ k < 0
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2RU (succ n) ↔ 2 ^ k < succ n
Tactic:
dsimp [log2RU]
Proof state after:
k n : Nat
⊢ k < log2' (2 * (succ n - 1)) ↔ 2 ^ k < succ n
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2' (2 * (succ n - 1)) ↔ 2 ^ k < succ n
Tactic:
simp [log2RU]
Proof state after:
k n : Nat
⊢ k < log2' (2 * n) ↔ 2 ^ k < succ n
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2' (2 * n) ↔ 2 ^ k < succ n
Tactic:
cases n
Proof 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✝)
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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)
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
⊢ k < log2' (2 * zero) ↔ 2 ^ k < succ zero
Tactic:
conv => lhs; rhs; reduce
Proof state after:
k : Nat
⊢ k < 0 ↔ 2 ^ k < succ zero
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
⊢ k < 0 ↔ 2 ^ k < succ zero
Tactic:
constructor
Proof state after:
case mp
k : Nat
⊢ k < 0 → 2 ^ k < succ zero

case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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
Proof state after:
case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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)
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
case mp
k : Nat
⊢ k < 0 → 2 ^ k < succ zero
Tactic:
intro h
Proof state after:
case mp
k : Nat
h : k < 0
⊢ 2 ^ k < succ zero
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
case mp
k : Nat
h : k < 0
⊢ 2 ^ k < succ zero
Tactic:
cases h
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
case mpr
k : Nat
⊢ 2 ^ k < succ zero → k < 0
Tactic:
intro hlt1
Proof state after:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
⊢ k < 0
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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)
Proof state after:
case mpr
k : Nat
hlt1 : 2 ^ k < succ zero
this : 2 ^ k > 0
⊢ k < 0
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof 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)
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k : Nat
hlt1 : 2 ^ k < succ zero
⊢ 0 < 2
Tactic:
decide
Proof state after:
no goals
Theorem: Nat.lt_log2RU_iff_pow2_lt
Proof state before:
k n : Nat
⊢ k < log2' (2 * succ n) ↔ 2 ^ k < succ (succ n)
Tactic:
rw [log2'_mul2]
Proof state after:
k n : Nat
⊢ k < log2' (succ n) + 1 ↔ 2 ^ k < succ (succ n)