-- Mathlib/Analysis/SpecialFunctions/MulExpNegMulSq.lean
theorem norm_deriv_mulExpNegMulSq_le_one (hε : 0 < ε) (x : ℝ) :
    ‖deriv (mulExpNegMulSq ε) x‖ ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y

Tactic:
refine ⟨le_trans two_mul_le_exp ((le_add_iff_nonneg_left (exp y)).mpr zero_le_one), ?_⟩

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 1 ≤ rexp y + 2 * y

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Tactic:
rw [heq, abs_mul, abs_exp]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))

Tactic:
ring

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ rexp (-y) * |1 - 2 * y| ≤ 1

Tactic:
have hynonneg : 0 ≤ y := by
  rw [hy, mul_assoc]
  exact mul_nonneg hε.le (mul_self_nonneg x)

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ rexp (-y) * |1 - 2 * y| ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y

Tactic:
rw [hy, mul_assoc]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * (x * x)

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1

Tactic:
simp only [← exp_neg (-y), neg_neg, mul_one, abs_le, neg_le_sub_iff_le_add, tsub_le_iff_right]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 2 * y ≤ 1 + rexp y ∧ 1 ≤ rexp y + 2 * y

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ rexp (-y) * |1 - 2 * y| ≤ 1

Tactic:
apply mul_le_of_le_inv_mul₀ (zero_le_one' ℝ) (exp_nonneg _)

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ |1 - 2 * y| ≤ (rexp (-y))⁻¹ * 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Tactic:
have heq : exp (- (ε * x * x)) + x * (exp (- (ε * x * x)) * (-2 * ε * x))
    = exp (- (ε * x * x)) * (1 -2 * (ε * x * x)) := by ring

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ 1

Tactic:
rw [norm_eq_abs, deriv_mulExpNegMulSq]

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x))| ≤ 1

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 0 ≤ 2 * y

Tactic:
simp [hynonneg]

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * (x * x)

Tactic:
exact mul_nonneg hε.le (mul_self_nonneg x)

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 1 ≤ rexp y + 2 * y

Tactic:
exact le_trans (one_le_exp hynonneg) (le_add_of_nonneg_right (by simp [hynonneg]))

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
x : ℝ
heq : rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))
⊢ rexp (-(ε * x * x)) * |1 - 2 * (ε * x * x)| ≤ 1

Tactic:
set y := ε * x * x with hy

Result:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ rexp (-y) * |1 - 2 * y| ≤ 1