awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Tendsto sigmoid atBot (𝓝 0)

Tactic:
tendsto_const_nhds.add_atTop (tendsto_exp_comp_atTop.mpr tendsto_neg_atBot_atTop)
    |>.inv_tendsto_atTop

Premises used: Iff.mpr, Filter.tendsto_neg_atBot_atTop, tendsto_const_nhds, Filter.Tendsto.add_atTop, Real.tendsto_exp_comp_atTop, Real.sigmoid, Filter.Tendsto.inv_tendsto_atTop
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 1 + rexp (-x) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
h : x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2
⊢ HasDerivAt sigmoid (x.sigmoid * (1 - x.sigmoid)) x

Tactic:
convert! (hasDerivAt_neg' x |>.exp.const_add 1 |>.inv <| by positivity) using 1

Premises used: hasDerivAt_neg', HasDerivAt.exp, HasDerivAt.const_add, OfNat.ofNat, HasDerivAt.inv
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
h : (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2
⊢ x.sigmoid * (1 - x.sigmoid) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2

Tactic:
rw [← sigmoid_neg, ← sigmoid_mul_rexp_neg x, sigmoid_def]

Premises used: Real.sigmoid_neg, Real.sigmoid_def, Real.sigmoid_mul_rexp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ (1 + rexp (-x))⁻¹ * ((1 + rexp (-x))⁻¹ * rexp (-x)) = -(rexp (-x) * -1) / HPow.hPow (β := ℕ) (1 + rexp (-x)) 2

Tactic:
field [sq]

Premises used: sq
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ deriv sigmoid = fun (x : ℝ) ↦ x.sigmoid * (1 - x.sigmoid)

Tactic:
funext fun x => (hasDerivAt_sigmoid x).deriv

Premises used: Real.hasDerivAt_sigmoid, HasDerivAt.deriv, funext
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ AnalyticAt ℝ (F := ℝ) (fun (i : ℝ) ↦ 1 + rexp (-i)) x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
fa : AnalyticAt ℝ f x
⊢ AnalyticAt ℝ (Real.sigmoid ∘ f) x

Tactic:
analyticAt_sigmoid.comp fa

Premises used: analyticAt_sigmoid, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
fa : AnalyticAt ℝ f x
⊢ AnalyticAt ℝ (F := ℝ) (fun (z : E) ↦ (f z).sigmoid) x

Tactic:
fa.sigmoid

Premises used: AnalyticAt.sigmoid, Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ AnalyticOnNhd ℝ sigmoid univ

Tactic:
fun _ _ ↦ analyticAt_sigmoid

Premises used: AnalyticOnNhd, analyticAt_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
fs : AnalyticOnNhd ℝ f s
⊢ AnalyticOnNhd ℝ (Real.sigmoid ∘ f) s

Tactic:
fun z n ↦ analyticAt_sigmoid.comp (fs z n)

Premises used: AnalyticOnNhd, analyticAt_sigmoid, AnalyticAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ AnalyticOn ℝ sigmoid univ

Tactic:
analyticOnNhd_sigmoid.analyticOn

Premises used: analyticOnNhd_sigmoid, AnalyticOnNhd.analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
fs : AnalyticOn ℝ f s
⊢ AnalyticOn ℝ (Real.sigmoid ∘ f) s

Tactic:
analyticOnNhd_sigmoid.comp_analyticOn fs (mapsTo_univ _ _)

Premises used: Set.mapsTo_univ, analyticOnNhd_sigmoid, AnalyticOnNhd.comp_analyticOn
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
s : Set ℝ
⊢ AnalyticWithinAt ℝ sigmoid s x

Tactic:
analyticAt_sigmoid.analyticWithinAt

Premises used: analyticAt_sigmoid, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x : E
fa : AnalyticWithinAt ℝ f s x
⊢ AnalyticWithinAt ℝ (Real.sigmoid ∘ f) s x

Tactic:
analyticAt_sigmoid.comp_analyticWithinAt fa

Premises used: AnalyticAt.comp_analyticWithinAt, analyticAt_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ ContDiff ℝ ω sigmoid

Tactic:
analyticOn_sigmoid.contDiff

Premises used: analyticOn_sigmoid, AnalyticOn.contDiff
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hf : ContDiff ℝ ω f
⊢ ContDiff ℝ ω (Real.sigmoid ∘ f)

Tactic:
contDiff_sigmoid.comp hf

Premises used: ContDiff.comp, contDiff_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Differentiable ℝ sigmoid

Tactic:
contDiff_sigmoid.of_le le_top |>.differentiable_one

Premises used: ContDiff.of_le, le_top, ContDiff.differentiable_one, contDiff_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
hf : Differentiable ℝ f
⊢ Differentiable ℝ (Real.sigmoid ∘ f)

Tactic:
differentiable_sigmoid.comp hf

Premises used: Differentiable.comp, differentiable_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ DifferentiableAt ℝ sigmoid x

Tactic:
differentiable_sigmoid x

Premises used: differentiable_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
x : E
hf : DifferentiableAt ℝ f x
⊢ DifferentiableAt ℝ (Real.sigmoid ∘ f) x

Tactic:
differentiableAt_sigmoid.comp x hf

Premises used: differentiableAt_sigmoid, DifferentiableAt.comp
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
apply : Differentiable ℝ sigmoid
⊢ Continuous sigmoid

Tactic:
apply Differentiable.continuous (𝕜 := ℝ)

Premises used: Differentiable.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Differentiable ℝ sigmoid

Tactic:
fun_prop
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : E → ℝ
hf : Continuous f
⊢ Continuous (Real.sigmoid ∘ f)

Tactic:
continuous_sigmoid.comp hf

Premises used: Continuous.comp, continuous_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x_1 : ℝ
⊢ 0 ≤ x_1.sigmoid

Tactic:
bound
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : E → ℝ
s : Set E
x_1 : ℝ
⊢ x_1.sigmoid ≤ 1

Tactic:
bound
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ 0 < sigmoid x

Tactic:
Real.sigmoid_pos x

Premises used: Real.sigmoid_pos, Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ sigmoid x < 1

Tactic:
Real.sigmoid_lt_one x

Premises used: Real.sigmoid, Real.sigmoid_lt_one
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ StrictMono sigmoid

Tactic:
Real.sigmoid_strictMono

Premises used: StrictMono, Subtype.coind, Real.sigmoid, Real.sigmoid_strictMono, unitInterval.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ sigmoid a ≤ sigmoid b ↔ a ≤ b

Tactic:
Real.sigmoid_le_iff

Premises used: Real.sigmoid_le_iff, Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a ≤ b → sigmoid a ≤ sigmoid b

Tactic:
sigmoid_le_iff.mpr

Premises used: Iff.mpr, unitInterval.sigmoid_le_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ sigmoid a < sigmoid b ↔ a < b

Tactic:
Real.sigmoid_lt_iff

Premises used: Real.sigmoid_lt_iff, Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ a < b → sigmoid a < sigmoid b

Tactic:
sigmoid_lt_iff.mpr

Premises used: Iff.mpr, unitInterval.sigmoid_lt_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Monotone sigmoid

Tactic:
sigmoid_strictMono.monotone

Premises used: unitInterval.sigmoid_strictMono, StrictMono.monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Function.Injective sigmoid

Tactic:
sigmoid_strictMono.injective

Premises used: unitInterval.sigmoid_strictMono, StrictMono.injective
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
a b : ℝ
⊢ sigmoid a = sigmoid b ↔ a = b

Tactic:
sigmoid_injective.eq_iff

Premises used: Function.Injective.eq_iff, unitInterval.sigmoid_injective
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Continuous sigmoid

Tactic:
_root_.continuous_sigmoid.subtype_mk _

Premises used: Continuous.subtype_mk, Subtype.coind, unitInterval.sigmoid, continuous_sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
a : (↑(sigmoid (-x)) : ℝ) = (↑(σ (sigmoid x)) : ℝ)
⊢ sigmoid (-x) = σ (sigmoid x)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ (↑(sigmoid (-x)) : ℝ) = (↑(σ (sigmoid x)) : ℝ)

Tactic:
Real.sigmoid_neg x

Premises used: Real.sigmoid_neg, Real.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
x : ℝ
⊢ (↑(sigmoid (-x)) : ℝ) = (↑(σ (sigmoid x)) : ℝ)

Tactic:
exact Real.sigmoid_neg x

Premises used: Real.sigmoid_neg
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
rw : Eq (α := Set (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Ioo 0 1) (Ioo 0 1)
⊢ range sigmoid = Ioo 0 1

Tactic:
rw [sigmoid, Subtype.range_coind, Real.range_sigmoid]

Premises used: Set.Subtype.range_coind, Real.range_sigmoid, unitInterval.sigmoid
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
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
⊢ Eq (α := Set (↑I : Type)) (Subtype.val (p := fun (x : ℝ) ↦ x ∈ I) ⁻¹' Ioo 0 1) (Ioo 0 1)

Tactic:
ext
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
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:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Tendsto sigmoid atTop (𝓝 1)

Tactic:
tendsto_subtype_rng.mpr Real.tendsto_sigmoid_atTop

Premises used: Iff.mpr, Real.tendsto_sigmoid_atTop, tendsto_subtype_rng
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ Tendsto sigmoid atBot (𝓝 0)

Tactic:
tendsto_subtype_rng.mpr Real.tendsto_sigmoid_atBot

Premises used: Iff.mpr, Real.tendsto_sigmoid_atBot, tendsto_subtype_rng
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ IsEmbedding unitInterval.sigmoid

Tactic:
OrderEmbedding.sigmoid.isEmbedding_of_ordConnected (ordConnected_of_Ioo <|
    fun a _ b _ _ => unitInterval.range_sigmoid ▸ Ioo_subset_Ioo a.2.1 b.2.2)

Premises used: Eq.rec, unitInterval.range_sigmoid, Subtype.coind, And.right, And.left, OrderEmbedding.sigmoid, OrderEmbedding.isEmbedding_of_ordConnected, Eq.symm, Set.Ioo_subset_Ioo, Set.ordConnected_of_Ioo, unitInterval.sigmoid, Subtype.property
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
⊢ MeasurableEmbedding unitInterval.sigmoid

Tactic:
Topology.isEmbedding_sigmoid.measurableEmbedding <| unitInterval.range_sigmoid ▸ measurableSet_Ioo

Premises used: Eq.rec, unitInterval.range_sigmoid, measurableSet_Ioo, Topology.isEmbedding_sigmoid, Eq.symm, Topology.IsEmbedding.measurableEmbedding
-- Module: Mathlib.Analysis.SpecialFunctions.Sigmoid
Goal:
α : Type u_2
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
⊢ MeasurableEmbedding (unitInterval.sigmoid ∘ MeasureTheory.embeddingReal α)

Tactic:
measurableEmbedding_sigmoid.comp (MeasureTheory.measurableEmbedding_embeddingReal α)

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, measurableEmbedding_sigmoid, MeasurableEmbedding.comp
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
hx : x ≤ 0
⊢ expNegInvGlue x = 0

Tactic:
simp [expNegInvGlue, hx]

Premises used: expNegInvGlue
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
⊢ expNegInvGlue 0 = 0

Tactic:
zero_of_nonpos le_rfl

Premises used: le_rfl, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
hx : 0 < x
⊢ 0 < expNegInvGlue x

Tactic:
simp [expNegInvGlue, not_le.2 hx, exp_pos]

Premises used: not_le, Iff.mpr, expNegInvGlue, Real.exp_pos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x

Tactic:
ge_of_eq (zero_of_nonpos h)

Premises used: ge_of_eq, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : x ≤ 0
⊢ 0 ≤ expNegInvGlue x

Tactic:
exact ge_of_eq (zero_of_nonpos h)

Premises used: ge_of_eq, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : 0 < x
⊢ 0 ≤ expNegInvGlue x

Tactic:
le_of_lt (pos_of_pos h)

Premises used: le_of_lt, expNegInvGlue.pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : 0 < x
⊢ 0 ≤ expNegInvGlue x

Tactic:
exact le_of_lt (pos_of_pos h)

Premises used: le_of_lt, expNegInvGlue.pos_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
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)

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ expNegInvGlue x = 0 ↔ x ≤ 0

Tactic:
⟨fun h ↦ not_lt.mp fun h' ↦ (pos_of_pos h').ne' h, zero_of_nonpos⟩

Premises used: expNegInvGlue.pos_of_pos, LT.lt.ne', not_lt, Iff.intro, Iff.mp, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
inl : ∀ (hx : x ≤ 0), expNegInvGlue x ≤ expNegInvGlue y
inr : ∀ (hx : 0 < x), expNegInvGlue x ≤ expNegInvGlue y
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
rcases le_or_gt x 0 with hx | hx

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
hx : x ≤ 0
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
simp [zero_of_nonpos hx, nonneg]

Premises used: expNegInvGlue.nonneg, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
hx : 0 < x
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
simp [expNegInvGlue, not_le.2 hx, not_le.2 (hx.trans_le hxy),
    inv_le_inv₀ (hx.trans_le hxy) hx, hxy]

Premises used: not_le, Iff.mpr, expNegInvGlue, LT.lt.trans_le, inv_le_inv₀
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h : AnalyticAt ℝ expNegInvGlue 0
obtain : ∀ (r : ℝ) (hr : 0 < r) (h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)), False
⊢ False

Tactic:
obtain ⟨r, hr, h⟩ := h.exists_ball_analyticOnNhd

Premises used: AnalyticAt.exists_ball_analyticOnNhd
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
this : expNegInvGlue (r / 2) = 0
⊢ False

Tactic:
simpa [hr, not_le_of_gt]

Premises used: not_le_of_gt
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
suffices : expNegInvGlue (r / 2) = 0
⊢ False

Tactic:
suffices expNegInvGlue (r / 2) = 0 by simpa [hr, not_le_of_gt]
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
⊢ Membership.mem (γ := Set ℝ) (Metric.ball 0 r) 0

Tactic:
simp [hr]
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
⊢ Membership.mem (γ := Set ℝ) (closure ({z : ℝ | expNegInvGlue z = 0} \ {0})) 0

Tactic:
simp [Set.Iic_def]

Premises used: Set.Iic_def
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
⊢ Membership.mem (γ := Set ℝ) (Metric.ball 0 r) (r / 2)

Tactic:
simp [abs_of_pos, hr]

Premises used: abs_of_pos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
h_1 : AnalyticAt ℝ expNegInvGlue 0
r : ℝ
hr : 0 < r
h : AnalyticOnNhd ℝ expNegInvGlue (Metric.ball 0 r)
⊢ expNegInvGlue (r / 2) = 0

Tactic:
exact h.eqOn_zero_of_preconnected_of_mem_closure (z₀ := 0)
    (Real.ball_eq_Ioo 0 r ▸ isPreconnected_Ioo)
    (by simp [hr]) (by simp [Set.Iic_def]) (by simp [abs_of_pos, hr])

Premises used: Real.ball_eq_Ioo, Eq.rec, AnalyticOnNhd.eqOn_zero_of_preconnected_of_mem_closure, isPreconnected_Ioo, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) (𝓝 0) (𝓝 0)

