awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
f : (k : ℕ) → ℝ := fun (k : ℕ) ↦ log (stirlingSeq (k + 1))
g : (k : ℕ) → ℝ := fun (k : ℕ) ↦ 1 / (12 * HAdd.hAdd (α := ℝ) (↑k : ℝ) 1)
hf :
  log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤
    1 / (12 * HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 1 / (12 * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)
⊢ 0 ≤ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹

Tactic:
have := log_stirlingSeq_bounded_aux n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ rexp 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
rw :
  ∀ (this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹),
    HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
rw₁ : ∀ (this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹), LE.le (α := ℝ) 0 2
rw₂ : ∀ (this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹), √2 ≠ 0
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this

Premises used: Real.log_sqrt, Real.log_exp, Stirling.stirlingSeq_one, Real.log_div
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ LE.le (α := ℝ) 0 2

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ √2 ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ 0 < (↑(n + 1)! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) * ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1))

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
⊢ ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))

Tactic:
have h := log_stirlingSeq_bounded_by_constant
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
⊢ ∃ (a : ℝ), 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
⟨exp c, exp_pos _, fun n => ?_⟩

Premises used: Real.exp, And.intro, Exists.intro, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
refine : ∀ (n : ℕ), rexp c ≤ stirlingSeq (n + 1)
⊢ ∃ (a : ℝ), 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)

Tactic:
refine ⟨exp c, exp_pos _, fun n => ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
rw : c ≤ log (stirlingSeq (n + 1))
⊢ rexp c ≤ stirlingSeq (n + 1)

Tactic:
rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]

Premises used: Real.le_log_iff_exp_le, Stirling.stirlingSeq'_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ c ≤ log (stirlingSeq (n + 1))

Tactic:
h n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ c ≤ log (stirlingSeq (n + 1))

Tactic:
exact h n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ Antitone (stirlingSeq ∘ succ)

Tactic:
fun n m h =>
  (log_le_log_iff (stirlingSeq'_pos m) (stirlingSeq'_pos n)).mp (log_stirlingSeq'_antitone h)

Premises used: Stirling.stirlingSeq, Antitone, Stirling.log_stirlingSeq'_antitone, Real.log_le_log_iff, Iff.mp, Stirling.stirlingSeq'_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
obtain :
  ∀ (x : ℝ) (x_pos : 0 < x) (hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)),
    ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
⊢ ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant

Premises used: Stirling.stirlingSeq'_bounded_by_pos_constant
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))

Tactic:
simpa [lowerBounds] using hx

Premises used: lowerBounds
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))

Tactic:
have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩

Premises used: le_csInf, Set.range_nonempty, And.intro, Exists.intro, lt_of_lt_of_le
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
refine : Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
⊢ ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)

Tactic:
refine ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
rw : Tendsto (fun (n : ℕ) ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
rw [← Filter.tendsto_add_atTop_iff_nat 1]

Premises used: Filter.tendsto_add_atTop_iff_nat, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun (n : ℕ) ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

Premises used: iInf, Stirling.stirlingSeq'_antitone, Stirling.stirlingSeq, tendsto_atTop_ciInf, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto (fun (n : ℕ) ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))

Tactic:
exact tendsto_atTop_ciInf stirlingSeq'_antitone ⟨x, hx'⟩

Premises used: Stirling.stirlingSeq'_antitone, tendsto_atTop_ciInf, Exists.intro
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
f : fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
l₁ : atTop
l₂ : 𝓝 (1 / 2)
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))

Tactic:
congr
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
| fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)

Tactic:
· skip
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
| atTop

Tactic:
· skip
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
l₂ : 𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹
| 𝓝 (1 / 2)

Tactic:
rw [one_div, ← add_zero (2 : ℝ)]

Premises used: one_div, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
l₂ : 𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))

Tactic:
congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]

Premises used: one_div, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
conv : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹)
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))

Tactic:
conv =>
    congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]

Premises used: one_div, add_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹)

