awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
split_ifs : ∀ (h : 0 ≤ x), ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
split_ifs₁ : ∀ (h : ¬0 ≤ x), ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
simp : ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Tactic:
simp only [exponentialPDF_eq]

Premises used: ProbabilityTheory.exponentialPDF_eq
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
rw :
  EqOn (β := ℝ≥0∞) (fun (y : ℝ) ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) (fun (x : ℝ) ↦ 0) (Iic x)
⊢ ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0

Tactic:
rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]

Premises used: MeasureTheory.setLIntegral_congr_fun, MeasureTheory.lintegral_zero, measurableSet_Iic, ENNReal.ofReal_zero
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
h_1 : a ≤ x
linarith : 0 ≤ a → x - 0 + (a - x) + (0 - a) = 0
⊢ ¬0 ≤ a

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
h_1 : a ≤ x
rw : ENNReal.ofReal 0 = 0
rw₁ rw₂ : LE.le (α := ℝ) 0 0
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0

Tactic:
rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

Premises used: ENNReal.ofReal_eq_zero, if_neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ EqOn (β := ℝ≥0∞) (fun (y : ℝ) ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) (fun (x : ℝ) ↦ 0) (Iic x)

Tactic:
exact fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Tactic:
case neg =>
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
    exact fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

Premises used: ProbabilityTheory.exponentialPDF_eq, MeasureTheory.setLIntegral_congr_fun, MeasureTheory.lintegral_zero, measurableSet_Iic, ENNReal.ofReal_zero
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]

Premises used: le_refl, ProbabilityTheory.lintegral_exponentialPDF_of_nonpos, zero_add, OfNat.ofNat, lintegral_Iic_eq_lintegral_Iio_add_Icc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
simp :
  ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
simp only [exponentialPDF_eq]

Premises used: ProbabilityTheory.exponentialPDF_eq
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
ha : a ∈ Icc 0 x
⊢ Eq (α := ℝ≥0∞) ((fun (x : ℝ) ↦ ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)) a)
    ((fun (x : ℝ) ↦ ENNReal.ofReal (r * rexp (-(r * x)))) a)

Tactic:
simp [ha.1]

Premises used: And.left
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]

Premises used: MeasureTheory.setLIntegral_congr_fun, measurableSet_Icc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
rw₁ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))
rw₂ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))

Tactic:
rw [← ENNReal.toReal_eq_toReal_iff' _ ENNReal.ofReal_ne_top,
        ← integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun _ ↦ le_of_lt
        (mul_pos hr (exp_pos _)))]

Premises used: ENNReal.toReal_eq_toReal_iff', le_of_lt, Filter.Eventually.of_forall, mul_pos, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, ENNReal.ofReal_ne_top, Real.exp_pos
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a))) =
    HSMul.hSMul (α := ℝ) (β := ℝ) (if 0 ≤ x then 1 else -1)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (uIoc 0 x)) fun (x : ℝ) ↦ r * rexp (-(r * x)))
rw₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a))) =
    HMul.hMul (α := ℝ) (if 0 ≤ x then 1 else -1)
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (uIoc 0 x)) fun (x : ℝ) ↦ r * rexp (-(r * x)))
rw₂ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a))) =
    HMul.hMul (α := ℝ) 1
      (@integral _ _ _ _ measurableSpace (Measure.restrict volume (uIoc 0 x)) fun (x : ℝ) ↦ r * rexp (-(r * x)))
rw₃ rw₄ :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (@integral _ _ _ _ measurableSpace (Measure.restrict volume (uIoc 0 x)) fun (x : ℝ) ↦ r * rexp (-(r * x)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))

Tactic:
rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]

Premises used: intervalIntegral.intervalIntegral_eq_integral_uIoc, if_pos, smul_eq_mul, one_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))

Tactic:
have : ∫ a in uIoc 0 x, r * rexp (-(r * a)) = ∫ a in 0..x, r * rexp (-(r * a)) := by
        rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
rw : ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]

Premises used: Set.uIoc_of_le, MeasureTheory.integral_Icc_eq_integral_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
rw : -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
rw₁ : IntervalIntegrable (ε := ℝ) (fun (a : ℝ) ↦ r * rexp (-(r * a))) volume 0 x
rw₂ : ContinuousOn (Y := ℝ) (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (Icc 0 x)
rw₃ : ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]

Premises used: intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
nlinarith : 0 < -(r * x) → 0 - -(r * x) + (0 - (0 - r) * (0 - x)) = 0
⊢ -(r * x) ≤ 0

Tactic:
nlinarith
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
rw : -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Tactic:
rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]

Premises used: Iff.mpr, Real.exp_le_one_iff, ENNReal.toReal_ofReal_eq_iff, sub_nonneg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
norm_num : -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))

Tactic:
norm_num
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))

Tactic:
ring
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
simp : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (a : ℝ) ↦ r * rexp (-(r * a))) (Ioc 0 x) volume
⊢ IntervalIntegrable (ε := ℝ) (fun (a : ℝ) ↦ r * rexp (-(r * a))) volume 0 x

Tactic:
simp only [intervalIntegrable_iff, uIoc_of_le h]

Premises used: intervalIntegrable_iff, Set.uIoc_of_le
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (a : ℝ) ↦ r * rexp (-(r * a))) (Ioc 0 x) volume

