awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (t : ℝ) ↦
      t ^ (α - 1) * (1 - t) ^ (β - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)))
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) /
      beta α β =
    1
have rw₁ : @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
  (Measure.restrict volume (Ioc 0 1))
Tactic: rw [div_eq_one_iff_eq (ne_of_gt (beta_pos hα hβ)), beta_eq_betaIntegralReal α β hα hβ,
      betaIntegral, intervalIntegral.integral_of_le (by norm_num),
      ← integral_Ioc_eq_integral_Ioo, ← RCLike.re_to_complex, ← integral_re]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 1)) fun (t : ℝ) ↦
      t ^ (α - 1) * (1 - t) ^ (β - 1))
    (@integral _ _ _ _ Real.measurableSpace (Measure.restrict volume (Ioc 0 1)) fun (x : ℝ) ↦
      (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)))
have refine : ∀ (x : ℝ),
  Membership.mem (γ := Set ℝ) (Ioc 0 1) x →
    ∀ (hx1 : 0 < x) (hx₂ : x ≤ 1),
      x ^ (α - 1) * (1 - x) ^ (β - 1) =
        (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
Tactic: refine setIntegral_congr_fun measurableSet_Ioc fun x ⟨hx1, hx₂⟩ ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
have norm_cast : x ^ (α - 1) * (1 - x) ^ (β - 1) =
  (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑(α - 1) : ℂ) * (↑(1 - x) : ℂ) ^ (↑(β - 1) : ℂ))
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑(α - 1) : ℂ) * (↑(1 - x) : ℂ) ^ (↑(β - 1) : ℂ))
have hx : 0 ≤ 1 - x
Tactic: rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex,
        Complex.re_mul_ofReal, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
hx : 0 ≤ 1 - x
⊢ x ^ (α - 1) * (1 - x) ^ (β - 1) =
    (RCLike.re : (a : ℂ) → ℝ) ((↑x : ℂ) ^ (↑(α - 1) : ℂ) * (↑(1 - x) : ℂ) ^ (↑(β - 1) : ℂ))
have hx₁ : 0 ≤ x
Tactic: rw [← Complex.ofReal_cpow, ← Complex.ofReal_cpow, RCLike.re_to_complex,
        Complex.re_mul_ofReal, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ 1 - x
have linarith : 1 - x < 0 → x - 1 + (1 - x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
h : Membership.mem (γ := Set ℝ) (Ioc 0 1) x
hx1 : 0 < x
hx₂ : x ≤ 1
⊢ 0 ≤ x
have linarith : x < 0 → 0 - x + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))
have a : @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1)) ↔
  IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) volume 0 1
Tactic: convert! betaIntegral_convergent (u := α) (v := β) (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) volume 0 1
have a : @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1)) ↔
  IntegrableOn (ε := ℂ) (mα := Real.measurableSpace)
    (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) (Ioc 0 1) volume
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
a :
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntegrableOn (ε := ℂ) (mα := Real.measurableSpace)
      (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) (Ioc 0 1) volume
⊢ @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
      (Measure.restrict volume (Ioc 0 1)) ↔
    IntervalIntegrable (ε := ℂ) (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1)) volume 0 1
have a₁ : @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1)) ↔
  @Integrable ℂ _ _ _ Real.measurableSpace (fun (x : ℝ) ↦ (↑x : ℂ) ^ ((↑α : ℂ) - 1) * (1 - (↑x : ℂ)) ^ ((↑β : ℂ) - 1))
    (Measure.restrict volume (Ioc 0 1))
Tactic: rw [intervalIntegrable_iff_integrableOn_Ioc_of_le (by simp), IntegrableOn]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
have hf : ∀ (x : ℝ) (hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x),
  LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x)
