awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
this : log (stirlingSeq 1) - log (stirlingSeq (n + 1)) ≤ 12⁻¹
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
have rw : ∀ (this : 1 - log 2 / 2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹),
  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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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))
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
have rw₁ : ∀ (this : 1 - log √2 - log (stirlingSeq (n + 1)) ≤ 12⁻¹), LE.le (α := ℝ) 0 2
Tactic: rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
have rw₂ : ∀ (this : log (rexp 1 / √2) - log (stirlingSeq (n + 1)) ≤ 12⁻¹), √2 ≠ 0
Tactic: rw [stirlingSeq_one, log_div (by positivity), log_exp, log_sqrt] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
⊢ ∃ (a : ℝ), 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)
have h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
Tactic: have h := log_stirlingSeq_bounded_by_constant
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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)
have refine : ∀ (n : ℕ), rexp c ≤ stirlingSeq (n + 1)
Tactic: refine ⟨exp c, exp_pos _, fun n => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
c : ℝ := HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2
h : ∀ (n : ℕ), HSub.hSub (α := ℝ) 1 12⁻¹ - log 2 / 2 ≤ log (stirlingSeq (n + 1))
n : ℕ
⊢ rexp c ≤ stirlingSeq (n + 1)
have rw : c ≤ log (stirlingSeq (n + 1))
Tactic: rw [← le_log_iff_exp_le (stirlingSeq'_pos n)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
have obtain : ∀ (x : ℝ) (x_pos : 0 < x) (hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)), ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
Tactic: obtain ⟨x, x_pos, hx⟩ := stirlingSeq'_bounded_by_pos_constant
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
⊢ ∃ (a : ℝ), 0 < a ∧ Tendsto stirlingSeq atTop (𝓝 a)
have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
Tactic: have hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ)) := by simpa [lowerBounds] using hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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)
have refine : Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
Tactic: refine ⟨_, lt_of_lt_of_le x_pos (le_csInf (Set.range_nonempty _) hx'), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
x : ℝ
x_pos : 0 < x
hx : ∀ (n : ℕ), x ≤ stirlingSeq (n + 1)
hx' : x ∈ lowerBounds (Set.range (stirlingSeq ∘ succ))
⊢ Tendsto stirlingSeq atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
have rw : Tendsto (fun (n : ℕ) ↦ stirlingSeq (n + 1)) atTop (𝓝 (sInf (Set.range (stirlingSeq ∘ succ))))
Tactic: rw [← Filter.tendsto_add_atTop_iff_nat 1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))
have f : fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
f : fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))
have l₁ : atTop
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
f : fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)
l₁ : atTop
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))
have l₂ : 𝓝 (1 / 2)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
| 𝓝 (1 / 2)
have l₂ : 𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹
Tactic: rw [one_div, ← add_zero (2 : ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
| Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))
have l₂ : 𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹
Tactic: congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (1 / 2))
have conv : Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹)
Tactic: conv =>
    congr
    · skip
    · skip
    rw [one_div, ← add_zero (2 : ℝ)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ Tendsto (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) atTop (𝓝 (HAdd.hAdd (α := ℝ) 2 0)⁻¹)
have refine : ∀ (n : ℕ) (hn : n ≥ 1),
  (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
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 => ?_⟩)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≥ 1
⊢ (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
have rw : ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≥ 1
rw :
  ((HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) / (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
⊢ (2 + HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))⁻¹ = (fun (n : ℕ) ↦ (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) n
have rw₁ : (↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1) = (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]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
⊢ HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    Wallis.W n
have this : 4 = HMul.hMul (α := ℕ) 2 2
Tactic: have : 4 = 2 * 2 := by rfl
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ HPow.hPow (β := ℕ) (stirlingSeq n) 4 / HPow.hPow (β := ℕ) (stirlingSeq (2 * n)) 2 *
      ((↑n : ℝ) / (HMul.hMul (α := ℝ) 2 (↑n : ℝ) + 1)) =
    Wallis.W n
have 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))
Tactic: rw [stirlingSeq, this, pow_mul, stirlingSeq, Wallis.W_eq_factorial_ratio]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ 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))
have 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))
Tactic: simp_rw [div_pow, mul_pow]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ 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))
have 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))
Tactic: rw [sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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))
⊢ 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))
have rw₁ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑(2 * n) : ℝ)
Tactic: rw [sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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) : ℝ)
⊢ 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))
have rw₂ : 0 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
Tactic: rw [sq_sqrt, sq_sqrt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
this : 4 = HMul.hMul (α := ℕ) 2 2
⊢ 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))
have 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)
Tactic: simp [field, ← exp_nsmul]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto Wallis.W atTop (𝓝 (HPow.hPow (β := ℕ) a 2 / 2))
have 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))
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)⟩) ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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)
have rw : LT.lt (α := ℕ) 2 4
Tactic: rw [mul_one_div, ← mul_one_div (a ^ 4) (a ^ 2), one_div, ← pow_sub_of_lt a]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
a : ℝ
hane : a ≠ 0
ha : Tendsto stirlingSeq atTop (𝓝 a)
⊢ 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))
have h : 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
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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 2 / 2))
have 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)))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ Tendsto stirlingSeq atTop (𝓝 √π)
have obtain : ∀ (a : ℝ) (hapos : 0 < a) (halimit : Tendsto stirlingSeq atTop (𝓝 a)), Tendsto stirlingSeq atTop (𝓝 √π)
Tactic: obtain ⟨a, hapos, halimit⟩ := stirlingSeq_has_pos_limit_a
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
⊢ Tendsto stirlingSeq atTop (𝓝 √π)
have hπ : π / 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)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
a : ℝ
hapos : 0 < a
halimit : Tendsto stirlingSeq atTop (𝓝 a)
hπ : π / 2 = HPow.hPow (β := ℕ) a 2 / 2
⊢ Tendsto stirlingSeq atTop (𝓝 √π)
have rwa : Tendsto stirlingSeq atTop (𝓝 √(HPow.hPow (β := ℕ) a 2))
Tactic: rwa [(div_left_inj' (two_ne_zero' ℝ)).mp hπ, sqrt_sq hapos.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ Asymptotics.IsEquivalent (E' := ℝ) atTop (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
    √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n
have huv : Tendsto
  (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
    √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
  atTop (𝓝 1)
Tactic: apply Asymptotics.isEquivalent_of_tendsto_one
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 1)
have this : √π ≠ 0
Tactic: have : sqrt π ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
this : √π ≠ 0
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 1)
have huv : Tendsto
  (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
    √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
  atTop (𝓝 (√π / √π))
Tactic: nth_rewrite 2 [← div_self this]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
this : √π ≠ 0
⊢ Tendsto
    (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n)
    atTop (𝓝 (√π / √π))
have h : (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
    √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) =
  stirlingSeq / fun (x : ℕ) ↦ √π
Tactic: convert! tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
this : √π ≠ 0
⊢ (HDiv.hDiv (α := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ)) fun (n : ℕ) ↦
      √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) =
    stirlingSeq / fun (x : ℕ) ↦ √π
