internlm/Lean-Github huggingface dataset:
Theorem: succLtTwoPow
Proof state before:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ a < 2 ^ a
Tactic:
rw [hu]
Proof state after:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Theorem: succLtTwoPow
Proof state before:
case intro
a u : ℕ
hu : a = 2 + u
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Tactic:
clear a hu
Proof state after:
case intro
u : ℕ
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Theorem: succLtTwoPow
Proof state before:
case intro
u : ℕ
⊢ Nat.succ (2 + u) < 2 ^ (2 + u)
Tactic:
induction u with
| zero => simp
| succ u h =>
  rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
  rw [← Nat.add_one]
  apply Nat.add_lt_add h
  apply Nat.one_lt_pow <;> linarith
Proof state after:
no goals
Theorem: succLtTwoPow
Proof state before:
case intro.zero

⊢ Nat.succ (2 + Nat.zero) < 2 ^ (2 + Nat.zero)
Tactic:
simp
Proof state after:
no goals
Theorem: succLtTwoPow
Proof state before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (2 + Nat.succ u) < 2 ^ (2 + Nat.succ u)
Tactic:
rw [Nat.add_succ, Nat.pow_succ, Nat.mul_two]
Proof state after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)
Theorem: succLtTwoPow
Proof state before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ Nat.succ (Nat.succ (2 + u)) < 2 ^ (2 + u) + 2 ^ (2 + u)
Tactic:
rw [← Nat.add_one]
Proof state after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 2 + u + 1 + 1 < 2 ^ (2 + u) + 2 ^ (2 + u)
Theorem: succLtTwoPow
Proof state before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 2 + u + 1 + 1 < 2 ^ (2 + u) + 2 ^ (2 + u)
Tactic:
apply Nat.add_lt_add h
Proof state after:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 1 < 2 ^ (2 + u)
Theorem: succLtTwoPow
Proof state before:
case intro.succ
u : ℕ
h : Nat.succ (2 + u) < 2 ^ (2 + u)
⊢ 1 < 2 ^ (2 + u)
Tactic:
apply Nat.one_lt_pow <;> linarith
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 2 * n = (2 * n) ^ (6⁻¹ * 6)
Tactic:
simp
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ (6⁻¹ * 6) = ((2 * n) ^ 6⁻¹) ^ 6
Tactic:
apply Real.rpow_mul (by linarith)
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ ((2 * n) ^ 6⁻¹) ^ 6 < (↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6
Tactic:
apply Real.rpow_lt_rpow _ _ (by norm_num)
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
. apply Real.rpow_nonneg_of_nonneg; linarith
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
. apply Nat.lt_floor_add_one
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 0 < 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_nonneg_of_nonneg
Proof state after:
case hx
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n
Theorem: twoMulLtTwoPow
Proof state before:
case hx
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (2 * n) ^ 6⁻¹ < ↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1
Tactic:
apply Nat.lt_floor_add_one
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (↑⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊)
Tactic:
norm_cast
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ⌊(2 * n) ^ 6⁻¹⌋₊)
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (6 * ⌊(2 * n) ^ 6⁻¹⌋₊)
Tactic:
conv => rhs; rhs; rw [mul_comm]
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (⌊(2 * n) ^ 6⁻¹⌋₊ * 6)
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < 2 ^ (⌊(2 * n) ^ 6⁻¹⌋₊ * 6)
Tactic:
rw [Nat.pow_mul]
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < (2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊) ^ 6
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ (⌊(2 * n) ^ 6⁻¹⌋₊ + 1) ^ 6 < (2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊) ^ 6
Tactic:
apply Nat.pow_lt_pow_of_lt_left _ (by norm_num)
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ ⌊(2 * n) ^ 6⁻¹⌋₊ + 1 < 2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ ⌊(2 * n) ^ 6⁻¹⌋₊ + 1 < 2 ^ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
apply succLtTwoPow
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
have h0 : 0 ≤ (2 * n) ^ 6⁻¹
Proof state after:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Theorem: twoMulLtTwoPow
Proof state before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
. apply le_of_lt; apply Real.rpow_pos_of_pos; linarith
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ ⌊(2 * n) ^ 6⁻¹⌋₊
Tactic:
rw [Nat.le_floor_iff h0]
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑2 ≤ (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑2 ≤ (2 * n) ^ 6⁻¹
Tactic:
norm_cast
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ≤ (2 * n) ^ 6⁻¹
Tactic:
rw [← Real.rpow_le_rpow_iff (by norm_num) h0 (by norm_num : (0:ℝ) < 6)]
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ ((2 * n) ^ 6⁻¹) ^ 6
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ ((2 * n) ^ 6⁻¹) ^ 6
Tactic:
rw [← Real.rpow_mul (by linarith)]
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ (2 * n) ^ (6⁻¹ * 6)
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ (2 * n) ^ (6⁻¹ * 6)
Tactic:
simp
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ 2 * n
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ 2 * n
Tactic:
rw [mul_comm]
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ n * 2
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 ≤ n * 2
Tactic:
rw [← div_le_iff (by norm_num)]
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 / 2 ≤ n
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 2 ^ 6 / 2 ≤ n
Tactic:
norm_cast
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑(2 ^ 6) / 2 ≤ n
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑(2 ^ 6) / 2 ≤ n
Tactic:
norm_num
Proof state after:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 32 ≤ n
Theorem: twoMulLtTwoPow
Proof state before:
case h2
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 32 ≤ n
Tactic:
assumption
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹
Tactic:
apply le_of_lt
Proof state after:
case h0.a
n : ℝ
hn : 32 ≤ n
⊢ 0 < (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
case h0.a
n : ℝ
hn : 32 ≤ n
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case h0.a.hx
n : ℝ
hn : 32 ≤ n
⊢ 0 < 2 * n
Theorem: twoMulLtTwoPow
Proof state before:
case h0.a.hx
n : ℝ
hn : 32 ≤ n
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 < 6
Tactic:
norm_num
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 2 ^ (6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊) ≤ 2 ^ (6 * (2 * n) ^ 6⁻¹)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_num)]
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ 6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ 6 * (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 6 * ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ 6 * (2 * n) ^ 6⁻¹
Tactic:
rw [mul_le_mul_left (by norm_num)]
Proof state after:
n : ℝ
hn : 32 ≤ n
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
have h0 : 0 ≤ (2 * n) ^ 6⁻¹
Proof state after:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
case h0
n : ℝ
hn : 32 ≤ n
⊢ 0 ≤ (2 * n) ^ 6⁻¹

n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
. apply le_of_lt; apply Real.rpow_pos_of_pos; linarith
Proof state after:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
h0 : 0 ≤ (2 * n) ^ 6⁻¹
⊢ ↑⌊(2 * n) ^ 6⁻¹⌋₊ ≤ (2 * n) ^ 6⁻¹
Tactic:
exact Nat.floor_le h0
Proof state after:
no goals
Theorem: twoMulLtTwoPow
Proof state before:
n : ℝ
hn : 32 ≤ n
⊢ 1 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 18 < 2 * Real.sqrt (2 * n)
Tactic:
rw [← div_lt_iff' (by norm_num)]
Proof state after:
n : ℝ
h : 81 / 2 < n
⊢ 18 / 2 < Real.sqrt (2 * n)
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 18 / 2 < Real.sqrt (2 * n)
Tactic:
rw [Real.lt_sqrt (by norm_num)]
Proof state after:
n : ℝ
h : 81 / 2 < n
⊢ (18 / 2) ^ 2 < 2 * n
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ (18 / 2) ^ 2 < 2 * n
Tactic:
norm_num
Proof state after:
n : ℝ
h : 81 / 2 < n
⊢ 81 < 2 * n
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 81 < 2 * n
Tactic:
rw [← div_lt_iff' (by norm_num)]
Proof state after:
n : ℝ
h : 81 / 2 < n
⊢ 81 / 2 < n
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 81 / 2 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: ltTwoMulSqrtTwoMul
Proof state before:
n : ℝ
h : 81 / 2 < n
⊢ 0 ≤ 18 / 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ (4 ^ (n / 3)) ^ 3
Tactic:
rw [← Real.rpow_mul (by norm_num)]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ 4 ^ (n / 3 * 3)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ 4 ^ (n / 3 * 3)
Tactic:
simp
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (4 ^ (n / 3)) ^ 3 ≤ ((2 * n) ^ (1 + Real.sqrt (2 * n))) ^ 3
Tactic:
apply Real.rpow_le_rpow _ h (by linarith)
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4 ^ (n / 3)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4 ^ (n / 3)
Tactic:
apply Real.rpow_nonneg_of_nonneg (by norm_num)
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 3
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ ((2 * n) ^ (1 + Real.sqrt (2 * n))) ^ 3 = (2 * n) ^ ((1 + Real.sqrt (2 * n)) * 3)
Tactic:
rw [Real.rpow_mul (by linarith)]
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ ((1 + Real.sqrt (2 * n)) * 3) < (2 ^ (6 * (2 * n) ^ 6⁻¹)) ^ ((1 + Real.sqrt (2 * n)) * 3)
Tactic:
apply Real.rpow_lt_rpow (by linarith) (twoMulLtTwoPow (by linarith))
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (1 + Real.sqrt (2 * n)) * 3
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (1 + Real.sqrt (2 * n)) * 3
Tactic:
simp
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1 + Real.sqrt (2 * n)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1 + Real.sqrt (2 * n)
Tactic:
exact lt_add_of_pos_of_le (by norm_num) (Real.sqrt_nonneg _)
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 32 ≤ n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 1
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 ^ (6 * (2 * n) ^ 6⁻¹)) ^ ((1 + Real.sqrt (2 * n)) * 3) < 2 ^ (20 * (2 * n) ^ (2 / 3))
Tactic:
rw [← Real.rpow_mul (by linarith)]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 2 ^ (6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3)) < 2 ^ (20 * (2 * n) ^ (2 / 3))
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 2 ^ (6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3)) < 2 ^ (20 * (2 * n) ^ (2 / 3))
Tactic:
rw [Real.rpow_lt_rpow_left_iff (by linarith)]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) < 20 * (2 * n) ^ (2 / 3)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) < 20 * (2 * n) ^ (2 / 3)
Tactic:
calc
_ = (18 * (1 + Real.sqrt (2*n))) * ((2*n)^6⁻¹) := by linarith
_ < (2 + 18) * Real.sqrt (2*n) * (2*n)^6⁻¹ := by
  rw [mul_lt_mul_right]
  . simp [mul_add, add_mul]
    apply ltTwoMulSqrtTwoMul
    linarith
  . apply Real.rpow_pos_of_pos
    linarith
