awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (hypothesis)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have h_rot₁ : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
Tactic: have h_rot : (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4))) = μ'.prod μ' := by
    calc (μ'.prod μ').map (ContinuousLinearMap.rotation (-(π / 4)))
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹)
        • (μ.prod μ).map (ContinuousLinearMap.rotation (-(π / 4))) := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
    _ = ((μ Set.univ)⁻¹ * (μ Set.univ)⁻¹) • (μ.prod μ) := by rw [h_rot]
    _ = μ'.prod μ' := by
      simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot_1 : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : ∀ (C : ℝ) (hC_pos : 0 < C) (hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ'),
  ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: obtain ⟨C, hC_pos, hC⟩ :=
    exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure (μ := μ') h_rot
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot_1 : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ'
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
Tactic: refine ⟨C, hC_pos, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot_1 : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ'
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg : ∀
  (hC :
    Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
      (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ)),
  Ne (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [hμ'_eq, integrable_smul_measure] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Probability.Distributions.Fernique (goal)
Goal:
E : Type u_1
inst : SeminormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SecondCountableTopology E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
μ : Measure E
inst_5 : IsFiniteMeasure μ
h_rot_1 : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
hμ' : IsProbabilityMeasure μ'
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'
C : ℝ
hC_pos : 0 < C
hC : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ'
neg :
  ∀
    (hC :
      Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
        (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ)),
    Ne (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
have neg₁ : ∀
  (hC :
    Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2))
      (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ)),
  Ne (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rwa [hμ'_eq, integrable_smul_measure] at hC
Cleared hypotheses: hC
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ ∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x
have rw : Disjoint (Iio z) (Icc z y)
Tactic: rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
⊢ Disjoint (Iio z) (Icc z y)
have simp_rw : ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, z ≤ b ∧ b ≤ y → a ≠ b
Tactic: simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a : ℝ
h : a < z
b : ℝ
h_1 : z ≤ b ∧ b ≤ y
⊢ a ≠ b
have linarith : a = b → a - z + (z - b) + -(a - b) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0
have rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
Tactic: rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a r : ℝ
hx : x ≤ 0
rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0
have rw₁ : EqOn (gammaPDF a r) (fun (x : ℝ) ↦ 0) (Iio x)
Tactic: rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a r : ℝ
hx : x ≤ 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0
have rw : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [lintegral_zero, ← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a r : ℝ
hx : x ≤ 0
rw : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0
have rw₁ : ENNReal.ofReal 0 = ENNReal.ofReal 0
Tactic: rw [lintegral_zero, ← ENNReal.ofReal_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
⊢ a ∈ Iio x → gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
have a₁ : a < x → gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
Tactic: (_ : a < _)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : a < x
⊢ gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
have simp : (if 0 ≤ a then r ^ a_1 / Gamma a_1 * a ^ (a_1 - 1) * rexp (-(r * a)) else 0) ≤ 0
Tactic: simp only [gammaPDF_eq, ENNReal.ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : 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.Gamma (goal)
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : a < x
⊢ (if 0 ≤ a then r ^ a_1 / Gamma a_1 * a ^ (a_1 - 1) * rexp (-(r * a)) else 0) ≤ 0
have rw : LE.le (α := ℝ) 0 0
Tactic: rw [if_neg (by linarith)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < gammaPDFReal a r x
have simp : 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Tactic: simp only [gammaPDFReal, if_pos hx.le]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
⊢ 0 ≤ if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0
have pos : 0 ≤ x → 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
pos : 0 ≤ x → 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ 0 ≤ if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0
have neg : ¬0 ≤ x → LE.le (α := ℝ) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
have rw : ∫⁻ (x : ℝ) in Iio 0, 0 ∂volume = 0
Tactic: rw [setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
rw : ∫⁻ (x : ℝ) in Iio 0, 0 ∂volume = 0
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (hypothesis)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1
have leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
Tactic: have leftSide : ∫⁻ x in Iio 0, gammaPDF a r x = 0 := by
    rw [setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (hypothesis)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1
have rightSide : ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
  ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
Tactic: have rightSide : ∫⁻ x in Ici 0, gammaPDF a r x =
      ∫⁻ x in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * exp (-(r * x))) :=
    setLIntegral_congr_fun measurableSet_Ici (fun _ ↦ gammaPDF_of_nonneg)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici 0)) fun (a_1 : ℝ) ↦
    r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)))
  1
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)))
    1
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1
have hf : (ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
  r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)))
    1
hf :
  (ae (F := Measure ℝ) (Measure.restrict volume (Ici 0))).EventuallyLE (β := ℝ) 0 fun (x : ℝ) ↦
    r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1
have hfm : AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (Measure.restrict volume (Ici 0))
Tactic: rw [← ENNReal.toReal_eq_one_iff, ← lintegral_add_compl _ measurableSet_Ici, compl_Ici,
    leftSide, rightSide, add_zero, ← integral_eq_lintegral_of_nonneg_ae]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ici 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * a_1 ^ (a - 1) * rexp (-(r * a_1)))
    1
have simp_rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
    r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
  1
Tactic: simp_rw [integral_Ici_eq_integral_Ioi, mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw : (r ^ a / Gamma a *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      a_1 ^ (a - 1) * rexp (-(r * a_1))) =
  1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₆ : r ^ a * (1 / r) ^ a = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gamma (goal)
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
rw :
  (r ^ a / Gamma a *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
        a_1 ^ (a - 1) * rexp (-(r * a_1))) =
    1
rw₁ : r ^ a / Gamma a * ((1 / r) ^ a * Gamma a) = 1
rw₂ : r ^ a * ((1 / r) ^ a * Gamma a) / Gamma a = 1
rw₃ : r ^ a * (1 / r) ^ a * Gamma a / Gamma a = 1
rw₄ : r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1
rw₅ : r ^ a * (1 / r) ^ a * 1 = 1
rw₆ : r ^ a * (1 / r) ^ a = 1
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (a_1 : ℝ) ↦
      r ^ a / Gamma a * (a_1 ^ (a - 1) * rexp (-(r * a_1))))
    1
have rw₇ : r ^ a * (HPow.hPow (α := ℝ) 1 a / r ^ a) = 1
Tactic: rw [integral_const_mul, integral_rpow_mul_exp_neg_mul_Ioi ha hr, div_mul_eq_mul_div,
      ← mul_assoc, mul_div_assoc, div_self (Gamma_pos_of_pos ha).ne', mul_one,
      div_rpow zero_le_one hr.le, one_rpow, mul_one_div, div_self (rpow_pos_of_pos hr _).ne']