Tactic:
(((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀
    ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)

Premises used: Iff.mpr, tendsto_const_div_atTop_nhds_zero_nat, Filter.Tendsto.inv₀, Exists.intro, Filter.Tendsto.const_add, Filter.Tendsto.congr', Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
refine :
  ∀ (n : ℕ) (hn : n ≥ 1),
    (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹)

Tactic:
refine (((tendsto_const_div_atTop_nhds_zero_nat 1).const_add (2 : ℝ)).inv₀
    ((add_zero (2 : ℝ)).symm ▸ two_ne_zero)).congr' (eventually_atTop.mpr ⟨1, fun n hn => ?_⟩)

Premises used: Iff.mpr, tendsto_const_div_atTop_nhds_zero_nat, Filter.Tendsto.inv₀, Exists.intro, Filter.Tendsto.const_add, Filter.Tendsto.congr', Filter.eventually_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≥ 1
rw :
  ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
rw₁ rw₂ :
  (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
⊢ (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n

Tactic:
rw [add_div' (1 : ℝ) 2 n (cast_ne_zero.mpr (one_le_iff_ne_zero.mp hn)), inv_div]

Premises used: Iff.mpr, Nat.cast, add_div', Iff.mp, inv_div, Nat.one_le_iff_ne_zero, OfNat.ofNat, Nat.cast_ne_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ 4 = HMul.hMul (α := ℕ) 2 2

Tactic:
rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
⊢ 4 = HMul.hMul (α := ℕ) 2 2

Tactic:
have : 4 = 2 * 2 := by rfl
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ((↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)) 2)
          2 /
        HPow.hPow (β := ℕ)
          ((↑(2 * n)! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ)) * ((↑(2 * n) : ℝ) / rexp 1) ^ (2 * n))) 2 *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    Wallis.W n

Tactic:
rw [stirlingSeq, this, pow_mul, stirlingSeq, Wallis.W_eq_factorial_ratio]

Premises used: pow_mul, Stirling.stirlingSeq, Real.Wallis.W_eq_factorial_ratio
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
simp_rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 2) 2 /
          (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ))) 2) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n / rexp 1 ^ n) 2) 2) /
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 /
          (HPow.hPow (β := ℕ) (√(HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ))) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑(2 * n) : ℝ) (2 * n) / rexp 1 ^ (2 * n)) 2)) *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
⊢ HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) ((↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)) 2)
          2 /
        HPow.hPow (β := ℕ)
          ((↑(2 * n)! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ)) * ((↑(2 * n) : ℝ) / rexp 1) ^ (2 * n))) 2 *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))

Tactic:
simp_rw [div_pow, mul_pow]

Premises used: div_pow, mul_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
rw :
  HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 2) 2 /
          (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n / rexp 1 ^ n) 2) 2) /
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 /
          (HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ) *
            HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑(2 * n) : ℝ) (2 * n) / rexp 1 ^ (2 * n)) 2)) *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))
rw₁ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ)
rw₂ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 2) 2 /
          (HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ))) 2) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n / rexp 1 ^ n) 2) 2) /
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 /
          (HPow.hPow (β := ℕ) (√(HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ))) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑(2 * n) : ℝ) (2 * n) / rexp 1 ^ (2 * n)) 2)) *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))

Tactic:
rw [sq_sqrt, sq_sqrt]

Premises used: Real.sq_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ 0 ≤ HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
simp :
  rexp (HMul.hMul (α := ℝ) 4 (↑n : ℝ)) * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) ^ (2 * n)) 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n) 4 * rexp (2 * HMul.hMul (α := ℝ) 2 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) 2 (4 * n)
⊢ HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 2) 2 /
          (HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) 2 *
            HPow.hPow (β := ℕ) (HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n / rexp 1 ^ n) 2) 2) /
        (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 /
          (HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ) *
            HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑(2 * n) : ℝ) (2 * n) / rexp 1 ^ (2 * n)) 2)) *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    HPow.hPow (α := ℝ) 2 (4 * n) * HPow.hPow (α := ℝ) (β := ℕ) (↑n ! : ℝ) 4 /
      (HPow.hPow (α := ℝ) (β := ℕ) (↑(2 * n)! : ℝ) 2 * (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1))

Tactic:
simp [field, ← exp_nsmul]

Premises used: Real.exp_nsmul
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ rexp (HMul.hMul (α := ℝ) 4 (↑n : ℝ)) * HPow.hPow (β := ℕ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ) ^ (2 * n)) 2 =
    HPow.hPow (β := ℕ) (HPow.hPow (α := ℝ) (↑n : ℝ) n) 4 * rexp (2 * HMul.hMul (α := ℝ) 2 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) 2 (4 * n)

Tactic:
ring_nf
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (HPow.hPow (β := ℕ) a 2 / 2))

Tactic:
Tendsto.congr' (eventually_atTop.mpr ⟨1, fun n hn =>
    stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩) ?_

Premises used: Iff.mpr, Exists.intro, Iff.mp, Nat.one_le_iff_ne_zero, Filter.Tendsto.congr', Filter.eventually_atTop, OfNat.ofNat, Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
refine :
  Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
        ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)))
    atTop (𝓝 (HPow.hPow (β := ℕ) a 2 / 2))
⊢ Tendsto Wallis.W atTop (𝓝 (HPow.hPow (β := ℕ) a 2 / 2))

Tactic:
refine Tendsto.congr' (eventually_atTop.mpr ⟨1, fun n hn =>
    stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq n (one_le_iff_ne_zero.mp hn)⟩) ?_

