awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
inr :
  ∀ (x : ℝ),
    Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x =
      slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x
⊢ Tendsto (α := ℝ) (slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0) (𝓝[≠] 0) (𝓝 0)

Tactic:
refine ((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
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
⊢ Polynomial.eval x⁻¹ (p * X) * expNegInvGlue x =
    slope (PE := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) 0 x

Tactic:
simp [slope_def_field, div_eq_mul_inv, mul_right_comm]

Premises used: div_eq_mul_inv, slope_def_field, mul_right_comm
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
x : ℝ
hx : 0 < x
⊢ 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')
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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⁻¹ ((derivative : (a : ℝ[X]) → ℝ[X]) p) * rexp (-x⁻¹) +
        Polynomial.eval x⁻¹ p * (rexp (-x⁻¹) * -1)) *
      -(HPow.hPow (β := ℕ) x 2)⁻¹)
    x

Tactic:
this.congr_of_eventuallyEq _

Premises used: HasDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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)⁻¹
inr :
  (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x]
    (HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv
⊢ 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:
convert! this.congr_of_eventuallyEq _ using 1

Premises used: HasDerivAt.congr_of_eventuallyEq
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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 :
  (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)⁻¹)
⊢ 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:
simp [expNegInvGlue, hx.not_ge]