_ = 20 * (Real.sqrt (2*n) * (2*n)^6⁻¹) := by linarith
_ = _ := by
  simp [Real.sqrt_eq_rpow]
  rw [← Real.rpow_add (by linarith)]
  norm_num
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 2
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 1 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) = 18 * (1 + Real.sqrt (2 * n)) * (2 * n) ^ 6⁻¹
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) * (2 * n) ^ 6⁻¹ < (2 + 18) * Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹
Tactic:
rw [mul_lt_mul_right]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)

n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)

n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
. simp [mul_add, add_mul]
  apply ltTwoMulSqrtTwoMul
  linarith
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
. apply Real.rpow_pos_of_pos
  linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)
Tactic:
simp [mul_add, add_mul]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 < 2 * Real.sqrt (2 * n)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 < 2 * Real.sqrt (2 * n)
Tactic:
apply ltTwoMulSqrtTwoMul
Proof state after:
case h
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 81 / 2 < n
Theorem: fourPowLtOf
Proof state before:
case h
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 81 / 2 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case hx
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n
Theorem: fourPowLtOf
Proof state before:
case hx
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 + 18) * Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹ = 20 * (Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹)
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 20 * (Real.sqrt (2 * n) * (2 * n) ^ 6⁻¹) = 20 * (2 * n) ^ (2 / 3)
Tactic:
simp [Real.sqrt_eq_rpow]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ 2⁻¹ * (2 * n) ^ 6⁻¹ = (2 * n) ^ (2 / 3)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ 2⁻¹ * (2 * n) ^ 6⁻¹ = (2 * n) ^ (2 / 3)
Tactic:
rw [← Real.rpow_add (by linarith)]
Proof state after:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ (2⁻¹ + 6⁻¹) = (2 * n) ^ (2 / 3)
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (2 * n) ^ (2⁻¹ + 6⁻¹) = (2 * n) ^ (2 / 3)
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLtOf
Proof state before:
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 4 ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [(by norm_num : (4 : ℝ) = 2 ^ 2)]
Proof state after:
n : ℝ
hn : 0 < n
⊢ (2 ^ 2) ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ (2 ^ 2) ^ n < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [← Real.rpow_mul (by norm_num)]
Proof state after:
n : ℝ
hn : 0 < n
⊢ 2 ^ (2 * n) < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 2 ^ (2 * n) < 2 ^ (20 * (2 * n) ^ (2 / 3)) ↔ n < 4000
Tactic:
rw [Real.rpow_lt_rpow_left_iff (by linarith)]
Proof state after:
n : ℝ
hn : 0 < n
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Tactic:
have h_nonneg : 0 < (2 * n) ^ (2 / 3) := by apply Real.rpow_pos_of_pos; linarith
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 20 * (2 * n) ^ (2 / 3) ↔ n < 4000
Tactic:
rw [← @Real.rpow_lt_rpow_iff _ _ 3 (by linarith) (by linarith) (by norm_num)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < (20 * (2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < (20 * (2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Tactic:
rw [@Real.mul_rpow 20 _ _ (by norm_num) (by linarith)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * ((2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * ((2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
Tactic:
rw [← Real.rpow_mul (by linarith)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ (2 / 3 * 3) ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ (2 / 3 * 3) ↔ n < 4000
Tactic:
simp
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [(by norm_num : (3:ℝ) = 1 + 2)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ (1 + 2) < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ (1 + 2) < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [@Real.rpow_add (2*n) (by linarith)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ (1 + 2) * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [@Real.rpow_add 20 (by norm_num)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ 1 * 20 ^ 2 * (2 * n) ^ 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 1 * (2 * n) ^ 2 < 20 ^ 1 * 20 ^ 2 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
norm_num
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n * (2 * n) ^ 2 < 8000 * (2 * n) ^ 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n * (2 * n) ^ 2 < 8000 * (2 * n) ^ 2 ↔ n < 4000
Tactic:
rw [mul_lt_mul_right (by apply sq_pos_of_pos; linarith)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 8000 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 2 * n < 8000 ↔ n < 4000
Tactic:
rw [mul_comm]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n * 2 < 8000 ↔ n < 4000