Premises used: Iff.mpr, Exists.intro, Iff.mp, Nat.one_le_iff_ne_zero, Filter.Tendsto.congr', Filter.eventually_atTop, OfNat.ofNat, Stirling.stirlingSeq_pow_four_div_stirlingSeq_pow_two_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
rw : LT.lt (α := ℕ) 2 4
⊢ HPow.hPow (β := ℕ) a 2 / 2 = HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)

Tactic:
rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]

Premises used: pow_sub_of_lt, HPow.hPow, mul_one_div, one_div, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ LT.lt (α := ℕ) 2 4

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ HPow.hPow (β := ℕ) a 2 / 2 = HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)

Tactic:
have h : a ^ 2 / 2 = a ^ 4 / a ^ 2 * (1 / 2) := by
    rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
    simp
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : HPow.hPow (β := ℕ) a 2 / 2 = HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)
rw :
  Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
        ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)))
    atTop (𝓝 (HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)))
⊢ Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
        ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)))
    atTop (𝓝 (HPow.hPow (β := ℕ) a 2 / 2))

Tactic:
rw [h]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : HPow.hPow (β := ℕ) a 2 / 2 = HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)
⊢ Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
        ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)))
    atTop (𝓝 (HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)))

Tactic:
((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2)
    (pow_ne_zero 2 hane)).mul tendsto_self_div_two_mul_self_add_one

Premises used: Filter.tendsto_id, two_pos, pow_ne_zero, Filter.Tendsto.div, Filter.Tendsto.pow, Filter.Tendsto.const_mul_atTop', Stirling.stirlingSeq, Filter.Tendsto.mul, Filter.Tendsto.comp, OfNat.ofNat, Stirling.tendsto_self_div_two_mul_self_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
h : HPow.hPow (β := ℕ) a 2 / 2 = HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)
⊢ Tendsto
    (fun (n : ℕ) ↦
      HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
        ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)))
    atTop (𝓝 (HPow.hPow (β := ℕ) a 4 / HPow.hPow (β := ℕ) a 2 * (1 / 2)))

Tactic:
exact ((ha.pow 4).div ((ha.comp (tendsto_id.const_mul_atTop' two_pos)).pow 2)
    (pow_ne_zero 2 hane)).mul tendsto_self_div_two_mul_self_add_one

Premises used: Filter.tendsto_id, two_pos, pow_ne_zero, Filter.Tendsto.div, Filter.Tendsto.pow, Filter.Tendsto.const_mul_atTop', Filter.Tendsto.mul, Filter.Tendsto.comp, OfNat.ofNat, Stirling.tendsto_self_div_two_mul_self_add_one
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
obtain : ∀ (a : ℝ) (hapos : 0 < a) (halimit : Tendsto stirlingSeq atTop (𝓝 a)), Tendsto stirlingSeq atTop (𝓝 √π)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a

Premises used: Stirling.stirlingSeq_has_pos_limit_a
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ π / 2 = HPow.hPow (β := ℕ) a 2 / 2

Tactic:
have hπ : π / 2 = a ^ 2 / 2 :=
    tendsto_nhds_unique Wallis.tendsto_W_nhds_pi_div_two (second_wallis_limit a hapos.ne' halimit)
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = HPow.hPow (β := ℕ) a 2 / 2
rwa : Tendsto stirlingSeq atTop (𝓝 √(HPow.hPow (β := ℕ) a 2))
rwa₁ rwa₂ rwa₃ rwa₄ : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)

Tactic:
rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]

Premises used: Real, LT.lt.le, two_ne_zero', Iff.mp, Real.sqrt_sq, div_left_inj'
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
huv :
  Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 1)
⊢ Asymptotics.IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
    √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n

Tactic:
apply Asymptotics.isEquivalent_of_tendsto_one

Premises used: Asymptotics.isEquivalent_of_tendsto_one
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ √π ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ √π ≠ 0

Tactic:
have : sqrt π ≠ 0 := by positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : √π ≠ 0
huv :
  Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 (√π / √π))
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 1)

Tactic:
nth_rewrite 2 [← div_self this]

Premises used: div_self
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : √π ≠ 0
⊢ Tendsto (stirlingSeq / fun (x : ℕ) ↦ √π) atTop (𝓝 (√π / √π))

Tactic:
tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Stirling.tendsto_stirlingSeq_sqrt_pi
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
this : √π ≠ 0
h :
  (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) =
    stirlingSeq / fun (x : ℕ) ↦ √π
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 (√π / √π))

Tactic:
convert! tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1

Premises used: tendsto_const_nhds, Filter.Tendsto.div, Stirling.tendsto_stirlingSeq_sqrt_pi