awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
this : (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ √x) fun (x : ℝ) ↦ 0
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x

Tactic:
exact
      ⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
        contDiffAt_const.congr_of_eventuallyEq this⟩
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0

Tactic:
simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]

Premises used: Iff.mpr, LT.lt.ne', two_ne_zero, Real.sqrt_pos
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0

Tactic:
have : ↑2 * √x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
this : 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0
inr : HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x
inr₁ : ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x

Tactic:
constructor
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
this : 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x

Tactic:
simpa using sqPartialHomeomorph.hasStrictDerivAt_symm hx this (hasStrictDerivAt_pow 2 _)

Premises used: Real.sqPartialHomeomorph, OfNat.ofNat, OpenPartialHomeomorph.hasStrictDerivAt_symm, hasStrictDerivAt_pow
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
this : 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0
⊢ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x

Tactic:
fun n => sqPartialHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (√x))
        (contDiffAt_id.pow 2)

Premises used: OpenPartialHomeomorph.contDiffAt_symm_deriv, ContDiffAt.pow, OpenPartialHomeomorph.toFun', contDiffAt_id, Real.sqPartialHomeomorph, hasDerivAt_pow, Real.sqrt, OfNat.ofNat, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
this : 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0
⊢ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x

Tactic:
exact fun n => sqPartialHomeomorph.contDiffAt_symm_deriv this hx (hasDerivAt_pow 2 (√x))
        (contDiffAt_id.pow 2)

Premises used: OpenPartialHomeomorph.contDiffAt_symm_deriv, ContDiffAt.pow, contDiffAt_id, Real.sqPartialHomeomorph, hasDerivAt_pow, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x

Tactic:
(deriv_sqrt_aux hx).1

Premises used: Real.deriv_sqrt_aux, And.left
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
n : WithTop ℕ∞
hx : x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x

Tactic:
(deriv_sqrt_aux hx).2 n

Premises used: Real.deriv_sqrt_aux, And.right
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x

Tactic:
(hasStrictDerivAt_sqrt hx).hasDerivAt