Premises used: expNegInvGlue, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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
⊢ (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:
ring
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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 :
  ∀ (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
⊢ (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) =ᶠ[𝓝 x]
    (HMul.hMul (α := ℝ → ℝ) (fun (x : ℝ) ↦ Polynomial.eval x p) fun (x : ℝ) ↦ rexp (-x)) ∘ Inv.inv

Tactic:
filter_upwards [lt_mem_nhds hx] with y hy

Premises used: lt_mem_nhds
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
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
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:
simp [expNegInvGlue, hy.not_ge]

Premises used: expNegInvGlue, LT.lt.not_ge
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
⊢ Differentiable ℝ (F := ℝ) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
fun x ↦
  (hasDerivAt_polynomial_eval_inv_mul p x).differentiableAt

Premises used: Differentiable, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, HasDerivAt.differentiableAt
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
p : ℝ[X]
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
(differentiable_polynomial_eval_inv_mul p).continuous

Premises used: expNegInvGlue.differentiable_polynomial_eval_inv_mul, Differentiable.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
p : ℝ[X]
apply : ∀ (m : ℕ), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
⊢ ContDiff ℝ (F := ℝ) (↑n : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
apply contDiff_all_iff_nat.2 (fun m => ?_) n

Premises used: Iff.mpr, contDiff_all_iff_nat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _

Premises used: Iff.mpr, contDiff_zero, WithTop.some, expNegInvGlue.continuous_polynomial_eval_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
p : ℝ[X]
⊢ ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
exact contDiff_zero.2 <| continuous_polynomial_eval_inv_mul _

Premises used: Iff.mpr, contDiff_zero, expNegInvGlue.continuous_polynomial_eval_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ Eq (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) ⊤ →
    AnalyticOn ℝ (F := ℝ) (fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x) univ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
succ : ContDiff ℝ (E := ℝ) (F := ℝ) (↑m : WithTop ℕ∞) (deriv fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)
⊢ ContDiff ℝ (F := ℝ) (HAdd.hAdd (α := WithTop ℕ∞) (↑m : WithTop ℕ∞) 1) fun (x : ℝ) ↦
    Polynomial.eval x⁻¹ p * expNegInvGlue x

Tactic:
refine contDiff_succ_iff_deriv.2 ⟨differentiable_polynomial_eval_inv_mul _, by simp, ?_⟩

Premises used: Iff.mpr, And.intro, contDiff_succ_iff_deriv, expNegInvGlue.differentiable_polynomial_eval_inv_mul
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
⊢ ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦
    Polynomial.eval x⁻¹
        (HPow.hPow (α := ℝ[X]) (β := ℕ) X 2 * HSub.hSub (β := ℝ[X]) p ((derivative : (a : ℝ[X]) → ℝ[X]) p : ℝ[X])) *
      expNegInvGlue x

Tactic:
ihm (X ^ 2 * (p - derivative (R := ℝ) p))

Premises used: Polynomial.derivative, HMul.hMul, HSub.hSub, HPow.hPow, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
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
⊢ ContDiff ℝ (E := ℝ) (F := ℝ) (↑m : WithTop ℕ∞) (deriv fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x)

Tactic:
convert! ihm (X ^ 2 * (p - derivative (R := ℝ) p)) using 2

Premises used: Polynomial.derivative, HMul.hMul, HSub.hSub, HPow.hPow, OfNat.ofNat, Polynomial.X, DFunLike.coe
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
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:
(hasDerivAt_polynomial_eval_inv_mul p _).deriv

Premises used: expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
m : ℕ
ihm : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑m : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
p : ℝ[X]
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:
exact (hasDerivAt_polynomial_eval_inv_mul p _).deriv

Premises used: expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, HasDerivAt.deriv
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
p : ℝ[X]
m : ℕ
zero : ∀ (p : ℝ[X]), ContDiff ℝ (F := ℝ) (↑0 : WithTop ℕ∞) fun (x : ℝ) ↦ Polynomial.eval x⁻¹ p * expNegInvGlue x
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
⊢ ContDiff ℝ (F := ℝ) (↑m : 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

Premises used: Iff.mpr, expNegInvGlue.hasDerivAt_polynomial_eval_inv_mul, contDiff_zero, HasDerivAt.deriv, expNegInvGlue.continuous_polynomial_eval_inv_mul, And.intro, contDiff_succ_iff_deriv, expNegInvGlue.differentiable_polynomial_eval_inv_mul, rfl
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) expNegInvGlue

Tactic:
simpa using contDiff_polynomial_eval_inv_mul 1

Premises used: expNegInvGlue.contDiff_polynomial_eval_inv_mul, OfNat.ofNat
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ 0 < expNegInvGlue x + expNegInvGlue (1 - x)

Tactic:
(zero_lt_one.gt_or_lt x).elim (fun hx => add_pos_of_pos_of_nonneg (pos_of_pos hx) (nonneg _))
    fun hx => add_pos_of_nonneg_of_pos (nonneg _) (pos_of_pos <| sub_pos.2 hx)

Premises used: Iff.mpr, sub_pos, LT.lt.gt_or_lt, HSub.hSub, expNegInvGlue.pos_of_pos, expNegInvGlue.nonneg, zero_lt_one, add_pos_of_nonneg_of_pos, Or.elim, OfNat.ofNat, add_pos_of_pos_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : 1 ≤ x
rw : expNegInvGlue x = expNegInvGlue x + 0
rw₁ rw₂ : expNegInvGlue x = expNegInvGlue x
⊢ expNegInvGlue x = expNegInvGlue x + expNegInvGlue (1 - x)

Tactic:
rw [zero_of_nonpos (sub_nonpos.2 h), add_zero]

Premises used: Iff.mpr, sub_nonpos, add_zero, expNegInvGlue.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ x.smoothTransition = 0 ↔ x ≤ 0

Tactic:
simp only [smoothTransition, _root_.div_eq_zero_iff, (pos_denom x).ne', zero_iff_nonpos, or_false]

Premises used: LT.lt.ne', Real.smoothTransition, Real.smoothTransition.zero_iff_nonpos, or_false, div_eq_zero_iff, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : x ≤ 0
⊢ x.smoothTransition = 0

Tactic:
zero_iff_nonpos.2 h

Premises used: Iff.mpr, Real.smoothTransition.zero_iff_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
⊢ smoothTransition 0 = 0

Tactic:
zero_of_nonpos le_rfl

Premises used: le_rfl, Real.smoothTransition.zero_of_nonpos
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
⊢ smoothTransition 1 = 1

Tactic:
one_of_one_le le_rfl

Premises used: le_rfl, Real.smoothTransition.one_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ (↑(projIcc 0 1 ⋯ x) : ℝ).smoothTransition = x.smoothTransition

Tactic:
congr_fun
    (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x

Premises used: Set.IccExtend_eq_self, zero_le_one, Real.smoothTransition, Set.IccExtend, congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
refine_1 : ∀ (x : ℝ) (hx : x < 0), x.smoothTransition = smoothTransition 0
refine_2 : ∀ (x : ℝ) (hx : 1 < x), x.smoothTransition = smoothTransition 1
⊢ (↑(projIcc 0 1 ⋯ x) : ℝ).smoothTransition = x.smoothTransition

Tactic:
refine congr_fun
    (IccExtend_eq_self zero_le_one smoothTransition (fun x hx => ?_) fun x hx => ?_) x

Premises used: Set.IccExtend_eq_self, zero_le_one, Real.smoothTransition, congr_fun
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x_1 x : ℝ
hx : x < 0
refine_1 : x.smoothTransition = 0
refine_1₁ refine_1₂ : Eq (α := ℝ) 0 0
⊢ x.smoothTransition = smoothTransition 0

Tactic:
rw [smoothTransition.zero, zero_of_nonpos hx.le]

Premises used: Real.smoothTransition.zero_of_nonpos, Real.smoothTransition.zero, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x_1 x : ℝ
hx : 1 < x
refine_2 : x.smoothTransition = 1
refine_2₁ refine_2₂ : Eq (α := ℝ) 1 1
⊢ x.smoothTransition = smoothTransition 1

Tactic:
rw [smoothTransition.one, one_of_one_le hx.le]

Premises used: Real.smoothTransition.one, Real.smoothTransition.one_of_one_le, LT.lt.le
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ x.smoothTransition ≤ 1

Tactic:
(div_le_one (pos_denom x)).2 <| le_add_of_nonneg_right (nonneg _)

Premises used: Iff.mpr, expNegInvGlue.nonneg, Real.smoothTransition, div_le_one, le_add_of_nonneg_right, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ 0 ≤ x.smoothTransition

Tactic:
div_nonneg (expNegInvGlue.nonneg _) (pos_denom x).le

Premises used: LT.lt.le, expNegInvGlue.nonneg, Real.smoothTransition, div_nonneg, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : x < 1
⊢ x.smoothTransition < 1

Tactic:
(div_lt_one <| pos_denom x).2 <| lt_add_of_pos_right _ <| pos_of_pos <| sub_pos.2 h

Premises used: Iff.mpr, sub_pos, lt_add_of_pos_right, expNegInvGlue.pos_of_pos, Real.smoothTransition, div_lt_one, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
h : 0 < x
⊢ 0 < x.smoothTransition

Tactic:
div_pos (expNegInvGlue.pos_of_pos h) (pos_denom x)

Premises used: expNegInvGlue.pos_of_pos, Real.smoothTransition, div_pos, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
inl : ∀ (hx : 1 ≤ x), x.smoothTransition = 1 ↔ 1 ≤ x
inr : ∀ (hx : x < 1), x.smoothTransition = 1 ↔ 1 ≤ x
⊢ x.smoothTransition = 1 ↔ 1 ≤ x

Tactic:
rcases le_or_gt 1 x with hx | hx

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

Tactic:
simp [hx, one_of_one_le]

Premises used: Real.smoothTransition.one_of_one_le
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
hx : x < 1
⊢ x.smoothTransition = 1 ↔ 1 ≤ x

Tactic:
simpa [(lt_one_of_lt_one hx).ne] using hx

Premises used: Real.smoothTransition.lt_one_of_lt_one, LT.lt.ne
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
n : ℕ∞
⊢ ContDiff ℝ (↑n : WithTop ℕ∞) smoothTransition

Tactic:
expNegInvGlue.contDiff.div
    (expNegInvGlue.contDiff.add <| expNegInvGlue.contDiff.comp <| contDiff_const.sub contDiff_id)
    fun x => (pos_denom x).ne'

Premises used: ContDiff.sub, contDiff_id, contDiff_const, LT.lt.ne', Real.smoothTransition, ContDiff.comp, ContDiff.add, expNegInvGlue.contDiff, Real.smoothTransition.pos_denom, ContDiff.div
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
n : ℕ∞
⊢ ContDiffAt ℝ (↑n : WithTop ℕ∞) smoothTransition x

Tactic:
smoothTransition.contDiff.contDiffAt

Premises used: Real.smoothTransition.contDiff, ContDiff.contDiffAt
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
⊢ Continuous smoothTransition

Tactic:
(@smoothTransition.contDiff 0).continuous

Premises used: ContDiff.continuous, Real.smoothTransition.contDiff
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x : ℝ
⊢ ContinuousAt smoothTransition x

Tactic:
smoothTransition.continuous.continuousAt

Premises used: Continuous.continuousAt, Real.smoothTransition.continuous
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
rw :
  expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
    expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))
⊢ expNegInvGlue x / (expNegInvGlue x + expNegInvGlue (1 - x)) ≤
    expNegInvGlue y / (expNegInvGlue y + expNegInvGlue (1 - y))

Tactic:
rw [div_le_div_iff₀ (pos_denom x) (pos_denom y)]

Premises used: div_le_div_iff₀, Real.smoothTransition.pos_denom
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
simp : expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)
⊢ expNegInvGlue x * (expNegInvGlue y + expNegInvGlue (1 - y)) ≤
    expNegInvGlue y * (expNegInvGlue x + expNegInvGlue (1 - x))

Tactic:
simp only [mul_add, mul_comm (expNegInvGlue x) (expNegInvGlue y), add_le_add_iff_left]

Premises used: add_le_add_iff_left, expNegInvGlue, mul_comm, mul_add
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
c0 : 0 ≤ expNegInvGlue (1 - y)
b0 : 0 ≤ expNegInvGlue y
h₁ : expNegInvGlue x ≤ expNegInvGlue y
h₂ : expNegInvGlue (1 - y) ≤ expNegInvGlue (1 - x)
⊢ expNegInvGlue x * expNegInvGlue (1 - y) ≤ expNegInvGlue y * expNegInvGlue (1 - x)

Tactic:
gcongr
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
⊢ 0 ≤ expNegInvGlue (1 - y)

Tactic:
expNegInvGlue.nonneg _

Premises used: expNegInvGlue.nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
⊢ 0 ≤ expNegInvGlue (1 - y)

Tactic:
exact expNegInvGlue.nonneg _

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

Tactic:
expNegInvGlue.nonneg _

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

Tactic:
exact expNegInvGlue.nonneg _

Premises used: expNegInvGlue.nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue x ≤ expNegInvGlue y

Tactic:
apply expNegInvGlue.monotone hxy

Premises used: expNegInvGlue.monotone
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
linarith : 1 - x < 1 - y → x - y + (1 - x - (1 - y)) = 0
⊢ 1 - y ≤ 1 - x

Tactic:
linarith
-- Module: Mathlib.Analysis.SpecialFunctions.SmoothTransition
Goal:
x y : ℝ
hxy : x ≤ y
⊢ expNegInvGlue (1 - y) ≤ expNegInvGlue (1 - x)

Tactic:
apply expNegInvGlue.monotone (by linarith)

Premises used: expNegInvGlue.monotone
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
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
inr :
  ∀ (hx : 0 < x),
    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

Tactic:
rcases hx.lt_or_gt with hx | hx

Premises used: Ne.lt_or_gt
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
inl :
  HasStrictDerivAt (F := ℝ) (fun (x : ℝ) ↦ √x) 0 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

Tactic:
rw [sqrt_eq_zero_of_nonpos hx.le, mul_zero, div_zero]

Premises used: Real.sqrt_eq_zero_of_nonpos, LT.lt.le, MulZeroClass.mul_zero, div_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Sqrt
Goal:
x : ℝ
hx_1 : x ≠ 0
hx : x < 0
⊢ (𝓝 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
-- 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:
⟨(hasStrictDerivAt_const x (0 : ℝ)).congr_of_eventuallyEq this.symm, fun n =>
        contDiffAt_const.congr_of_eventuallyEq this⟩

Premises used: hasStrictDerivAt_const, And.intro, contDiffAt_const, OfNat.ofNat, ContDiffAt.congr_of_eventuallyEq, HasStrictDerivAt.congr_of_eventuallyEq, Filter.EventuallyEq.symm