have h : ∀ (n : ℕ),
  HDiv.hDiv (α := ℕ → ℝ) (β := ℕ → ℝ) (fun (n : ℕ) ↦ (↑n ! : ℝ))
      (fun (n : ℕ) ↦ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ) * π) * ((↑n : ℝ) / rexp 1) ^ n) n =
    HDiv.hDiv (β := ℕ → ℝ) stirlingSeq (fun (x : ℕ) ↦ √π) n
Tactic: ext n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
have inl : √(2 * π * (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0 ≤ (↑0! : ℝ)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
inl : √(2 * π * (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0 ≤ (↑0! : ℝ)
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
have inr : ∀ (hn : n ≠ 0), √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have simp : √2 * √π * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√2 * √(↑n : ℝ) * ((↑n : ℝ) / rexp 1) ^ n)
Tactic: simp [sqrt_mul']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (hypothesis)
Goal:
n : ℕ
hn : n ≠ 0
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
have this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
Tactic: have : √(2 * π * n) * (n / exp 1) ^ n = √π * (√(2 * n) * (n / exp 1) ^ n) := by
    simp [sqrt_mul']; ring
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
this : √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n = √π * (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
⊢ √(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n ≤ (↑n ! : ℝ)
have inr : √π ≤ (↑n ! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
Tactic: rw [this, ← le_div_iff₀ (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have hx : Ne (α := ℝ) (↑n : ℝ) 0
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have hy : rexp 1 ≠ 0
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
hn : n ≠ 0
hx : Ne (α := ℝ) (↑n : ℝ) 0
hy : rexp 1 ≠ 0
⊢ (log (2 * π) + log (↑n : ℝ)) / 2 + (↑n : ℝ) * (log (↑n : ℝ) - 1) = log (√(2 * π * (↑n : ℝ)) * ((↑n : ℝ) / rexp 1) ^ n)
have hx₁ : 2 * π ≠ 0
Tactic: rw [log_mul (x := √_), log_sqrt, log_mul (x := 2 * π), log_pow, log_div, log_exp]