awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
rw₁₀ : √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₁ : √((‖x‖ * 1 - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₁₂ : √((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
x : ℂ
rw : |(x ^ (↑2 : ℂ)⁻¹).im| = √((‖x‖ - x.re) / 2)
rw₁ : |(x ^ (↑2⁻¹ : ℂ)).im| = √((‖x‖ - x.re) / 2)
rw₂ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg * 2⁻¹)| = √((‖x‖ - x.re) / 2)
rw₃ : |HPow.hPow (β := ℝ) ‖x‖ 2⁻¹ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₄ : |‖x‖ ^ HDiv.hDiv (α := ℝ) 1 2 * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₅ : |√‖x‖ * Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₆ : |√‖x‖| * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₇ : √‖x‖ * |Real.sin (x.arg / 2)| = √((‖x‖ - x.re) / 2)
rw₈ : √‖x‖ * √((1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₉ : √(‖x‖ * ((1 - Real.cos x.arg) / 2)) = √((‖x‖ - x.re) / 2)
rw₁₀ : √(‖x‖ * (1 - Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₁ : √((‖x‖ * 1 - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
rw₁₂ : √((‖x‖ - ‖x‖ * Real.cos x.arg) / 2) = √((‖x‖ - x.re) / 2)
⊢ |(HPow.hPow (β := ℂ) x 2⁻¹).im| = √((‖x‖ - x.re) / 2)
have rw₁₃ : √((‖x‖ - x.re) / 2) = √((‖x‖ - x.re) / 2)
Tactic: rw [← ofReal_ofNat, ← ofReal_inv, cpow_ofReal_im, ← div_eq_mul_inv, ← one_div,
    ← Real.sqrt_eq_rpow, abs_mul, abs_of_nonneg (sqrt_nonneg _), abs_sin_half,
    ← sqrt_mul (norm_nonneg _), ← mul_div_assoc, mul_sub, mul_one, norm_mul_cos_arg]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < (HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ))⁻¹
have refine : 0 < HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
Tactic: refine RCLike.inv_pos_of_pos ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
n : ℕ
hn : n ≠ 0
x : ℝ
⊢ 0 < HPow.hPow (α := ℂ) (↑n : ℂ) (↑x : ℂ)
have rw : 0 < (↑(HPow.hPow (α := ℝ) (↑n : ℝ) x) : ℂ)
Tactic: rw [show (n : ℂ) ^ (x : ℂ) = (n : ℝ) ^ (x : ℂ) from rfl, ← ofReal_cpow n.cast_nonneg']
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
⊢ a ^ b = a ^ n
have rw : HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
Tactic: rw [h.1, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsNat b n
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑n : ℝ) = a ^ n
⊢ a ^ b = a ^ n
have rw₁ : a ^ n = a ^ n
Tactic: rw [h.1, Real.rpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
⊢ a ^ b = (a ^ n)⁻¹
have rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₄ : (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
n : ℕ
h : IsInt b (Int.negOfNat n)
a : ℝ
rw : HPow.hPow (β := ℝ) a (↑(Int.negOfNat n) : ℝ) = (a ^ n)⁻¹
rw₁ : a ^ Int.negOfNat n = (a ^ n)⁻¹
rw₂ : a ^ (-Int.ofNat n) = (a ^ n)⁻¹
rw₃ : (a ^ Int.ofNat n)⁻¹ = (a ^ n)⁻¹
rw₄ : (HPow.hPow (β := ℤ) a (↑n : ℤ))⁻¹ = (a ^ n)⁻¹
⊢ a ^ b = (a ^ n)⁻¹
have rw₅ : (a ^ n)⁻¹ = (a ^ n)⁻¹
Tactic: rw [h.1, Real.rpow_intCast, Int.negOfNat_eq, zpow_neg, Int.ofNat_eq_natCast, zpow_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
m n d r : ℕ
ha : IsNat a m
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (a ^ b) r
have rcases : IsNat (HPow.hPow (α := ℝ) (↑m : ℝ) b) r
Tactic: rcases ha with ⟨rfl⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ IsNat (HPow.hPow (α := ℝ) (↑m : ℝ) b) r
have out : HPow.hPow (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (hypothesis)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
⊢ HPow.hPow (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)
have this : d ≠ 0
Tactic: have : d ≠ 0 := mod_cast hb.den_nz
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
⊢ HPow.hPow (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)
have out : LE.le (α := ℝ) 0 (↑r : ℝ)
Tactic: rw [hb.to_eq rfl rfl, div_eq_mul_inv, Real.rpow_natCast_mul, ← Nat.cast_pow, hm, ← hkl, ← hr,
    Nat.cast_pow, Real.pow_rpow_inv_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
b : ℝ
m n d r : ℕ
hb : IsNNRat b n d
k : ℕ
hr : r ^ d = k
l : ℕ
hm : m ^ n = l
hkl : k = l
this : d ≠ 0
out : LE.le (α := ℝ) 0 (↑r : ℝ)
out₁ : d ≠ 0
⊢ HPow.hPow (α := ℝ) (↑m : ℝ) b = (↑r : ℝ)
have out₂ : LE.le (α := ℝ) 0 (↑m : ℝ)
Tactic: rw [hb.to_eq rfl rfl, div_eq_mul_inv, Real.rpow_natCast_mul, ← Nat.cast_pow, hm, ← hkl, ← hr,
    Nat.cast_pow, Real.pow_rpow_inv_natCast]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ IsNNRat (a ^ b) nr dr
have suffices : IsNNRat (HDiv.hDiv (α := ℝ) (↑nr : ℝ) (↑dr : ℝ)) nr dr
Tactic: suffices IsNNRat (nr / dr : ℝ) nr dr by
    simpa [ha.to_eq, Real.div_rpow, hnum.1, hden.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ IsNNRat (HDiv.hDiv (α := ℝ) (↑nr : ℝ) (↑dr : ℝ)) nr dr
have h : Ne (α := ℝ) (↑dr : ℝ) 0
Tactic: apply IsNNRat.of_raw
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ Ne (α := ℝ) (↑dr : ℝ) 0
have h : HPow.hPow (α := ℝ) (↑da : ℝ) b ≠ 0
Tactic: rw [← hden.1]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
na da : ℕ
ha : IsNNRat a na da
nr dr : ℕ
hnum : IsNat (HPow.hPow (α := ℝ) (↑na : ℝ) b) nr
hden : IsNat (HPow.hPow (α := ℝ) (↑da : ℝ) b) dr
⊢ HPow.hPow (α := ℝ) (↑da : ℝ) b ≠ 0
have apply : LT.lt (α := ℝ) 0 (↑da : ℝ)
Tactic: apply (Real.rpow_pos_of_pos _ _).ne'
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
have rw : a ^ b = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [← Real.rpow_neg_eq_inv_rpow, hb.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Pow.Real (goal)
Goal:
a b : ℝ
n d : ℕ
hb : IsRat b (Int.negOfNat n) d
rw : a ^ b = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
⊢ a ^ b = a⁻¹ ^ HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)
have rw₁ : a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ)) = a ^ (-HDiv.hDiv (α := ℝ) (↑n : ℝ) (↑d : ℝ))
Tactic: rw [← Real.rpow_neg_eq_inv_rpow, hb.neg_to_eq rfl rfl]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
a b : ℝ
hab : a < b
⊢ (1 + rexp (-a))⁻¹ < (1 + rexp (-b))⁻¹
have hb : 0 < 1 + rexp (-b)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
⊢ (1 + rexp (- -x))⁻¹ = 1 - (1 + rexp (-x))⁻¹
have field_simp : 1 + rexp (-x) = (1 + rexp x) * (1 + rexp (-x) - 1)
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
⊢ x.sigmoid * rexp (-x) = (-x).sigmoid
have rw : (1 + rexp (-x))⁻¹ * rexp (-x) = 1 - (1 + rexp (-x))⁻¹
Tactic: rw [sigmoid_neg, sigmoid_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
⊢ range sigmoid = Ioo 0 1
have refine_1 : range sigmoid ⊆ Ioo 0 1
Tactic: refine subset_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
refine_1 : range sigmoid ⊆ Ioo 0 1
⊢ range sigmoid = Ioo 0 1
have refine_2 : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x), x ∈ range sigmoid
Tactic: refine subset_antisymm ?_ fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ 0 < x⁻¹ - 1
have rwa : 1 < x⁻¹
Tactic: rwa [sub_pos, one_lt_inv_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
rwa : 1 < x⁻¹
⊢ 0 < x⁻¹ - 1
have rwa₁ : 0 < x ∧ x < 1
Tactic: rwa [sub_pos, one_lt_inv_iff₀]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (hypothesis)
Goal:
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ x ∈ range sigmoid
have hx₁ : 0 < x⁻¹ - 1
Tactic: replace hx : 0 < x⁻¹ - 1 := by rwa [sub_pos, one_lt_inv_iff₀]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
⊢ HasDerivAt sigmoid (x.sigmoid * (1 - x.sigmoid)) x
have h : x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2
Tactic: convert! (hasDerivAt_neg' x |>.exp.const_add 1 |>.inv <| by positivity) using 1
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
⊢ x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2
have h : (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2
Tactic: rw [← sigmoid_neg, ← sigmoid_mul_rexp_neg x, sigmoid_def]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
⊢ Continuous sigmoid
have apply : Differentiable ℝ sigmoid
Tactic: apply Differentiable.continuous (𝕜 := ℝ)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
x : ℝ
⊢ sigmoid (-x) = σ (sigmoid x)
have a : (↑(sigmoid (-x)) : ℝ) = (↑(σ (sigmoid x)) : ℝ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
⊢ range sigmoid = Ioo 0 1
have rw : Eq (α := Set (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Ioo 0 1) (Ioo 0 1)
Tactic: rw [sigmoid, Subtype.range_coind, Real.range_sigmoid]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Sigmoid (goal)
Goal:
⊢ Eq (α := Set (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Ioo 0 1) (Ioo 0 1)
have h : ∀ (x : { x : ℝ // x ∈ I }),
  Membership.mem (γ := Set { x : ℝ // x ∈ I }) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Ioo 0 1) x ↔
    Membership.mem (γ := Set { x : ℝ // x ∈ I }) (Ioo 0 1) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (hypothesis)
Goal:
x : ℝ
⊢ 0 ≤ expNegInvGlue x
have x₁ : x ≤ 0 ∨ 0 < x
Tactic: cases le_or_gt x 0 with
  | inl h => exact ge_of_eq (zero_of_nonpos h)
  | inr h => exact le_of_lt (pos_of_pos h)
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x ≤ expNegInvGlue y
have inl : ∀ (hx : x ≤ 0), expNegInvGlue x ≤ expNegInvGlue y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
x y : ℝ
hxy : x ≤ y
inl : ∀ (hx : x ≤ 0), expNegInvGlue x ≤ expNegInvGlue y
⊢ expNegInvGlue x ≤ expNegInvGlue y
have inr : ∀ (hx : 0 < x), expNegInvGlue x ≤ expNegInvGlue y
Tactic: rcases le_or_gt x 0 with hx | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
h : AnalyticAt ℝ expNegInvGlue 0
⊢ False
have obtain : ∀ (r : ℝ) (hr : 0 < r) (h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)), False
Tactic: obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
⊢ False
have suffices : expNegInvGlue (r / 2) = 0
Tactic: suffices expNegInvGlue (r / 2) = 0 by simpa [hr, not_le_of_gt]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)
Tactic: simp only [expNegInvGlue, mul_ite, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | ¬x ≤ 0}) (𝓝 0)
Tactic: refine tendsto_const_nhds.if ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | ¬x ≤ 0}) (𝓝 0)
have simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | 0 < x}) (𝓝 0)
Tactic: simp only [not_le]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (hypothesis)
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | 0 < x}) (𝓝 0)
have this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
Tactic: have : Tendsto (fun x ↦ p.eval x⁻¹ / exp x⁻¹) (𝓝[>] 0) (𝓝 0) :=
    p.tendsto_div_exp_atTop.comp tendsto_inv_nhdsGT_zero
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | 0 < x}) (𝓝 0)
have refine : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) {x : ℝ | 0 < x} x),
  Membership.mem (γ := Set ℝ)
    {x : ℝ | (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p / rexp x⁻¹ = (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) x) x}
    x
Tactic: refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
⊢ 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 inl : ∀ (hx : x < 0),
  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
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
inl :
  ∀ (hx : x < 0),
    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
⊢ 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 : HasDerivAt (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
  (Polynomial.eval 0⁻¹
      (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
    expNegInvGlue 0)
  0
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
inl :
  ∀ (hx : x < 0),
    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
inr :
  HasDerivAt (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval 0⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue 0)
    0
⊢ 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₁ : ∀ (hx : 0 < x),
  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
Tactic: rcases lt_trichotomy x 0 with hx | rfl | hx
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ 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 inl : HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
Tactic: rw [zero_of_nonpos hx.le, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
have inl : (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) fun (x : ℝ) ↦ 0
Tactic: refine (hasDerivAt_const _ 0).congr_of_eventuallyEq ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) fun (x : ℝ) ↦ 0
have h : ∀ (y : ℝ) (hy : y < 0), Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
Tactic: filter_upwards [gt_mem_nhds hx] with y hy
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
have h : Polynomial.eval y⁻¹ p * 0 = 0
Tactic: rw [zero_of_nonpos hy.le, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
h : Polynomial.eval y⁻¹ p * 0 = 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
have h₁ : Eq (α := ℝ) 0 0
Tactic: rw [zero_of_nonpos hy.le, mul_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
⊢ HasDerivAt (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
    (Polynomial.eval 0⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue 0)
    0
have inr : Tendsto (α := ℝ) (slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)
Tactic: rw [expNegInvGlue.zero, mul_zero, hasDerivAt_iff_tendsto_slope]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (goal)
Goal:
p : ℝ[X]
⊢ Tendsto (α := ℝ) (slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)
have inr : ∀ (x : ℝ),
  Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x =
    slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
Tactic: refine ((tendsto_polynomial_inv_mul_zero (p * X)).mono_left inf_le_left).congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.SmoothTransition (hypothesis)
Goal:
p : ℝ[X]
x : ℝ
hx : 0 < x
⊢ 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 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
Tactic: have := ((p.hasDerivAt x⁻¹).mul (hasDerivAt_neg _).exp).comp x (hasDerivAt_inv hx.ne')
-- 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
⊢ 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 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)⁻¹
Tactic: convert! this.congr_of_eventuallyEq _ using 1