Premises used: Real.hasStrictDerivAt_sqrt, HasStrictDerivAt.hasDerivAt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
f : ℝ → ℝ
s : Set ℝ
f' x : ℝ
hf : HasDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasDerivWithinAt (fun (y : ℝ) ↦ √(f y)) (f' / (2 * √(f x))) s x

Tactic:
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using
    (hasDerivAt_sqrt hx).comp_hasDerivWithinAt x hf

Premises used: Function.comp, HasDerivAt.comp_hasDerivWithinAt, mul_one, div_eq_inv_mul, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasDerivAt f f' x
hx : f x ≠ 0
⊢ HasDerivAt (fun (y : ℝ) ↦ √(f y)) (f' / (2 * √(f x))) x

Tactic:
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasDerivAt_sqrt hx).comp x hf

Premises used: HasDerivAt.comp, Function.comp, mul_one, div_eq_inv_mul, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
f : ℝ → ℝ
f' x : ℝ
hf : HasStrictDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictDerivAt (fun (t : ℝ) ↦ √(f t)) (f' / (2 * √(f x))) x

Tactic:
simpa only [(· ∘ ·), div_eq_inv_mul, mul_one] using (hasStrictDerivAt_sqrt hx).comp x hf

Premises used: Function.comp, HasStrictDerivAt.comp, Real.hasStrictDerivAt_sqrt, mul_one, div_eq_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
f : ℝ → ℝ
s : Set ℝ
x : ℝ
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
hxs : UniqueDiffWithinAt ℝ s x
⊢ derivWithin (fun (x : ℝ) ↦ √(f x)) s x = derivWithin f s x / (2 * √(f x))

Tactic:
(hf.hasDerivWithinAt.sqrt hx).derivWithin hxs

Premises used: DifferentiableWithinAt.hasDerivWithinAt, HasDerivWithinAt.sqrt, HasDerivWithinAt.derivWithin
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
f : ℝ → ℝ
x : ℝ
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ deriv (fun (x : ℝ) ↦ √(f x)) x = deriv f x / (2 * √(f x))

Tactic:
(hf.hasDerivAt.sqrt hx).deriv

Premises used: DifferentiableAt.hasDerivAt, HasDerivAt.sqrt, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
f' : StrongDual ℝ E
hf : HasFDerivAt f f' x
hx : f x ≠ 0
⊢ HasFDerivAt (fun (y : E) ↦ √(f y)) ((1 / (2 * √(f x))) • f') x

Tactic:
(hasDerivAt_sqrt hx).comp_hasFDerivAt x hf

Premises used: HasDerivAt.comp_hasFDerivAt, NNReal.toReal, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
f' : StrongDual ℝ E
hf : HasStrictFDerivAt f f' x
hx : f x ≠ 0
⊢ HasStrictFDerivAt (fun (y : E) ↦ √(f y)) ((1 / (2 * √(f x))) • f') x

Tactic:
(hasStrictDerivAt_sqrt hx).comp_hasStrictFDerivAt x hf

Premises used: HasStrictDerivAt.comp_hasStrictFDerivAt, Real.hasStrictDerivAt_sqrt, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
f' : StrongDual ℝ E
hf : HasFDerivWithinAt f f' s x
hx : f x ≠ 0
⊢ HasFDerivWithinAt (fun (y : E) ↦ √(f y)) ((1 / (2 * √(f x))) • f') s x

Tactic:
(hasDerivAt_sqrt hx).comp_hasFDerivWithinAt x hf

Premises used: HasDerivAt.comp_hasFDerivWithinAt, NNReal.toReal, Real.hasDerivAt_sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
⊢ DifferentiableWithinAt ℝ (F := ℝ) (fun (y : E) ↦ √(f y)) s x

Tactic:
(hf.hasFDerivWithinAt.sqrt hx).differentiableWithinAt

Premises used: HasFDerivWithinAt.sqrt, HasFDerivWithinAt.differentiableWithinAt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (y : E) ↦ √(f y)) x

Tactic:
(hf.hasFDerivAt.sqrt hx).differentiableAt

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.differentiableAt, HasFDerivAt.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
hf : DifferentiableOn ℝ f s
hs : ∀ x ∈ s, f x ≠ 0
⊢ DifferentiableOn ℝ (F := ℝ) (fun (y : E) ↦ √(f y)) s

Tactic:
fun x hx => (hf x hx).sqrt (hs x hx)

Premises used: DifferentiableWithinAt.sqrt, DifferentiableOn
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hf : Differentiable ℝ f
hs : ∀ (x : E), f x ≠ 0
⊢ Differentiable ℝ (F := ℝ) fun (y : E) ↦ √(f y)

Tactic:
fun x => (hf x).sqrt (hs x)

Premises used: Differentiable, DifferentiableAt.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
hf : DifferentiableWithinAt ℝ f s x
hx : f x ≠ 0
hxs : UniqueDiffWithinAt ℝ s x
⊢ fderivWithin ℝ (fun (x : E) ↦ √(f x)) s x = HSMul.hSMul (β := E →L[ℝ] ℝ) (1 / (2 * √(f x))) (fderivWithin ℝ f s x)

Tactic:
(hf.hasFDerivWithinAt.sqrt hx).fderivWithin hxs

Premises used: HasFDerivWithinAt.fderivWithin, HasFDerivWithinAt.sqrt, DifferentiableWithinAt.hasFDerivWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
hx : f x ≠ 0
⊢ fderiv ℝ (fun (x : E) ↦ √(f x)) x = HSMul.hSMul (β := E →L[ℝ] ℝ) (1 / (2 * √(f x))) (fderiv ℝ f x)

Tactic:
(hf.hasFDerivAt.sqrt hx).fderiv

Premises used: DifferentiableAt.hasFDerivAt, HasFDerivAt.fderiv, HasFDerivAt.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : WithTop ℕ∞
x : E
hf : ContDiffAt ℝ n f x
hx : f x ≠ 0
⊢ ContDiffAt ℝ (F := ℝ) n (fun (y : E) ↦ √(f y)) x

Tactic:
(contDiffAt_sqrt hx).comp x hf

Premises used: Real.contDiffAt_sqrt, ContDiffAt.comp, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : WithTop ℕ∞
s : Set E
x : E
hf : ContDiffWithinAt ℝ n f s x
hx : f x ≠ 0
⊢ ContDiffWithinAt ℝ (F := ℝ) n (fun (y : E) ↦ √(f y)) s x

Tactic:
(contDiffAt_sqrt hx).comp_contDiffWithinAt x hf

Premises used: Real.contDiffAt_sqrt, ContDiffAt.comp_contDiffWithinAt, NNReal.toReal
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : WithTop ℕ∞
s : Set E
hf : ContDiffOn ℝ n f s
hs : ∀ x ∈ s, f x ≠ 0
⊢ ContDiffOn ℝ (F := ℝ) n (fun (y : E) ↦ √(f y)) s

Tactic:
fun x hx => (hf x hx).sqrt (hs x hx)

Premises used: ContDiffOn, ContDiffWithinAt.sqrt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
n : ℕ∞ω
hf : ContDiff ℝ n f
h : ∀ (x : E), f x ≠ 0
⊢ ContDiff ℝ (F := ℝ) n fun (y : E) ↦ √(f y)

Tactic:
contDiff_iff_contDiffAt.2 fun x => hf.contDiffAt.sqrt (h x)

Premises used: Iff.mpr, contDiff_iff_contDiffAt, ContDiffAt.sqrt, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
rw : (↑0! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0) = 0
rw₁ : (↑0! : ℝ) / (√(HMul.hMul (α := ℝ) 2 0) * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
rw₂ : (↑0! : ℝ) / (√0 * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
rw₃ : (↑0! : ℝ) / (0 * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
rw₄ : HDiv.hDiv (α := ℝ) (↑0! : ℝ) 0 = 0
rw₅ rw₆ : Eq (α := ℝ) 0 0
⊢ stirlingSeq 0 = 0

Tactic:
rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero, Stirling.stirlingSeq, Real.sqrt_zero, Nat.cast_zero, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
rw : (↑1! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * HPow.hPow (β := ℕ) ((↑1 : ℝ) / rexp 1) 1) = rexp 1 / √2
rw₁ : (↑1! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * ((↑1 : ℝ) / rexp 1)) = rexp 1 / √2
rw₂ : (↑1 : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * ((↑1 : ℝ) / rexp 1)) = rexp 1 / √2
rw₃ : 1 / (√(HMul.hMul (α := ℝ) 2 1) * (1 / rexp 1)) = rexp 1 / √2
rw₄ : 1 / (√2 * (1 / rexp 1)) = rexp 1 / √2
rw₅ : 1 / (√2 / rexp 1) = rexp 1 / √2
rw₆ rw₇ : rexp 1 / √2 = rexp 1 / √2
⊢ stirlingSeq 1 = rexp 1 / √2

Tactic:
rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]

Premises used: Stirling.stirlingSeq, mul_one_div, pow_one, mul_one, Nat.cast_one, one_div_div, Nat.factorial_one
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
zero :
  log (stirlingSeq 0) = log (↑0! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) - (↑0 : ℝ) * log ((↑0 : ℝ) / rexp 1)
succ :
  ∀ (n : ℕ),
    log (stirlingSeq (n + 1)) =
      log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
        (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)
⊢ log (stirlingSeq n) =
    log (↑n ! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) - (↑n : ℝ) * log ((↑n : ℝ) / rexp 1)

Tactic:
cases n
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
⊢ log (stirlingSeq 0) = log (↑0! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) - (↑0 : ℝ) * log ((↑0 : ℝ) / rexp 1)

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
succ : 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)
succ₁ : √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) ≠ 0
succ₂ : ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1) ≠ 0
succ₃ : Ne (α := ℝ) (↑(n + 1)! : ℝ) 0
succ₄ : √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) * ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1) ≠ 0
⊢ log (stirlingSeq (n + 1)) =
    log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
      (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)

Tactic:
rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]

