Theorem: centralBinomialUpper_limit (ExponentialRamsey/Prereq/Mathlib/Analysis/SpecialFunctions/ExplicitStirling.lean)

State before:
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have : (sqrt π)⁻¹ = (sqrt π)⁻¹ / Real.sqrt 1 := by rw [Real.sqrt_one, div_one]
State after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)

State before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
have h : Real.sqrt 1 ≠ 0 := sqrt_ne_zero'.2 zero_lt_one
State after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)

State before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 (Real.sqrt π)⁻¹)
Tactic:
rw [this]
State after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))

State before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ Tendsto centralBinomialUpper atTop (𝓝 ((Real.sqrt π)⁻¹ / Real.sqrt 1))
Tactic:
refine' (centralBinom_limit.div (tendsto_coe_nat_div_add_atTop (1 / 3 : ℝ)).sqrt h).congr' _
State after:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) =ᶠ[atTop]
    centralBinomialUpper

State before:
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) =ᶠ[atTop]
    centralBinomialUpper
Tactic:
filter_upwards [eventually_gt_atTop 0] with n hn
State after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) n =
    centralBinomialUpper n

State before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ((fun n => ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n) / fun x => Real.sqrt (↑x / (↑x + 1 / 3))) n =
    centralBinomialUpper n
Tactic:
dsimp
State after:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 3)) = centralBinomialUpper n

State before:
case h
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ ↑(centralBinom n) * Real.sqrt ↑n / 4 ^ n / Real.sqrt (↑n / (↑n + 1 / 3)) = centralBinomialUpper n
Tactic:
rw [sqrt_div (Nat.cast_nonneg _), centralBinomialUpper, div_div, mul_div_assoc',
  div_div_eq_mul_div, mul_right_comm, mul_div_mul_right]
State after:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0

State before:
⊢ (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
Tactic:
rw [Real.sqrt_one, div_one]
State after:
no goals

State before:
case h.hc
this : (Real.sqrt π)⁻¹ = (Real.sqrt π)⁻¹ / Real.sqrt 1
h : Real.sqrt 1 ≠ 0
n : ℕ
hn : 0 < n
⊢ Real.sqrt ↑n ≠ 0
Tactic:
positivity
State after:
no goals