Tactic:
simp only [expNegInvGlue, mul_ite, mul_zero]

Premises used: mul_ite, MulZeroClass.mul_zero, expNegInvGlue
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)

Tactic:
tendsto_const_nhds.if ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.if
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | ¬x ≤ 0}) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ if x ≤ 0 then 0 else Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0) (𝓝 0)

Tactic:
refine tendsto_const_nhds.if ?_

Premises used: tendsto_const_nhds, Filter.Tendsto.if
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
simp : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | 0 < x}) (𝓝 0)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | ¬x ≤ 0}) (𝓝 0)

Tactic:
simp only [not_le]

Premises used: not_le
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
⊢ 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
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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)

Tactic:
this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_

Premises used: self_mem_nhdsWithin, Filter.Tendsto.congr', Filter.mem_of_superset
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
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
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * rexp (-x⁻¹)) (𝓝 0 ⊓ 𝓟 {x : ℝ | 0 < x}) (𝓝 0)

Tactic:
refine this.congr' <| mem_of_superset self_mem_nhdsWithin fun x hx ↦ ?_

Premises used: self_mem_nhdsWithin, Filter.Tendsto.congr', Filter.mem_of_superset
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
this : Tendsto (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p / rexp x⁻¹) (𝓝[>] 0) (𝓝 0)
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:
simp [exp_neg, div_eq_mul_inv]

