awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Distributions.Fernique
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∞) μ
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set E) → ℝ≥0∞) Set.univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hμ_zero]
-- Module: Mathlib.Probability.Distributions.Fernique
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∞) μ
⊢ IsProbabilityMeasure μ'

Tactic:
have hμ' : IsProbabilityMeasure μ' := cond_isProbabilityMeasure <| by simp [hμ_zero]
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') =
    HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ))

Tactic:
simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]

Premises used: smul_smul, MeasureTheory.Measure.prod_smul_right, MeasureTheory.Measure.prod_smul_left
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
rw rw₁ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ
⊢ HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ

Tactic:
rw [h_rot]
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ =
    μ'.prod μ'

Tactic:
simp [hμ'_eq, Measure.prod_smul_left, Measure.prod_smul_right, smul_smul]

Premises used: smul_smul, MeasureTheory.Measure.prod_smul_right, MeasureTheory.Measure.prod_smul_left
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
calc :
  Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') =
    HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ))
calc₁ :
  HSMul.hSMul (β := Measure (E × E))
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞))
      (Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ.prod μ)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ
calc₂ :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞)
        (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) •
      μ.prod μ =
    μ'.prod μ'
⊢ Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4))) : (a : E × E) → E × E) (μ'.prod μ') = μ'.prod μ'

Tactic:
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]

Premises used: Real.pi, HMul.hMul, Set.univ, HDiv.hDiv, ContinuousLinearMap.rotation, Inv.inv, MeasureTheory.Measure.prod, MeasureTheory.Measure.map, OfNat.ofNat, DFunLike.coe, Neg.neg
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
⊢ 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]
-- Module: Mathlib.Probability.Distributions.Fernique
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 μ'
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)) μ
⊢ ∃ (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

Premises used: ProbabilityTheory.exists_integrable_exp_sq_of_map_rotation_eq_self_of_isProbabilityMeasure
-- Module: Mathlib.Probability.Distributions.Fernique
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)) μ

Tactic:
⟨C, hC_pos, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Probability.Distributions.Fernique
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 : Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ
⊢ ∃ (C : ℝ), 0 < C ∧ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
refine ⟨C, hC_pos, ?_⟩
-- Module: Mathlib.Probability.Distributions.Fernique
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∞)
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∞)
⊢ Integrable (ε := ℝ) (fun (x : E) ↦ rexp (C * HPow.hPow (β := ℕ) ‖x‖ 2)) μ

Tactic:
rwa [hμ'_eq, integrable_smul_measure] at hC

Premises used: MeasureTheory.integrable_smul_measure
-- Module: Mathlib.Probability.Distributions.Fernique
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))
    (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ)
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Distributions.Fernique
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))
    (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ)
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set E) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
simp [hμ_zero]
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
rw : Disjoint (Iio z) (Icc z y)
⊢ ∫⁻ (x : ℝ) in Iic y, f x = (∫⁻ (x : ℝ) in Iio z, f x) + ∫⁻ (x : ℝ) in Icc z y, f x

Tactic:
rw [← Iio_union_Icc_eq_Iic hzy, lintegral_union measurableSet_Icc]

Premises used: MeasureTheory.lintegral_union, measurableSet_Icc, Set.Iio_union_Icc_eq_Iic
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
simp_rw : ∀ ⦃a : ℝ⦄, a < z → ∀ ⦃b : ℝ⦄, z ≤ b ∧ b ≤ y → a ≠ b
⊢ Disjoint (Iio z) (Icc z y)

Tactic:
simp_rw [Set.disjoint_iff_forall_ne, mem_Iio, mem_Icc]

Premises used: Set.mem_Iio, Set.disjoint_iff_forall_ne, Set.mem_Icc
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
y z : ℝ
f : ℝ → ℝ≥0∞
hzy : z ≤ y
a : ℝ
h : a < z
b : ℝ
h_1 : z ≤ b ∧ b ≤ y
linarith : a = b → a - z + (z - b) + -(a - b) = 0
⊢ a ≠ b

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r x : ℝ
⊢ gammaPDF a r x = ENNReal.ofReal (if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0)

Tactic:
rfl

Premises used: ProbabilityTheory.gammaPDFReal, ProbabilityTheory.gammaPDF, rfl
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r x : ℝ
hx : x < 0
⊢ gammaPDF a r x = 0

Tactic:
simp only [gammaPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

Premises used: not_le, Iff.mpr, ProbabilityTheory.gammaPDF_eq, ENNReal.ofReal_zero, if_neg
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r x : ℝ
hx : 0 ≤ x
⊢ gammaPDF a r x = ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))

Tactic:
simp only [gammaPDF_eq, if_pos hx]

Premises used: if_pos, ProbabilityTheory.gammaPDF_eq
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a r : ℝ
hx : x ≤ 0
rw : ∫⁻ (x : ℝ) in Iio x, 0 = 0
rw₁ : EqOn (gammaPDF a r) (fun (x : ℝ) ↦ 0) (Iio x)
⊢ ∫⁻ (y : ℝ) in Iio x, gammaPDF a r y = 0

