Theorem: chapter02.bertrand_main_inequality (FormalBook/Chapter_02.lean)

State before:
n : ℕ
n_large : 512 ≤ n
⊢ n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
Tactic:
rw [← @cast_le ℝ]
State after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)

State before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ ↑(4 ^ n)
Tactic:
simp only [cast_add, cast_one, cast_mul, cast_pow, ← Real.rpow_natCast]
State after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n

State before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑4 ^ ↑n
Tactic:
refine' _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
State after:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ (2 * ↑n).sqrt * 4 ^ (2 * ↑n / 3)

State before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑n * (↑2 * ↑n) ^ ↑(2 * n).sqrt * ↑4 ^ ↑(2 * n / 3) ≤ ↑n * (2 * ↑n) ^ (2 * ↑n).sqrt * 4 ^ (2 * ↑n / 3)
Tactic:
gcongr
State after:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n

case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ (2 * ↑n).sqrt

case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4

case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3

State before:
n : ℕ
n_large : 512 ≤ n
⊢ 512 ≤ ↑n
Tactic:
exact_mod_cast n_large
State after:
no goals

State before:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑2 * ↑n
Tactic:
have n2_pos : 0 < 2 * n := by positivity
State after:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n

State before:
case h₁.h.hx
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ ↑2 * ↑n
Tactic:
exact mod_cast n2_pos
State after:
no goals

State before:
n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n
Tactic:
positivity
State after:
no goals

State before:
case h₁.h.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n).sqrt ≤ (2 * ↑n).sqrt
Tactic:
exact_mod_cast Real.nat_sqrt_le_real_sqrt
State after:
no goals

State before:
case h₂.hx
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ ↑4
Tactic:
norm_num1
State after:
no goals

State before:
case h₂.hyz
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n / 3) ≤ 2 * ↑n / 3
Tactic:
exact cast_div_le.trans (by norm_cast)
State after:
no goals

State before:
n : ℕ
n_large : 512 ≤ n
⊢ ↑(2 * n) / ↑3 ≤ 2 * ↑n / 3
Tactic:
norm_cast
State after:
no goals