-- Module: Mathlib.Probability.Distributions.Exponential
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)))
case₆ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
case₇ :
  (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
    (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
case₈ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))
case₉ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
case₁₀ :
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
    (Measure.restrict volume (Icc 0 x))
case₁₁ case₁₂ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = 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) _

Premises used: Iff.mpr, ENNReal.toReal_eq_toReal_iff', MeasureTheory.Integrable.aestronglyMeasurable, intervalIntegrable_iff, le_refl, HasDerivAt.hasDerivWithinAt, MeasureTheory.Integrable.const_mul, intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le, le_of_lt, ProbabilityTheory.exponentialPDF_eq, ProbabilityTheory.lintegral_exponentialPDF_of_nonpos, MeasureTheory.setLIntegral_congr_fun, MeasureTheory.IntegrableOn, MeasureTheory.IntegrableOn.setLIntegral_lt_top, Filter.Eventually.of_forall, zero_add, ProbabilityTheory.exp_neg_integrableOn_Ioc, ProbabilityTheory.hasDerivAt_neg_exp_mul_exp, mul_pos, measurableSet_Icc, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, integrableOn_Icc_iff_integrableOn_Ioc, neg_mul, Real.exp_le_one_iff, ENNReal.ofReal_ne_top, ENNReal.toReal_ofReal_eq_iff, OfNat.ofNat, ne_of_lt, sub_nonneg, Set.uIoc_of_le, one_mul, MeasureTheory.integral_Icc_eq_integral_Ioc, Real.exp_pos, lintegral_Iic_eq_lintegral_Iio_add_Icc