Premises used: div_eq_mul_inv, Real.exp_neg
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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
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
⊢ 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

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
inl : HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 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:
rw [zero_of_nonpos hx.le, mul_zero]

Premises used: LT.lt.le, MulZeroClass.mul_zero, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x

Tactic:
(hasDerivAt_const _ 0).congr_of_eventuallyEq ?_

Premises used: HasDerivAt.congr_of_eventuallyEq, hasDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
inl : (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) fun (x : ℝ) ↦ 0
⊢ HasDerivAt (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x

Tactic:
refine (hasDerivAt_const _ 0).congr_of_eventuallyEq ?_

Premises used: HasDerivAt.congr_of_eventuallyEq, hasDerivAt_const, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
h : ∀ (y : ℝ) (hy : y < 0), Polynomial.eval y⁻¹ p * expNegInvGlue y = 0
⊢ (𝓝 x).EventuallyEq (β := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) fun (x : ℝ) ↦ 0

Tactic:
filter_upwards [gt_mem_nhds hx] with y hy

Premises used: gt_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : x < 0
y : ℝ
hy : y < 0
h : Polynomial.eval y⁻¹ p * 0 = 0
h₁ h₂ : Eq (α := ℝ) 0 0
⊢ Polynomial.eval y⁻¹ p * expNegInvGlue y = 0

Tactic:
rw [zero_of_nonpos hy.le, mul_zero]

Premises used: LT.lt.le, MulZeroClass.mul_zero, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
inr : Tendsto (α := ℝ) (slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)
⊢ 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:
rw [expNegInvGlue.zero, mul_zero, hasDerivAt_iff_tendsto_slope]

Premises used: MulZeroClass.mul_zero, expNegInvGlue.zero, hasDerivAt_iff_tendsto_slope
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
⊢ Tendsto (α := ℝ) (slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)

Tactic:
((tendsto_polynomial_inv_mul_zero (p * X)).mono_left inf_le_left).congr fun x ↦ ?_

Premises used: HMul.hMul, expNegInvGlue.tendsto_polynomial_inv_mul_zero, Filter.Tendsto.mono_left, Filter.Tendsto.congr, inf_le_left, Polynomial.X