Premises used: Real.log_rpow, Real.log_div, Stirling.stirlingSeq, tsub_tsub, Real.log_pow, Real.log_mul, Real.sqrt_eq_rpow
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ Ne (α := ℝ) (↑(n + 1)! : ℝ) 0

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

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
change : HasSum (fun (k : ℕ) ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))
⊢ HasSum
    (fun (k : ℕ) ↦
      1 / (HMul.hMul (α := ℝ) 2 (↑(k + 1) : ℝ) + 1) *
        HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ (k + 1))
    (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Tactic:
change HasSum (fun k => f (k + 1)) _

Premises used: HAdd.hAdd, HasSum, OfNat.ofNat, SummationFilter.unconditional
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
rw : HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)
⊢ HasSum (fun (k : ℕ) ↦ f (k + 1)) (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)))

Tactic:
rw [hasSum_nat_add_iff]

Premises used: hasSum_nat_add_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ HasSum
    (fun (i : ℕ) ↦
      ((↑(m + 1) : ℝ) + 1 / 2) *
        (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1)))
    (((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹))

Tactic:
(hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2)

Premises used: Real.hasSum_log_one_add_inv, Nat.cast_add_one_pos, HDiv.hDiv, HasSum.mul_left, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h :
  f = fun (i : ℕ) ↦
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1))
h₁ :
  log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    ((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹)
⊢ HasSum f (log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i)

Tactic:
convert! (hasSum_log_one_add_inv m.cast_add_one_pos).mul_left ((↑(m + 1) : ℝ) + 1 / 2) using 1

Premises used: Real.hasSum_log_one_add_inv, Nat.cast_add_one_pos, HDiv.hDiv, HasSum.mul_left, Nat.cast, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h :
  ∀ (k : ℕ),
    f k =
      ((↑(m + 1) : ℝ) + 1 / 2) *
        (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))
