awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) =
    ((↑(Real.Gamma α) : ℂ) * (↑(Real.Gamma β) : ℂ) / (↑(Real.Gamma (α + β)) : ℂ)).re
have norm_cast : Real.Gamma α * Real.Gamma β / Real.Gamma (α + β) = Real.Gamma α * Real.Gamma β / Real.Gamma (α + β)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β x : ℝ
hx_pos : 0 < x
hx_lt : x < 1
⊢ betaPDF α β x = ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw : ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0) =
  ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [betaPDF_eq, if_pos ⟨hx_pos, hx_lt⟩]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β x : ℝ
hx_pos : 0 < x
hx_lt : x < 1
rw :
  ENNReal.ofReal (if 0 < x ∧ x < 1 then 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1) else 0) =
    ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ betaPDF α β x = ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₁ : ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) =
  ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [betaPDF_eq, if_pos ⟨hx_pos, hx_lt⟩]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw : (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₂ : 0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₃ : ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₄ : ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₅ : ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
    ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₇ : 0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₈ : ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₈ :
  ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₉ : ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₈ :
  ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₉ :
  ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₁₀ : ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₈ :
  ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₉ :
  ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₀ :
  ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₁₁ : ∫⁻ (x : ℝ) in Ioo 0 1, betaPDF α β x =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
rw :
  (∫⁻ (x : ℝ) in Iic 0, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁ : ℝ
rw₂ :
  0 + ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₃ :
  ∫⁻ (x : ℝ) in (Iic 0)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₄ :
  ∫⁻ (x : ℝ) in Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₅ :
  ∫⁻ (x : ℝ) in Ici 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) +
      ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₆ : ℝ
rw₇ :
  0 + ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₈ :
  ∫⁻ (x : ℝ) in (Ici 1)ᶜ, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₉ :
  ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂Measure.restrict volume (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₀ :
  ∫⁻ (x : ℝ) in Iio 1 ∩ Ioi 0, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
rw₁₁ :
  ∫⁻ (x : ℝ) in Ioo 0 1, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
have rw₁₂ : ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) ∂volume =
  ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Tactic: rw [← lintegral_add_compl _ measurableSet_Iic,
    setLIntegral_eq_zero measurableSet_Iic (fun x (hx : x ≤ 0) ↦ betaPDF_eq_zero_of_nonpos hx),
    zero_add, compl_Iic, ← lintegral_add_compl _ measurableSet_Ici,
    setLIntegral_eq_zero measurableSet_Ici (fun x (hx : 1 ≤ x) ↦ betaPDF_eq_zero_of_one_le hx),
    zero_add, compl_Ici, Measure.restrict_restrict measurableSet_Iio, Iio_inter_Ioi,
    setLIntegral_congr_fun measurableSet_Ioo
      (fun x ⟨hx_pos, hx_lt⟩ ↦ betaPDF_of_pos_lt_one hx_pos hx_lt)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 0 < betaPDFReal α β x
have rw : 0 < 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
Tactic: rw [betaPDFReal, if_pos ⟨hx1, hx2⟩]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β x : ℝ
hx1 : 0 < x
hx2 : x < 1
hα : 0 < α
hβ : 0 < β
⊢ 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 : ℝ), betaPDF α β x = 1
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
    1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
  1
Tactic: rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
    1
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
  1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
Tactic: rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
    1
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ioo 0 1))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1
have hfm : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ 1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) (Measure.restrict volume (Ioo 0 1))
Tactic: rw [lintegral_betaPDF, ← ENNReal.toReal_eq_one_iff, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      1 / beta α β * a ^ (α - 1) * (1 - a) ^ (β - 1))
    1
have simp_rw : (1 / beta α β *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      a ^ (α - 1) * (1 - a) ^ (β - 1)) =
  1
Tactic: simp_rw [mul_assoc, integral_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (1 / beta α β *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) =
    1
have field_simp : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
      a ^ (α - 1) * (1 - a) ^ (β - 1)) /
    beta α β =
  1
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Beta (goal)
Goal:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioo 0 1)) fun (a : ℝ) ↦
        a ^ (α - 1) * (1 - a) ^ (β - 1)) /
      beta α β =
    1
have 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)))
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]