Theorem: rpowDivThreeLe (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
n : ℕ
hn : 0 < n
h : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [← natRealCoeLeCoe] at h
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
have : 4^(↑n/3 : ℝ) = 4^(↑n : ℝ) / 4^(2*↑n/3 : ℝ)
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [eq_div_iff]
  swap; {apply ne_of_gt; apply Real.rpow_pos_of_pos (by norm_num)}
  rw [← Real.rpow_add (by norm_num)]
  simp [Real.rpow_def_of_pos]  norm_num
  push_cast
  simp [div_add_div_same]
  norm_cast
  rw [(by linarith : n + 2*n = n*3)]
  simp
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [this]
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
clear this
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n / 4 ^ (2 * ↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [div_le_iff]
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
swap
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
{apply Real.rpow_pos_of_pos; norm_num}
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ ↑n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
rw [Real.rpow_nat_cast]
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ n ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
norm_cast
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(4 ^ n) ≤ ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(4 ^ n) ≤ ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
apply le_trans h
State after:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
clear h
State after:
n : ℕ
hn : 0 < n
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)

State before:
n : ℕ
hn : 0 < n
⊢ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)) ≤
    ↑(2 * n) ^ (1 + Real.sqrt ↑(2 * n)) * 4 ^ (↑(2 * n) / 3)
Tactic:
push_cast
State after:
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n)) * 4 ^ (2 * ↑n / 3)
Tactic:
apply mul_le_mul
State after:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [← Real.rpow_nat_cast]
  rw [Real.rpow_le_rpow_left_iff (by norm_cast; linarith)]
  simp [-Real.sqrt_mul']
  norm_cast
  apply Real.nat_sqrt_le_real_sqrt
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)

case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. rw [← Real.rpow_nat_cast]
  rw [Real.rpow_le_rpow_left_iff (by norm_cast)]
  rw [le_div_iff (by norm_num)]
  norm_cast
  apply Nat.le_trans (Nat.mul_le_mul_right 3 (Nat.pred_le _))
  apply Nat.div_mul_le_self
State after:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)

case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. apply pow_nonneg (by norm_num)
State after:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
. apply Real.rpow_nonneg_of_nonneg (by norm_cast; linarith)
State after:
no goals

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
Tactic:
rw [eq_div_iff]
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0
Tactic:
swap
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0

case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Tactic:
{apply ne_of_gt; apply Real.rpow_pos_of_pos (by norm_num)}
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) * 4 ^ (2 * ↑n / 3) = 4 ^ ↑n
Tactic:
rw [← Real.rpow_add (by norm_num)]
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3 + 2 * ↑n / 3) = 4 ^ ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3 + 2 * ↑n / 3) = 4 ^ ↑n
Tactic:
simp [Real.rpow_def_of_pos]
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n ∨ 4 = -1

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n ∨ 4 = -1
Tactic:
norm_num
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n
Tactic:
simp [div_add_div_same]
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ (↑n + 2 * ↑n) / 3 = ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ (↑n + 2 * ↑n) / 3 = ↑n
Tactic:
norm_cast
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n + 2 * n) / 3 = ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n + 2 * n) / 3 = ↑n
Tactic:
rw [(by linarith : n + 2*n = n*3)]
State after:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n * 3) / 3 = ↑n

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑(n * 3) / 3 = ↑n
Tactic:
simp
State after:
no goals

State before:
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (2 * ↑n / 3) ≠ 0
Tactic:
apply ne_of_gt
State after:
case this.h
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)

State before:
case this.h
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
apply Real.rpow_pos_of_pos (by norm_num)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ n + 2 * n = n * 3
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4 ^ (2 * ↑n / 3)
Tactic:
apply Real.rpow_pos_of_pos
State after:
case hx
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4

State before:
case hx
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ (1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [← Real.rpow_nat_cast]
State after:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ ↑(1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ ↑(1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_cast; linarith)]
State after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(1 + Nat.sqrt (2 * n)) ≤ 1 + Real.sqrt (2 * ↑n)

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(1 + Nat.sqrt (2 * n)) ≤ 1 + Real.sqrt (2 * ↑n)
Tactic:
simp [-Real.sqrt_mul']
State after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt (2 * ↑n)

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt (2 * ↑n)
Tactic:
norm_cast
State after:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt ↑(2 * n)

State before:
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(Nat.sqrt (2 * n)) ≤ Real.sqrt ↑(2 * n)
Tactic:
apply Real.nat_sqrt_le_real_sqrt
State after:
no goals

State before:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * ↑n
Tactic:
norm_cast
State after:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * n

State before:
n : ℕ
hn : 0 < n
⊢ 1 < 2 * n
Tactic:
linarith
State after:
no goals

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ Nat.pred (2 * n / 3) ≤ 4 ^ (2 * ↑n / 3)
Tactic:
rw [← Real.rpow_nat_cast]
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ ↑(Nat.pred (2 * n / 3)) ≤ 4 ^ (2 * ↑n / 3)

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ 4 ^ ↑(Nat.pred (2 * n / 3)) ≤ 4 ^ (2 * ↑n / 3)
Tactic:
rw [Real.rpow_le_rpow_left_iff (by norm_cast)]
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) ≤ 2 * ↑n / 3

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) ≤ 2 * ↑n / 3
Tactic:
rw [le_div_iff (by norm_num)]
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) * 3 ≤ 2 * ↑n

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ ↑(Nat.pred (2 * n / 3)) * 3 ≤ 2 * ↑n
Tactic:
norm_cast
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ Nat.pred (2 * n / 3) * 3 ≤ 2 * n

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ Nat.pred (2 * n / 3) * 3 ≤ 2 * n
Tactic:
apply Nat.le_trans (Nat.mul_le_mul_right 3 (Nat.pred_le _))
State after:
case h₂
n : ℕ
hn : 0 < n
⊢ 2 * n / 3 * 3 ≤ 2 * n

State before:
case h₂
n : ℕ
hn : 0 < n
⊢ 2 * n / 3 * 3 ≤ 2 * n
Tactic:
apply Nat.div_mul_le_self
State after:
no goals

State before:
n : ℕ
hn : 0 < n
⊢ 1 < 4
Tactic:
norm_cast
State after:
no goals

State before:
n : ℕ
hn : 0 < n
⊢ 0 < 3
Tactic:
norm_num
State after:
no goals

State before:
case c0
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4 ^ Nat.pred (2 * n / 3)
Tactic:
apply pow_nonneg (by norm_num)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 4
Tactic:
norm_num
State after:
no goals

State before:
case b0
n : ℕ
hn : 0 < n
⊢ 0 ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
Tactic:
apply Real.rpow_nonneg_of_nonneg (by norm_cast; linarith)
State after:
no goals

State before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * ↑n
Tactic:
norm_cast
State after:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * n

State before:
n : ℕ
hn : 0 < n
⊢ 0 ≤ 2 * n
Tactic:
linarith
State after:
no goals