Tactic:
Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn, ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (a : ℝ) ↦ r * rexp (-(r * a))) (Ioc 0 x) volume

Tactic:
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Premises used: MeasureTheory.Integrable.const_mul, ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
simp : Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-r * a)
⊢ Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-(r * a))

Tactic:
simp only [← neg_mul]

Premises used: neg_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-r * a)

Tactic:
(continuous_const_mul (-r)).rexp

Premises used: Continuous.rexp, continuous_const_mul, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-r * a)

Tactic:
exact (continuous_const_mul (-r)).rexp

Premises used: Continuous.rexp, continuous_const_mul, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-(r * a))

Tactic:
have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this_1 :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
this : Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-(r * a))
⊢ ContinuousOn (Y := ℝ) (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)

Premises used: Continuous.comp', Continuous.continuousOn, continuous_const_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this_1 :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
this : Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-(r * a))
⊢ ContinuousOn (Y := ℝ) (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (Icc 0 x)

Tactic:
exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)

Premises used: Continuous.comp', Continuous.continuousOn, continuous_const_mul, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
simp : ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
simp only [neg_mul, one_mul]

Premises used: neg_mul, one_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

Premises used: HasDerivAt.hasDerivWithinAt, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
⊢ ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1

Tactic:
exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp

Premises used: HasDerivAt.hasDerivWithinAt, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))

Tactic:
Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
refine : @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ rexp (-(r * x))) (Measure.restrict volume (Icc 0 x))
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))

Tactic:
refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)

Premises used: MeasureTheory.Integrable.aestronglyMeasurable, MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ rexp (-(r * x))) (Ioc 0 x) volume
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ rexp (-(r * x))) (Measure.restrict volume (Icc 0 x))

Tactic:
rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]

Premises used: MeasureTheory.IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
exp_neg_integrableOn_Ioc hr

Premises used: ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
exact exp_neg_integrableOn_Ioc hr

Premises used: ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞

Tactic:
ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)

Premises used: MeasureTheory.IntegrableOn.setLIntegral_lt_top, ne_of_lt
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
refine : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Icc 0 x) volume
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞

Tactic:
refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)

Premises used: MeasureTheory.IntegrableOn.setLIntegral_lt_top, ne_of_lt
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Ioc 0 x) volume
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Icc 0 x) volume

Tactic:
rw [integrableOn_Icc_iff_integrableOn_Ioc]

Premises used: integrableOn_Icc_iff_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Premises used: MeasureTheory.Integrable.const_mul, MeasureTheory.IntegrableOn, ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Ioc 0 x) volume

Tactic:
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Premises used: MeasureTheory.Integrable.const_mul, ProbabilityTheory.exp_neg_integrableOn_Ioc
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
rw : 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0
⊢ (↑(cdf (expMeasure r)) : ℝ → ℝ) x = if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
rw [cdf_expMeasure_eq_lintegral hr, lintegral_exponentialPDF_eq_antiDeriv hr x,
    ENNReal.toReal_ofReal_eq_iff]

Premises used: ProbabilityTheory.lintegral_exponentialPDF_eq_antiDeriv, ProbabilityTheory.cdf_expMeasure_eq_lintegral, ENNReal.toReal_ofReal_eq_iff
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
pos : ∀ (h : 0 ≤ x), 0 ≤ 1 - rexp (-(r * x))
neg : ∀ (h : ¬0 ≤ x), LE.le (α := ℝ) 0 0
⊢ 0 ≤ if 0 ≤ x then 1 - rexp (-(r * x)) else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
pos : 0 ≤ r * x
⊢ 0 ≤ 1 - rexp (-(r * x))

Tactic:
simp only [sub_nonneg, exp_le_one_iff, Left.neg_nonpos_iff]

Premises used: Left.neg_nonpos_iff, Real.exp_le_one_iff, sub_nonneg
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r * x

Tactic:
mul_nonneg hr.le h

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r * x

Tactic:
exact mul_nonneg hr.le h

Premises used: mul_nonneg, LT.lt.le
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ LE.le (α := ℝ) 0 0

Tactic:
le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Distributions.Exponential
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ LE.le (α := ℝ) 0 0

Tactic:
exact le_rfl

Premises used: le_rfl
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∀ (b : β), ∃ (a : ℕ), b ≤ t a

Tactic:
simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto

Premises used: StrictMono.monotone, Filter.tendsto_atTop_atTop_iff_of_monotone
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
x : β
hx : t 0 < x
ht_tendsto : ∀ (b : β), ∃ (a : ℕ), b ≤ t a
⊢ ∃ (n : ℕ), x ≤ t n

Tactic:
ht_tendsto x
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
x : β
hx : t 0 < x
ht_tendsto : ∀ (b : β), ∃ (a : ℕ), b ≤ t a
⊢ ∃ (n : ℕ), x ≤ t n

Tactic:
exact ht_tendsto x
-- Module: Mathlib.Probability.Distributions.Fernique
Goal:
β : Type u_1
inst : LinearOrder β
t : ℕ → β
ht_mono : StrictMono t
ht_tendsto : Tendsto t atTop atTop
x : β
hx : t 0 < x
⊢ ∃ (n : ℕ), x ≤ t n

Tactic:
have h : ∃ n, x ≤ t n := by
    simp only [tendsto_atTop_atTop_iff_of_monotone ht_mono.monotone] at ht_tendsto
    exact ht_tendsto x