awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹)
    x
h :
  Polynomial.eval x⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue x =
    (Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹
⊢ HasDerivAt (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval x⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue x)
    x
have inr : (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x]
  (HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv
Tactic: convert! this.congr_of_eventuallyEq _ using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹)
    x
⊢ Polynomial.eval x⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue x =
    (Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹
have h : (HPow.hPow (β := ℕ) x 2)⁻¹ * (Polynomial.eval x⁻¹ p - Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p)) *
    rexp (-x⁻¹) =
  -((Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) + -(Polynomial.eval x⁻¹ p * rexp (-x⁻¹))) *
      (HPow.hPow (β := ℕ) x 2)⁻¹)
Tactic: simp [expNegInvGlue, hx.not_ge]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : 0 < x
this :
  HasDerivAt ((HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv)
    ((Polynomial.eval x⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹)
    x
⊢ (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x]
    (HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv
have h : ∀ (y : ℝ) (hy : 0 < y),
  Polynomial.eval y⁻¹ p * expNegInvGlue y =
    ((HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv) y
Tactic: filter_upwards [lt_mem_nhds hx] with y hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
have apply : ∀ (m : ℕ), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
Tactic: apply contDiff_all_iff_nat.2 (fun m => ?_) n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (F := ℝ) (HAdd.hAdd (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) 1) fun (x : ℝ) ↦
    Polynomial.eval x⁻¹ p * expNegInvGlue x
have succ : ContDiff ℝ (E := ℝ) (F := ℝ) (↑m : WithTop ℕ∞) (deriv fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
Tactic: refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (E := ℝ) (F := ℝ) (↑m : WithTop ℕ∞) (deriv fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
have h : ∀ (x : ℝ),
  deriv (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) x =
    Polynomial.eval x⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue x
Tactic: convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
n : ℕ∞
p : ℝ[X]
m : ℕ
⊢ ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
have zero : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
Tactic: induction m generalizing p with
  | zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
  | succ m ihm =>
    rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
    refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
    convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
    exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
Cleared hypotheses: p, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
n : ℕ∞
p : ℝ[X]
m : ℕ
zero : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
⊢ ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
have succ : ∀ (m : ℕ)
  (ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
  (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑(m + 1) : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
Tactic: induction m generalizing p with
  | zero => exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _
  | succ m ihm =>
    rw [show ((m + 1 : ℕ) : WithTop ℕ∞) = m + 1 from rfl]
    refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩
    convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2
    exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv
Cleared hypotheses: p, m
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
h : 1 ≤ x
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)
have rw : expNegInvGlue x = expNegInvGlue x + 0
Tactic: rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
h : 1 ≤ x
rw : expNegInvGlue x = expNegInvGlue x + 0
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)
have rw₁ : expNegInvGlue x = expNegInvGlue x
Tactic: rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
⊢ (↑(projIcc 0 1 ⋯ x) : ℝ).smoothTransition = x.smoothTransition
have refine_1 : ∀ (x : ℝ) (hx : x < 0), x.smoothTransition = smoothTransition 0
Tactic: refine congr_fun
    (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
refine_1 : ∀ (x : ℝ) (hx : x < 0), x.smoothTransition = smoothTransition 0
⊢ (↑(projIcc 0 1 ⋯ x) : ℝ).smoothTransition = x.smoothTransition
have refine_2 : ∀ (x : ℝ) (hx : 1 < x), x.smoothTransition = smoothTransition 1
Tactic: refine congr_fun
    (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x_1 x : ℝ
hx : x < 0
⊢ x.smoothTransition = smoothTransition 0
have refine_1 : x.smoothTransition = 0
Tactic: rw [smoothTransition.zero, zero_of_nonpos hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x_1 x : ℝ
hx : x < 0
refine_1 : x.smoothTransition = 0
⊢ x.smoothTransition = smoothTransition 0
have refine_1₁ : Eq (α := ℝ) 0 0
Tactic: rw [smoothTransition.zero, zero_of_nonpos hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x_1 x : ℝ
hx : 1 < x
⊢ x.smoothTransition = smoothTransition 1
have refine_2 : x.smoothTransition = 1
Tactic: rw [smoothTransition.one, one_of_one_le hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x_1 x : ℝ
hx : 1 < x
refine_2 : x.smoothTransition = 1
⊢ x.smoothTransition = smoothTransition 1
have refine_2₁ : Eq (α := ℝ) 1 1
Tactic: rw [smoothTransition.one, one_of_one_le hx.le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
⊢ x.smoothTransition = 1 ↔ 1 ≤ x
have inl : ∀ (hx : 1 ≤ x), x.smoothTransition = 1 ↔ 1 ≤ x
Tactic: rcases le_or_gt 1 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x : ℝ
inl : ∀ (hx : 1 ≤ x), x.smoothTransition = 1 ↔ 1 ≤ x
⊢ x.smoothTransition = 1 ↔ 1 ≤ x
have inr : ∀ (hx : x < 1), x.smoothTransition = 1 ↔ 1 ≤ x
Tactic: rcases le_or_gt 1 x with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1 - x)) ≤
    expNegInvGlue y / (expNegInvGlue y + expNegInvGlue (1 - y))
have rw : expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
  expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))
Tactic: rw [div_le_div_iff₀ (pos_denom x) (pos_denom y)]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
    expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))
have simp : expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
Tactic: simp only [mul_add, mul_comm (expNegInvGlue x) (expNegInvGlue y), add_le_add_iff_left]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
have c0 : 0 ≤ expNegInvGlue (1 - y)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
c0 : 0 ≤ expNegInvGlue (1 - y)
⊢ expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
have b0 : 0 ≤ expNegInvGlue y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
c0 : 0 ≤ expNegInvGlue (1 - y)
b0 : 0 ≤ expNegInvGlue y
⊢ expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
have h₁ : expNegInvGlue x ≤ expNegInvGlue y
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
c0 : 0 ≤ expNegInvGlue (1 - y)
b0 : 0 ≤ expNegInvGlue y
h₁ : expNegInvGlue x ≤ expNegInvGlue y
⊢ expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
have h₂ : expNegInvGlue (1 - y) ≤ expNegInvGlue (1 - x)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ 1 - y ≤ 1 - x
have linarith : 1 - x < 1 - y → x - y + (1 - x - (1 - y)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (goal)
Goal:
x : ℝ
hx : x ≠ 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have inl : ∀ (hx : x < 0),
  HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (goal)
Goal:
x : ℝ
hx : x ≠ 0
inl :
  ∀ (hx : x < 0),
    HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
      ∀ (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
have inr : ∀ (hx : 0 < x),
  HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
Tactic: rcases hx.lt_or_gt with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (goal)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have inl : HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
Tactic: rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (hypothesis)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ √x) 0 x ∧ ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have this : (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ √x) fun (x : ℝ) ↦ 0
Tactic: have : (√·) =ᶠ[𝓝 x] fun _ => 0 := (gt_mem_nhds hx).mono fun x hx => sqrt_eq_zero_of_nonpos hx.le
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (hypothesis)
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : 0 < x
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have this : 2 * √x ^ HSub.hSub (α := ℕ) 2 1 ≠ 0
Tactic: have : ↑2 * √x ^ (2 - 1) ≠ 0 := by simp [(sqrt_pos.2 hx).ne', @two_ne_zero ℝ]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (goal)
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 ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have inr : HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sqrt (goal)
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
⊢ HasStrictDerivAt (fun (x : ℝ) ↦ √x) (1 / (2 * √x)) x ∧
    ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
have inr₁ : ∀ (n : WithTop ℕ∞), ContDiffAt ℝ (F := ℝ) n (fun (x : ℝ) ↦ √x) x
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ stirlingSeq 0 = 0
have rw : (↑0! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0) = 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
rw : (↑0! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) * HPow.hPow (β := ℕ) ((↑0 : ℝ) / rexp 1) 0) = 0
⊢ stirlingSeq 0 = 0
have rw₁ : (↑0! : ℝ) / (√(HMul.hMul (α := ℝ) 2 0) * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 0 = 0
have rw₂ : (↑0! : ℝ) / (√0 * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 0 = 0
have rw₃ : (↑0! : ℝ) / (0 * HPow.hPow (β := ℕ) (0 / rexp 1) 0) = 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 0 = 0
have rw₄ : HDiv.hDiv (α := ℝ) (↑0! : ℝ) 0 = 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 0 = 0
have rw₅ : Eq (α := ℝ) 0 0
Tactic: rw [stirlingSeq, cast_zero, mul_zero, Real.sqrt_zero, zero_mul, div_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
⊢ stirlingSeq 1 = rexp 1 / √2
have rw : (↑1! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * HPow.hPow (β := ℕ) ((↑1 : ℝ) / rexp 1) 1) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
rw : (↑1! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * HPow.hPow (β := ℕ) ((↑1 : ℝ) / rexp 1) 1) = rexp 1 / √2
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₁ : (↑1! : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * ((↑1 : ℝ) / rexp 1)) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₂ : (↑1 : ℝ) / (√(HMul.hMul (α := ℝ) 2 (↑1 : ℝ)) * ((↑1 : ℝ) / rexp 1)) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₃ : 1 / (√(HMul.hMul (α := ℝ) 2 1) * (1 / rexp 1)) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₄ : 1 / (√2 * (1 / rexp 1)) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₅ : 1 / (√2 / rexp 1) = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ stirlingSeq 1 = rexp 1 / √2
have rw₆ : rexp 1 / √2 = rexp 1 / √2
Tactic: rw [stirlingSeq, pow_one, factorial_one, cast_one, mul_one, mul_one_div, one_div_div]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ log (stirlingSeq n) =
    log (↑n ! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) - (↑n : ℝ) * log ((↑n : ℝ) / rexp 1)
have zero : log (stirlingSeq 0) = log (↑0! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) - (↑0 : ℝ) * log ((↑0 : ℝ) / rexp 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
zero :
  log (stirlingSeq 0) = log (↑0! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑0 : ℝ)) - (↑0 : ℝ) * log ((↑0 : ℝ) / rexp 1)
⊢ log (stirlingSeq n) =
    log (↑n ! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) - (↑n : ℝ) * log ((↑n : ℝ) / rexp 1)
have succ : ∀ (n : ℕ),
  log (stirlingSeq (n + 1)) =
    log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
      (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
⊢ log (stirlingSeq (n + 1)) =
    log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
      (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)
have succ : 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)
Tactic: rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
succ : 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)
⊢ log (stirlingSeq (n + 1)) =
    log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
      (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)
have succ₁ : √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) ≠ 0
Tactic: rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
succ : 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)
succ₁ : √(HMul.hMul (α := ℝ) 2 (↑(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)
have succ₂ : ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1) ≠ 0
Tactic: rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
Goal:
n : ℕ
succ : 0 < HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)
succ₁ : √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) ≠ 0
succ₂ : ((↑(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)
have succ₃ : Ne (α := ℝ) (↑(n + 1)! : ℝ) 0
Tactic: rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Stirling (goal)
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
⊢ log (stirlingSeq (n + 1)) =
    log (↑(n + 1)! : ℝ) - 1 / 2 * log (HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) -
      (↑(n + 1) : ℝ) * log ((↑(n + 1) : ℝ) / rexp 1)
have succ₄ : √(HMul.hMul (α := ℝ) 2 (↑(n + 1) : ℝ)) * ((↑(n + 1) : ℝ) / rexp 1) ^ (n + 1) ≠ 0
Tactic: rw [stirlingSeq, log_div, log_mul, sqrt_eq_rpow, log_rpow, Real.log_pow, tsub_tsub]