⊢ f = fun (i : ℕ) ↦
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑i : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * i + 1))

Tactic:
ext k
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
h :
  1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))
⊢ f k =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))

Tactic:
dsimp only [f]
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
h :
  1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) ^ (2 * k) =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
        ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
          HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k + 1))

Tactic:
rw [← pow_mul, pow_add]

Premises used: pow_add, pow_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
h :
  1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) =
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
        ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
          HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) ^ (2 * k) =
    ((↑(m + 1) : ℝ) + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
        ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
          HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))

Tactic:
push_cast
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
k : ℕ
⊢ 1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) =
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
      (2 * (1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1)) *
        ((1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) ^ (2 * k) *
          HPow.hPow (β := ℕ) (1 / (2 * HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) 1))

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
x : ℝ
hx : x ≠ 0
⊢ 1 + x⁻¹ = (x + 1) / x

Tactic:
field
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
⊢ ∀ (x : ℝ) (hx : x ≠ 0), 1 + x⁻¹ = (x + 1) / x

Tactic:
have h (x) (hx : x ≠ (0 : ℝ)) : 1 + x⁻¹ = (x + 1) / x := by field
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h : ∀ (x : ℝ) (hx : x ≠ 0), 1 + x⁻¹ = (x + 1) / x
h₁ :
  log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ) - 1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) -
          HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) - 1) -
        (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) + (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ)) -
            1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) -
          (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - 1)) +
      f 0 =
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
      (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1))
⊢ log (stirlingSeq (m + 1)) - log (stirlingSeq (m + 2)) + ∑ i ∈ range 1, f i =
    ((↑(m + 1) : ℝ) + 1 / 2) * log (1 + (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)⁻¹)

Tactic:
simp (disch := positivity) only [log_stirlingSeq_formula, log_div, log_mul, log_exp,
      factorial_succ, cast_mul, cast_succ, range_one, sum_singleton, h]

Premises used: Nat.cast_succ, Real.log_exp, Stirling.log_stirlingSeq_formula, Nat.factorial_succ, Real.log_div, Finset.sum_singleton, Nat.cast_mul, Finset.range_one, Real.log_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
m : ℕ
f : (k : ℕ) → ℝ :=
  fun (k : ℕ) ↦
    1 / (HMul.hMul (α := ℝ) 2 (↑k : ℝ) + 1) * HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1)) 2 ^ k
h : ∀ (x : ℝ) (hx : x ≠ 0), 1 + x⁻¹ = (x + 1) / x
⊢ log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ) - 1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1)) -
          HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) - 1) -
        (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) + (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1) + log (↑m ! : ℝ)) -
            1 / 2 * (log 2 + log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1)) -
          (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) * (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - 1)) +
      f 0 =
    (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1 / 2) *
      (log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1 + 1) - log (HAdd.hAdd (α := ℝ) (↑m : ℝ) 1))

Tactic:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n m : ℕ
⊢ 0 ≤
    1 / (HMul.hMul (α := ℝ) 2 (↑(m + 1) : ℝ) + 1) *
      HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2 ^ (m + 1)

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Stirling
Goal:
n : ℕ
⊢ 0 ≤ HPow.hPow (β := ℕ) (1 / (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ) + 1)) 2

Tactic:
have h_nonneg : (0 : ℝ) ≤ ((1 : ℝ) / (2 * ↑(n + 1) + 1)) ^ 2 := sq_nonneg _