Tactic: refine ae_restrict_of_forall_mem measurableSet_Ioo (fun x hx ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ LE.le (α := ℝ) (0 x) ((fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x)
have h : (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x
Tactic: convert! betaPDFReal_pos hx.1 hx.2 hα hβ |>.le using 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
⊢ (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x
have h : (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x =
  if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0
Tactic: rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
x : ℝ
hx : Membership.mem (γ := Set ℝ) (Ioo 0 1) x
h :
  (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x =
    if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0
⊢ (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = betaPDFReal α β x
have h₁ : (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) x = 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
Tactic: rw [betaPDFReal, if_pos ⟨hx.1, hx.2⟩]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Binomial (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (ω : Ω) ∂P, X ω ≤ n
have rw : ∀ᵐ (x : Set ℕ) ∂setBer(Set.Iio n, p), x.ncard ≤ n
Tactic: rw [hX.ae_iff (p := (· ≤ n)) <| by fun_prop, binomial,
    ae_map_iff (by fun_prop) (Set.finite_Iic _).measurableSet]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Binomial (goal)
Goal:
Ω : Type u_2
m : MeasurableSpace Ω
P : Measure Ω
n : ℕ
p : (↑I : Type)
X : Ω → ℕ
hX : HasLaw X Bin(n, p) P
⊢ ∀ᵐ (x : Set ℕ) ∂setBer(Set.Iio n, p), x.ncard ≤ n
have h : ∀ (s : Set ℕ) (hs : s ⊆ Set.Iio n), s.ncard ≤ n
Tactic: filter_upwards [setBernoulli_ae_subset] with s hs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
⊢ cauchyPDFReal x₀ 0 = 0
have h : ∀ (x : ℝ), cauchyPDFReal x₀ 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
have pos : ∀ (h : γ = 0),
  π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
Tactic: by_cases h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
x : ℝ
pos :
  ∀ (h : γ = 0),
    π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
      π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
⊢ π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
have neg : ∀ (h : ¬γ = 0),
  π⁻¹ * (↑γ : ℝ) * (HPow.hPow (β := ℕ) (x - x₀) 2 + HPow.hPow (β := ℕ) (↑γ : ℝ) 2)⁻¹ =
    π⁻¹ * (↑γ⁻¹ : ℝ) * (1 + HPow.hPow (β := ℕ) ((x - x₀) / (↑γ : ℝ)) 2)⁻¹
Tactic: by_cases h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
⊢ cauchyPDF x₀ 0 = 0
have h : ∀ (x : ℝ), cauchyPDF x₀ 0 x = 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : ℝ) ↦ cauchyPDFReal x₀ γ x) 1
have simp : π⁻¹ * (↑γ : ℝ)⁻¹ * ((↑γ : ℝ) * π) = 1
Tactic: simp [cauchyPDFReal_def', NNReal.coe_inv, integral_const_mul,
    integral_sub_right_eq_self (f := fun x : ℝ ↦ (1 + (x / ↑γ) ^ 2)⁻¹),
    integral_comp_div (g := fun x : ℝ ↦ (1 + x ^ 2)⁻¹)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
have pos : ∀ (h : γ = 0), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
Tactic: by_cases! h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
pos : ∀ (h : γ = 0), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
have neg : ∀ (h : γ ≠ 0), @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
Tactic: by_cases! h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
have pos : @Integrable ℝ _ _ ℝ MeasureSpace.toMeasurableSpace 0 volume
Tactic: simp only [h, cauchyPDFReal_scale_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
h : γ ≠ 0
⊢ @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (cauchyPDFReal x₀ γ) volume
have neg : Ne (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 0
Tactic: apply Integrable.of_integral_ne_zero
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1
have rw : (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae
    (ae_of_all _ fun x ↦ (cauchyPDF_pos x₀ hγ x).le) (by fun_prop),
    integral_cauchyPDFReal_eq_one x₀ hγ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
rw : (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1
have rw₁ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 1
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae
    (ae_of_all _ fun x ↦ (cauchyPDF_pos x₀ hγ x).le) (by fun_prop),
    integral_cauchyPDFReal_eq_one x₀ hγ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
rw : (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1
rw₁ : Eq (α := ℝ) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : ℝ) ↦ cauchyPDFReal x₀ γ a) 1
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae
    (ae_of_all _ fun x ↦ (cauchyPDF_pos x₀ hγ x).le) (by fun_prop),
    integral_cauchyPDFReal_eq_one x₀ hγ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
⊢ Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have pos : ∀ (h : γ = 0), Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: by_cases h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Cauchy (goal)
Goal:
x₀ : ℝ
γ : ℝ≥0
pos : ∀ (h : γ = 0), Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have neg : ∀ (h : ¬γ = 0), Eq (α := ℝ≥0∞) ((cauchyMeasure x₀ γ : (a : Set ℝ) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: by_cases h : γ = 0
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r x : ℝ
⊢ HasDerivAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x))) x
have h : Eq (α := ℝ → ℝ) (fun (a : ℝ) ↦ -rexp (-(r * a))) fun (y : ℝ) ↦ -1 * rexp (-r * id y)
Tactic: convert! (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r x : ℝ
h : Eq (α := ℝ → ℝ) (fun (a : ℝ) ↦ -rexp (-(r * a))) fun (y : ℝ) ↦ -1 * rexp (-r * id y)
⊢ HasDerivAt (fun (a : ℝ) ↦ -rexp (-(r * a))) (r * rexp (-(r * x))) x
have h₁ : r * rexp (-(r * x)) = -1 * (rexp (-r * id x) * (-r * 1))
Tactic: convert! (((hasDerivAt_id x).const_mul (-r)).exp.const_mul (-1)) using 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
b x : ℝ
hb : 0 < b
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-(b * x))) (Ioc 0 x) volume
have simp : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (x : ℝ) ↦ rexp (-b * x)) (Ioc 0 x) volume
Tactic: simp only [neg_mul_eq_neg_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)
have split_ifs : ∀ (h : 0 ≤ x), ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
split_ifs : ∀ (h : 0 ≤ x), ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (1 - rexp (-(r * x)))
⊢ ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal (if 0 ≤ x then 1 - rexp (-(r * x)) else 0)
have split_ifs₁ : ∀ (h : ¬0 ≤ x), ∫⁻ (y : ℝ) in Iic x, exponentialPDF r y = ENNReal.ofReal 0
Tactic: split_ifs with h
-- 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 0
have simp : ∫⁻ (y : ℝ) in Iic x, ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0) = ENNReal.ofReal 0
Tactic: simp only [exponentialPDF_eq]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
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
have rw : EqOn (β := ℝ≥0∞) (fun (y : ℝ) ↦ ENNReal.ofReal (if 0 ≤ y then r * rexp (-(r * y)) else 0)) (fun (x : ℝ) ↦ 0) (Iic x)
Tactic: rw [setLIntegral_congr_fun measurableSet_Iic, lintegral_zero, ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
h_1 : a ≤ x
⊢ ¬0 ≤ a
have linarith : 0 ≤ a → x - 0 + (a - x) + (0 - a) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
h_1 : a ≤ x
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0
have rw : ENNReal.ofReal 0 = 0
Tactic: rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
a : ℝ
h_1 : a ≤ x
rw : ENNReal.ofReal 0 = 0
⊢ ENNReal.ofReal (if 0 ≤ a then r * rexp (-(r * a)) else 0) = 0
have rw₁ : LE.le (α := ℝ) 0 0
Tactic: rw [if_neg (by linarith), ENNReal.ofReal_eq_zero]
-- 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 rw : ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = 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]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
Goal:
r : ℝ
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ ∫⁻ (x : ℝ) in Icc 0 x, exponentialPDF r x = ENNReal.ofReal (1 - rexp (-(r * x)))
have simp : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0) = ENNReal.ofReal (1 - rexp (-(r * x)))
Tactic: simp only [exponentialPDF_eq]
-- 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 (if 0 ≤ x then r * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (1 - rexp (-(r * x)))
have rw : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = 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])]
-- 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 = ENNReal.ofReal (1 - rexp (-(r * x)))
have rw : (@integral _ _ _ _ measurableSpace (Measure.restrict volume (Icc 0 x)) fun (a : ℝ) ↦ r * rexp (-(r * a))) =
  (ENNReal.ofReal (1 - rexp (-(r * x)))).toReal
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 _)))]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
have rw₁ : AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ r * rexp (-(r * x)))
  (Measure.restrict volume (Icc 0 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 _)))]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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))
⊢ ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume = ENNReal.ofReal (1 - rexp (-(r * x)))
have rw₂ : ∫⁻ (x : ℝ) in Icc 0 x, ENNReal.ofReal (r * rexp (-(r * x))) ∂volume ≠ ∞
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 _)))]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Exponential (goal)
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)))
have 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)))
Tactic: 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
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)))
⊢ 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₁ : (@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)))
Tactic: 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
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)))
⊢ 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₂ : (@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)))
Tactic: rw [intervalIntegral.intervalIntegral_eq_integral_uIoc, smul_eq_mul, if_pos h, one_mul]