-- Mathlib/Probability/Distributions/Exponential.lean
lemma lintegral_exponentialPDF_eq_antiDeriv {r : ℝ} (hr : 0 < r) (x : ℝ) :
    ∫⁻ y in Iic x, exponentialPDF r y
    = ENNReal.ofReal (if 0 ≤ x then 1 - exp (-(r * x)) else 0)

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

Tactic:
rw [ENNReal.toReal_ofReal_eq_iff.2 (by norm_num; positivity)]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ -1 * rexp (-(r * x)) - -1 * rexp (-(r * 0)) = 1 - rexp (-(r * x))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Ι 0 x, 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]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ 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 (ae_of_all _
    (by intro a ⟨(hle : _ ≤ a), _⟩; rw [if_pos hle]))]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) = ENNReal.ofReal (1 - rexp (-(r * x)))

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

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

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ IntervalIntegrable (fun a => r * rexp (-(r * a))) ℙ 0 x

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ ContinuousOn (fun a => -1 * rexp (-(r * a))) (Icc 0 x)

r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)

Tactic:
split_ifs with h

Result:
case pos
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))

case neg
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ 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]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iic x → ENNReal.ofReal (if 0 ≤ x_1 then r * rexp (-(r * x_1)) else 0) = 0

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ 0 ≤ r * x

Tactic:
positivity

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ IntegrableOn (fun a => r * rexp (-(r * a))) (Ioc 0 x) ℙ

Tactic:
exact Integrable.const_mul (exp_neg_integrableOn_Ioc hr) _

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
a : ℝ
hle : 0 ≤ a
right✝ : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = ?m.16773 a

Tactic:
rw [if_pos hle]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ ∀ᵐ (x_1 : ℝ), x_1 ∈ Iic x → ENNReal.ofReal (if 0 ≤ x_1 then r * rexp (-(r * x_1)) else 0) = 0

Tactic:
exact ae_of_all _ fun a (_ : a ≤ _) ↦ by rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

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]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ ∫ (a : ℝ) in Icc 0 x, r * rexp (-(r * a)) = (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, r * rexp (-(r * a)) = ∫ (a : ℝ) in 0 ..x, r * rexp (-(r * a))
⊢ ∫ (a : ℝ) in Icc 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]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

Proof state:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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

Tactic:
simp only [neg_mul, one_mul]

Result:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
this : ∫ (a : ℝ) in Ι 0 x, 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