Tactic:
rw [setLIntegral_congr_fun (g := fun _ ↦ 0) measurableSet_Iio]

Premises used: measurableSet_Iio, MeasureTheory.setLIntegral_congr_fun
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a r : ℝ
hx : x ≤ 0
rw : Eq (α := ℝ≥0∞) 0 0
rw₁ rw₂ : ENNReal.ofReal 0 = ENNReal.ofReal 0
⊢ ∫⁻ (x : ℝ) in Iio x, 0 = 0

Tactic:
rw [lintegral_zero, ← ENNReal.ofReal_zero]

Premises used: MeasureTheory.lintegral_zero, ENNReal.ofReal_zero
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
a₁ : a < x → gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a
⊢ a ∈ Iio x → gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a

Tactic:
(_ : a < _)
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : a < x
simp : (if 0 ≤ a then r ^ a_1 / Gamma a_1 * a ^ (a_1 - 1) * rexp (-(r * a)) else 0) ≤ 0
⊢ gammaPDF a_1 r a = (fun (x : ℝ) ↦ (0 : ℝ≥0∞)) a

Tactic:
simp only [gammaPDF_eq, ENNReal.ofReal_eq_zero]

Premises used: ENNReal.ofReal_eq_zero, ProbabilityTheory.gammaPDF_eq
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : a < x
linarith : 0 ≤ a → x - 0 + (a - x) + (0 - a) = 0
⊢ ¬0 ≤ a

Tactic:
linarith
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a_1 r : ℝ
hx : x ≤ 0
a : ℝ
h : a < x
rw rw₁ : LE.le (α := ℝ) 0 0
⊢ (if 0 ≤ a then r ^ a_1 / Gamma a_1 * a ^ (a_1 - 1) * rexp (-(r * a)) else 0) ≤ 0

Tactic:
rw [if_neg (by linarith)]

Premises used: if_neg
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
⊢ Measurable (gammaPDFReal a r)

Tactic:
Measurable.ite measurableSet_Ici (((measurable_id'.pow_const _).const_mul _).mul
    (measurable_id'.const_mul _).neg.exp) measurable_const

Premises used: Measurable.mul, ProbabilityTheory.gammaPDFReal, Measurable.ite, Measurable.neg, measurable_id', measurable_const, Measurable.const_mul, Measurable.exp, Measurable.pow_const, measurableSet_Ici
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
⊢ StronglyMeasurable (gammaPDFReal a r)

Tactic:
(measurable_gammaPDFReal a r).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, ProbabilityTheory.measurable_gammaPDFReal
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
simp : 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
⊢ 0 < gammaPDFReal a r x

Tactic:
simp only [gammaPDFReal, if_pos hx.le]

Premises used: ProbabilityTheory.gammaPDFReal, LT.lt.le, if_pos
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
x a r : ℝ
ha : 0 < a
hr : 0 < r
hx : 0 < x
⊢ 0 < r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
pos : 0 ≤ x → 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))
neg : ¬0 ≤ x → LE.le (α := ℝ) 0 0
⊢ 0 ≤ if 0 ≤ x then r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)) else 0

Tactic:
split_ifs
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
h : 0 ≤ x
⊢ 0 ≤ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
h : ¬0 ≤ x
⊢ LE.le (α := ℝ) 0 0

Tactic:
positivity
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
rw : ∫⁻ (x : ℝ) in Iio 0, 0 ∂volume = 0
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0

Tactic:
rw [setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx), lintegral_zero]

Premises used: measurableSet_Iio, MeasureTheory.setLIntegral_congr_fun, MeasureTheory.lintegral_zero, ProbabilityTheory.gammaPDF_of_neg
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (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]
-- Module: Mathlib.Probability.Distributions.Gamma
Goal:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
⊢ ∫⁻ (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)
-- Module: Mathlib.Probability.Distributions.Gamma
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))
hfm :
  AEStronglyMeasurable (β := ℝ) (m₀ := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (Measure.restrict volume (Ici 0))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 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]

Premises used: MeasureTheory.lintegral_add_compl, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, Set.compl_Ici, add_zero, measurableSet_Ici, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.Probability.Distributions.Gamma
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)))
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
⊢ 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:
simp_rw [integral_Ici_eq_integral_Ioi, mul_assoc]

Premises used: MeasureTheory.integral_Ici_eq_integral_Ioi, mul_assoc
-- Module: Mathlib.Probability.Distributions.Gamma
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
rw₇ : r ^ a * (HPow.hPow (α := ℝ) 1 a / r ^ a) = 1
rw₈ : r ^ a * (1 / r ^ a) = 1
rw₉ : r ^ a / r ^ a = 1
rw₁₀ rw₁₁ : Eq (α := ℝ) 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

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']

Premises used: Real.Gamma_pos_of_pos, Real.rpow_pos_of_pos, MeasureTheory.integral_const_mul, mul_assoc, mul_div_assoc, LT.lt.le, Real.one_rpow, div_mul_eq_mul_div, Real.div_rpow, zero_le_one, LT.lt.ne', mul_one_div, Real.integral_rpow_mul_exp_neg_mul_Ioi, mul_one, div_self