awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
h : Disjoint (Function.support u) (Function.support v)
huint : Integrable u μ
hvint : Integrable v μ
hu : StronglyMeasurable u
hv : StronglyMeasurable v
hu_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
hv_eq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
pos : μ.real s • HAdd.hAdd (α := E) (∫ (a : Ω), u a ∂μ) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₁ :
  HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), u a ∂μ) + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) =
    ∫ (x : Ω) in s, (u + v) x ∂μ
pos₂ : ∫ (x : Ω) in s, u x ∂μ + HSMul.hSMul (β := E) (μ.real s) (∫ (a : Ω), v a ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₃ : HAdd.hAdd (α := E) (∫ (x : Ω) in s, u x ∂μ) (∫ (x : Ω) in s, v x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ
pos₄ pos₅ :
  HAdd.hAdd (α := E) (∫ (x : Ω) in s, u x ∂μ) (∫ (x : Ω) in s, v x ∂μ) =
    HAdd.hAdd (α := E) (∫ (a : Ω) in s, u a ∂μ) (∫ (a : Ω) in s, v a ∂μ)
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (u + v) x ∂μ) = ∫ (x : Ω) in s, (u + v) x ∂μ

Tactic:
rw [integral_add' huint hvint, smul_add, hu_eq, hv_eq,
      integral_add' huint.integrableOn hvint.integrableOn]

Premises used: MeasureTheory.integral_add', MeasureTheory.Integrable.integrableOn, smul_add
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ

Tactic:
simpa using continuous_integral.comp (ContinuousLinearMap.continuous (Submodule.subtypeL _))

Premises used: Submodule.subtypeL, Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_integral
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ

Tactic:
have h_integral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x, (f : Ω → E) x ∂μ := by
      simpa using continuous_integral.comp (ContinuousLinearMap.continuous (Submodule.subtypeL _))
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_integral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
⊢ Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ

Tactic:
simpa using (continuous_setIntegral s).comp
        (ContinuousLinearMap.continuous (Submodule.subtypeL _))

Premises used: Submodule.subtypeL, Continuous.comp, ContinuousLinearMap.continuous, MeasureTheory.continuous_setIntegral
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_integral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
⊢ Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ

Tactic:
have h_setIntegral : Continuous fun f : lpMeas E ℝ m₁ 1 μ => ∫ x in s, (f : Ω → E) x ∂μ := by
      simpa using (continuous_setIntegral s).comp
        (ContinuousLinearMap.continuous (Submodule.subtypeL _))
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_integral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
h_setIntegral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
⊢ IsClosed (X := ↥(lpMeas E ℝ m₁ 1 μ))
    {f : ↥(lpMeas E ℝ m₁ 1 μ) |
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ) =
        ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ}

Tactic:
isClosed_eq (Continuous.const_smul h_integral _) h_setIntegral

Premises used: isClosed_eq, Continuous.const_smul
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_integral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
h_setIntegral :
  Continuous (Y := E) fun (f : ↥(lpMeas E ℝ m₁ 1 μ)) ↦ ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ
⊢ IsClosed (X := ↥(lpMeas E ℝ m₁ 1 μ))
    {f : ↥(lpMeas E ℝ m₁ 1 μ) |
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ) =
        ∫ (x : Ω) in s, (↑(↑(↑f : ↥(Lp E 1 μ)) : Ω →ₘ[μ] E) : Ω → E) x ∂μ}

Tactic:
exact isClosed_eq (Continuous.const_smul h_integral _) h_setIntegral

Premises used: isClosed_eq, Continuous.const_smul
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
pos :
  MemLp u 1 μ →
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ →
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ
⊢ MemLp u 1 μ →
    HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ →
      HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ

Tactic:
_
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
rwa : ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x
⊢ HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), v x ∂μ) = ∫ (x : Ω) in s, v x ∂μ

Tactic:
rwa [← integral_congr_ae huv, ←
      (setIntegral_congr_ae (hle₂ _ hms) _ : ∫ x in s, u x ∂μ = ∫ x in s, v x ∂μ)]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.setIntegral_congr_ae
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h_1 : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
x : Ω
hx : u x = v x
h : x ∈ s → u x = v x
⊢ x ∈ s → u x = v x

Tactic:
_
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
x : Ω
hx : u x = v x
h_1 : x ∈ s
⊢ u x = v x

Tactic:
hx
-- Module: Mathlib.Probability.ConditionalExpectation
Goal:
Ω : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst_3 : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
u v : Ω → E
huv : u =ᶠ[ae μ] v
h_1 : MemLp u 1 μ
hueq : HSMul.hSMul (β := E) (μ.real s) (∫ (x : Ω), u x ∂μ) = ∫ (x : Ω) in s, u x ∂μ
h :
  ∀ (a : Ω),
    Membership.mem (γ := Set Ω)
      {x : Ω |
        Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ u x = v x) x} x →
          Membership.mem (γ := Set Ω) {x : Ω | (fun (x : Ω) ↦ x ∈ s → u x = v x) x} x}
      a
h₁ h₂ : ∀ (x : Ω) (hx : u x = v x), x ∈ s → u x = v x
⊢ ∀ᵐ (x : Ω) ∂μ, x ∈ s → u x = v x

Tactic:
filter_upwards [huv] with x hx _ using hx
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
simp : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ Eq (α := ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s) : (a : Set Ω) → ℝ≥0∞) univ : ℝ≥0∞)
    (1 : ℝ≥0∞)

Tactic:
simp only [Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
      Set.univ_inter, smul_eq_mul]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasureTheory.Measure.coe_smul, smul_eq_mul, MeasurableSet.univ, Pi.smul_apply
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
ENNReal.inv_mul_cancel hcs hs

Premises used: ENNReal.inv_mul_cancel
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
exact ENNReal.inv_mul_cancel hcs hs

Premises used: ENNReal.inv_mul_cancel
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
inst : IsFiniteMeasure μ
hcs : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ IsProbabilityMeasure μ[|s]

Tactic:
cond_isProbabilityMeasure_of_finite hcs (measure_ne_top μ s)

Premises used: ProbabilityTheory.cond_isProbabilityMeasure_of_finite, MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
measure_univ : Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (0 : ℝ≥0∞) ∨ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsZeroOrProbabilityMeasure μ[|s]

Tactic:
constructor
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
measure_univ :
  HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (0 : ℝ≥0∞) ∨ Eq (α := ℝ≥0∞) (μ[univ | s] : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp only [cond, Measure.coe_smul, Pi.smul_apply, MeasurableSet.univ, Measure.restrict_apply,
    univ_inter, smul_eq_mul, ← ENNReal.div_eq_inv_mul]

Premises used: MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasureTheory.Measure.coe_smul, smul_eq_mul, ProbabilityTheory.cond, MeasurableSet.univ, ENNReal.div_eq_inv_mul, Pi.smul_apply
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
measure_univ :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
measure_univ₁ :
  ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
rcases eq_or_ne (μ s) 0 with h | h

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
simp [h]
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
measure_univ :
  ∀ (h' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
measure_univ₁ :
  ∀ (h' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
      HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
rcases eq_or_ne (μ s) ∞ with h' | h'

Premises used: eq_or_ne, Top.top, DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
simp [h']
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
Ω' : Type u_2
α : Type u_3
m : MeasurableSpace Ω
m' : MeasurableSpace Ω'
μ : Measure Ω
s t : Set Ω
h : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 0 ∨
    HDiv.hDiv (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) = 1

Tactic:
simp [ENNReal.div_self h h']

Premises used: ENNReal.div_self
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
pos :
  ∀ (hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
      HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
neg :
  ∀ (hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
      HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)

Tactic:
by_cases hnt : μ s = ∞

Premises used: DFunLike.coe
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)

Tactic:
simp [hnt]
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hnt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) (toMeasurable μ s))⁻¹ : ℝ≥0∞) (μ.restrict (toMeasurable μ s)) =
    HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) s)⁻¹ : ℝ≥0∞) (μ.restrict s)

Tactic:
simp [Measure.restrict_toMeasurable hnt]

Premises used: MeasureTheory.Measure.restrict_toMeasurable
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ μ[|s] ≪ μ

Tactic:
smul_absolutelyContinuous.trans restrict_le_self.absolutelyContinuous

Premises used: MeasureTheory.Measure.AbsolutelyContinuous.trans, MeasureTheory.Measure.smul_absolutelyContinuous, LE.le.absolutelyContinuous, MeasureTheory.Measure.restrict_le_self, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
rw : μ ≪ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ
⊢ μ ≪ μ[|univ]

Tactic:
rw [cond, restrict_univ]

Premises used: ProbabilityTheory.cond, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ μ ≪ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ

Tactic:
absolutelyContinuous_smul ?_

Premises used: MeasureTheory.Measure.absolutelyContinuous_smul
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
refine : Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ ≪ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ

Tactic:
refine absolutelyContinuous_smul ?_

Premises used: MeasureTheory.Measure.absolutelyContinuous_smul
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsFiniteMeasure μ
⊢ Ne (α := ℝ≥0∞) (((μ : (a : Set Ω) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [measure_ne_top]

Premises used: MeasureTheory.measure_ne_top
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs : MeasurableSet s
p : Ω → Prop
h : ∀ x ∈ s, p x
⊢ ∀ᵐ (x : Ω) ∂μ[|s], p x

Tactic:
ae_smul_measure (ae_restrict_of_forall_mem hs h) _

Premises used: MeasureTheory.ae_restrict_of_forall_mem, MeasureTheory.Measure.ae_smul_measure, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs : NullMeasurableSet s μ
⊢ ∀ᵐ (x : Ω) ∂μ[|s], x ∈ s

Tactic:
ae_smul_measure (ae_restrict_mem₀ hs) _

Premises used: MeasureTheory.ae_restrict_mem₀, MeasureTheory.Measure.ae_smul_measure, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hs : MeasurableSet s
⊢ ∀ᵐ (x : Ω) ∂μ[|s], x ∈ s

Tactic:
ae_smul_measure (ae_restrict_mem hs) _

Premises used: MeasureTheory.ae_restrict_mem, MeasureTheory.Measure.ae_smul_measure, ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
⊢ μ[|∅] = 0

Tactic:
simp [cond]

Premises used: ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
inst : IsProbabilityMeasure μ
⊢ μ[|univ] = μ

Tactic:
simp [cond, measure_univ, Measure.restrict_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, ProbabilityTheory.cond, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
⊢ μ[|s] = 0 ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [cond]

Premises used: ProbabilityTheory.cond
-- Module: Mathlib.Probability.ConditionalProbability
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
s : Set Ω
hμs : Eq (α := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ[|s] = 0

Tactic:
simp [hμs]