awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (uIoc 0 x)) fun (a : ℝ) ↦
      r * rexp (-(r * a)))
    (∫ (a : ℝ) in 0..x, r * rexp (-(r * a)))
have 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)))
Tactic: rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (hypothesis)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have 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)))
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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw : ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
Tactic: rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw : -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (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))) _ _]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw₁ : IntervalIntegrable (ε := ℝ) (fun (a : ℝ) ↦ r * rexp (-(r * a))) volume 0 x
Tactic: rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw₂ : ContinuousOn (Y := ℝ) (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (Icc 0 x)
Tactic: rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)
⊢ ∫ (a : ℝ) in 0..x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw₃ : ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
Tactic: rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ -(r * x) ≤ 0
have nlinarith : 0 < -(r * x) → 0 - -(r * x) + (0 - (0 - r) * (0 - x)) = 0
Tactic: nlinarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
have rw : -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))
Tactic: rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))
have norm_num : -rexp (-(r * x)) + 1 = 1 - rexp (-(r * x))
Tactic: norm_num
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
⊢ IntervalIntegrable (ε := ℝ) (fun (a : ℝ) ↦ r * rexp (-(r * a))) volume 0 x
have simp : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (a : ℝ) ↦ r * rexp (-(r * a))) (Ioc 0 x) volume
Tactic: simp only [intervalIntegrable_iff, uIoc_of_le h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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))
have simp : Continuous (Y := ℝ) fun (a : ℝ) ↦ rexp (-r * a)
Tactic: simp only [← neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (hypothesis)
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)))
⊢ ContinuousOn (Y := ℝ) (fun (a : ℝ) ↦ -1 * rexp (-(r * a))) (Icc 0 x)
have this₁ : 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
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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 : ℝ) ↦ -1 * rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
have simp : ∀ x_1 ∈ Ioo 0 x, HasDerivWithinAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x_1))) (Ioi x_1) x_1
Tactic: simp only [neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))
have refine : @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ rexp (-(r * x))) (Measure.restrict volume (Icc 0 x))
Tactic: refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ @Integrable ℝ _ _ _ measurableSpace (fun (x : ℝ) ↦ rexp (-(r * x))) (Measure.restrict volume (Icc 0 x))
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ rexp (-(r * x))) (Ioc 0 x) volume
Tactic: rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
have refine : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Icc 0 x) volume
Tactic: refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Icc 0 x) volume
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x))) (Ioc 0 x) volume
Tactic: rw [integrableOn_Icc_iff_integrableOn_Ioc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
have case : (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
  ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    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 _)))]
    · 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]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (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)))
have case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    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 _)))]
    · 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]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (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)))
have case₂ : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    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 _)))]
    · 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]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₂ case₃ case₄ : ∫⁻ (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)))
have case₅ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    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 _)))]
    · 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]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
case :
  (∫⁻ (x : ℝ) in Iio 0, exponentialPDF r x) + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x =
    ENNReal.ofReal (1 - rexp (-(r * x)))
case₁ : 0 + ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₂ case₃ case₄ : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
case₅ :
  ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
have case₆ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: case pos =>
    rw [lintegral_Iic_eq_lintegral_Iio_add_Icc _ h, lintegral_exponentialPDF_of_nonpos (le_refl 0),
      zero_add]
    simp only [exponentialPDF_eq]
    rw [setLIntegral_congr_fun measurableSet_Icc (g := fun x ↦ ENNReal.ofReal (r * rexp (-(r * x))))
      (by intro a ha; simp [ha.1])]
    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 _)))]
    · 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]
      rw [integral_Icc_eq_integral_Ioc, ← uIoc_of_le h, this]
      rw [intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le h
        (f := fun a ↦ -1 * rexp (-(r * a))) _ _]
      · rw [ENNReal.toReal_ofReal_eq_iff.2
          (sub_nonneg.2 (Real.exp_le_one_iff.2 <| by nlinarith))]
        norm_num; ring
      · simp only [intervalIntegrable_iff, uIoc_of_le h]
        exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _
      · have : Continuous (fun a ↦ rexp (-(r * a))) := by
          simp only [← neg_mul]; exact (continuous_const_mul (-r)).rexp
        exact Continuous.continuousOn (Continuous.comp' (continuous_const_mul (-1)) this)
      · simp only [neg_mul, one_mul]
        exact fun _ _ ↦ HasDerivAt.hasDerivWithinAt hasDerivAt_neg_exp_mul_exp
    · refine Integrable.aestronglyMeasurable (Integrable.const_mul ?_ _)
      rw [← IntegrableOn, integrableOn_Icc_iff_integrableOn_Ioc]
      exact exp_neg_integrableOn_Ioc hr
    · refine ne_of_lt (IntegrableOn.setLIntegral_lt_top ?_)
      rw [integrableOn_Icc_iff_integrableOn_Ioc]
      exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _