awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst : NoAtoms μ
rw : ∀ i ∈ s, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {i} : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rw [← biUnion_of_singleton s, measure_biUnion_null_iff h]

Premises used: Set.biUnion_of_singleton, MeasureTheory.measure_biUnion_null_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst : NoAtoms μ
⊢ ∀ i ∈ s, Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) {i} : ENNReal) (0 : ENNReal)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst : NoAtoms μ
⊢ ∀ᵐ (x : α) ∂μ, x ∉ s

Tactic:
simpa only [ae_iff, Classical.not_not] using h.measure_zero μ

Premises used: Classical.not_not, Set.Countable.measure_zero, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
a : α
⊢ ∀ᵐ (x : α) ∂μ, x ≠ a

Tactic:
(countable_singleton a).ae_notMem μ

Premises used: Set.Mem, setOf, Set.Countable.ae_notMem, Set.singleton, Set.countable_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Countable
μ : Measure α
inst : NoAtoms μ
⊢ μ.restrict sᶜ = μ

Tactic:
restrict_eq_self_of_ae_mem <| h.ae_notMem μ

Premises used: Set.Countable.ae_notMem, MeasureTheory.Measure.restrict_eq_self_of_ae_mem
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
a : α
⊢ μ.restrict {a}ᶜ = μ

Tactic:
(countable_singleton _).measure_restrict_compl μ

Premises used: Set.Countable.measure_restrict_compl, Set.countable_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : s.Finite
μ : Measure α
inst : NoAtoms μ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
h.countable.measure_zero μ

Premises used: Set.Countable.measure_zero, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Finset α
μ : Measure α
inst : NoAtoms μ
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (↑s : Set α) : ENNReal) (0 : ENNReal)

Tactic:
s.finite_toSet.measure_zero μ

Premises used: Set.Finite.measure_zero, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
a : α
s : Set α
⊢ insert a s =ᶠ[ae μ] s

Tactic:
union_ae_eq_right.2 <| measure_mono_null diff_subset (measure_singleton _)

Premises used: Iff.mpr, Set.diff_subset, Set.insert, Set.Mem, MeasureTheory.union_ae_eq_right, setOf, MeasureTheory.measure_mono_null, MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
by_contra! : ∀ (h : ∀ (x : X), ¬AccPt x (𝓟 E)), False
⊢ ∃ (x : X), AccPt x (𝓟 E)

Tactic:
by_contra! h
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
h : ∀ (x : X), ¬AccPt x (𝓟 E)
⊢ DiscreteTopology.{u_2} (↑E : Type u_2)

Tactic:
haveI : DiscreteTopology E := discreteTopology_of_noAccPts fun x _ => h x
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
h : ∀ (x : X), ¬AccPt x (𝓟 E)
this : DiscreteTopology.{u_2} (↑E : Type u_2)
⊢ False

Tactic:
hE.ne' <| (Set.countable_coe_iff.mp <| separableSpace_iff_countable.mp ‹_›).measure_zero μ

Premises used: Set.countable_coe_iff, Set.Countable.measure_zero, LT.lt.ne', Iff.mp, TopologicalSpace.separableSpace_iff_countable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
X : Type u_2
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
μ : Measure X
inst_2 : NoAtoms μ
E : Set X
inst_3 : SeparableSpace.{u_2} (↑E : Type u_2)
hE : LT.lt (α := ENNReal) (0 : ENNReal) ((μ : (a : Set X) → ENNReal) E : ENNReal)
h : ∀ (x : X), ¬AccPt x (𝓟 E)
this : DiscreteTopology.{u_2} (↑E : Type u_2)
⊢ False

Tactic:
exact hE.ne' <| (Set.countable_coe_iff.mp <| separableSpace_iff_countable.mp ‹_›).measure_zero μ

Premises used: Set.countable_coe_iff, Set.Countable.measure_zero, LT.lt.ne', Iff.mp, TopologicalSpace.separableSpace_iff_countable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a : α
⊢ Iio a =ᶠ[ae μ] Iic a

Tactic:
Iio_ae_eq_Iic' (measure_singleton a)

Premises used: MeasureTheory.Iio_ae_eq_Iic', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a : α
⊢ Ioi a =ᶠ[ae μ] Ici a

Tactic:
Ioi_ae_eq_Ici' (measure_singleton a)

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.Ioi_ae_eq_Ici'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ioo a b =ᶠ[ae μ] Ioc a b

Tactic:
Ioo_ae_eq_Ioc' (measure_singleton b)

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.Ioo_ae_eq_Ioc'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ioc a b =ᶠ[ae μ] Icc a b

Tactic:
Ioc_ae_eq_Icc' (measure_singleton a)

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.Ioc_ae_eq_Icc'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ioo a b =ᶠ[ae μ] Ico a b

Tactic:
Ioo_ae_eq_Ico' (measure_singleton a)

Premises used: MeasureTheory.Ioo_ae_eq_Ico', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ioo a b =ᶠ[ae μ] Icc a b

Tactic:
Ioo_ae_eq_Icc' (measure_singleton a) (measure_singleton b)

Premises used: MeasureTheory.NoAtoms.measure_singleton, MeasureTheory.Ioo_ae_eq_Icc'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ico a b =ᶠ[ae μ] Icc a b

Tactic:
Ico_ae_eq_Icc' (measure_singleton b)

Premises used: MeasureTheory.Ico_ae_eq_Icc', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ Ico a b =ᶠ[ae μ] Ioc a b

Tactic:
Ico_ae_eq_Ioc' (measure_singleton a) (measure_singleton b)

Premises used: MeasureTheory.Ico_ae_eq_Ioc', MeasureTheory.NoAtoms.measure_singleton
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a : α
⊢ μ.restrict (Iio a) = μ.restrict (Iic a)

Tactic:
restrict_congr_set Iio_ae_eq_Iic

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Iio_ae_eq_Iic
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a : α
⊢ μ.restrict (Ioi a) = μ.restrict (Ici a)

Tactic:
restrict_congr_set Ioi_ae_eq_Ici

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioi_ae_eq_Ici
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ioo a b) = μ.restrict (Ioc a b)

Tactic:
restrict_congr_set Ioo_ae_eq_Ioc

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ioc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ioc a b) = μ.restrict (Icc a b)

Tactic:
restrict_congr_set Ioc_ae_eq_Icc

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioc_ae_eq_Icc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ioo a b) = μ.restrict (Ico a b)

Tactic:
restrict_congr_set Ioo_ae_eq_Ico

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Ico
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ioo a b) = μ.restrict (Icc a b)

Tactic:
restrict_congr_set Ioo_ae_eq_Icc

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ioo_ae_eq_Icc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ico a b) = μ.restrict (Icc a b)

Tactic:
restrict_congr_set Ico_ae_eq_Icc

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ico_ae_eq_Icc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : PartialOrder α
a b : α
⊢ μ.restrict (Ico a b) = μ.restrict (Ioc a b)

Tactic:
restrict_congr_set Ico_ae_eq_Ioc

Premises used: MeasureTheory.Measure.restrict_congr_set, MeasureTheory.Ico_ae_eq_Ioc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.NoAtoms
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : NoAtoms μ
inst_1 : LinearOrder α
a b : α
⊢ Ι a b =ᶠ[ae μ] [[a, b]]

Tactic:
Ioc_ae_eq_Icc

Premises used: Set.uIoc, MeasureTheory.Ioc_ae_eq_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsZeroOrProbabilityMeasure μ ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞) ∨
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
⟨fun _ ↦ IsZeroOrProbabilityMeasure.measure_univ, IsZeroOrProbabilityMeasure.mk⟩

Premises used: MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ, Iff.intro, MeasureTheory.IsZeroOrProbabilityMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
apply : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
apply (measure_mono (subset_univ _)).trans

Premises used: Set.subset_univ, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
inl :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
inr :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)),
    LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rcases IsZeroOrProbabilityMeasure.measure_univ (μ := μ) with h | h

Premises used: MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
s : Set α
⊢ μ.real s ≤ 1

Tactic:
ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.ofReal_one.symm ▸ prob_le_one)

Premises used: MeasureTheory.prob_le_one, MeasureTheory.Measure.real, Eq.rec, ENNReal.ofReal_one, zero_le_one, ENNReal.toReal_le_of_le_ofReal, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
⊢ LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
⟨fun h => le_antisymm prob_le_one h, fun h => h ▸ le_refl _⟩

Premises used: le_refl, MeasureTheory.prob_le_one, Eq.rec, le_antisymm, Iff.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
μ : Measure α
inst_1 : IsZeroOrProbabilityMeasure μ
⊢ IsFiniteMeasure μ

Tactic:
⟨prob_le_one.trans_lt one_lt_top⟩

Premises used: MeasureTheory.prob_le_one, ENNReal.one_lt_top, MeasureTheory.IsFiniteMeasure.mk, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
⊢ IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0

Tactic:
⟨Or.inl rfl⟩

Premises used: Or.inl, MeasureTheory.IsZeroOrProbabilityMeasure.mk, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsProbabilityMeasure μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
⟨fun _ ↦ measure_univ, IsProbabilityMeasure.mk⟩

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, Iff.intro, MeasureTheory.IsProbabilityMeasure.mk
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
⊢ IsZeroOrProbabilityMeasure μ

Tactic:
⟨Or.inr measure_univ⟩

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.IsZeroOrProbabilityMeasure.mk, Or.inr
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
by_contra! : ∀ (maybe_empty : IsEmpty α), False
⊢ Nonempty α

Tactic:
by_contra! maybe_empty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]

Premises used: Iff.mpr, Set.univ_eq_empty_iff, MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
have : μ Set.univ = 0 := by
    rw [Set.univ_eq_empty_iff.mpr maybe_empty, measure_empty]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
maybe_empty : IsEmpty α
this : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ False

Tactic:
simp at this
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
μ : Measure α
inst_1 : IsProbabilityMeasure μ
⊢ NeZero μ

Tactic:
⟨IsProbabilityMeasure.ne_zero μ⟩

Premises used: NeZero.mk, MeasureTheory.IsProbabilityMeasure.ne_zero
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ (ae μ).NeBot

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : MeasurableSet s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) = 1

Tactic:
(measure_add_measure_compl h).trans measure_univ

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.measure_add_measure_compl, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : MeasurableSet s
⊢ μ.real s + μ.real sᶜ = 1

Tactic:
simpa [Measure.real, ENNReal.toReal_add] using congr($(prob_add_prob_compl (μ := μ) h).toReal)

Premises used: ENNReal.toReal_add, MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsFiniteMeasure μ
inst_2 : NeZero μ
⊢ IsProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
⟨ENNReal.inv_mul_cancel (NeZero.ne (μ univ)) (measure_ne_top _ _)⟩

Premises used: Set.univ, MeasureTheory.measure_ne_top, MeasureTheory.IsProbabilityMeasure.mk, ENNReal.inv_mul_cancel, DFunLike.coe, NeZero.ne
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst_2 : ∀ (h : p), IsProbabilityMeasure (μ h)
inst_3 : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
isTrue : ∀ (h : p), IsProbabilityMeasure (μ h)
isFalse : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
⊢ IsProbabilityMeasure (dite p μ ν)

Tactic:
split
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst_2 : ∀ (h : p), IsProbabilityMeasure (μ h)
inst_3 : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h : p
⊢ IsProbabilityMeasure (μ h)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ : p → Measure α
ν : ¬p → Measure α
inst_2 : ∀ (h : p), IsProbabilityMeasure (μ h)
inst_3 : ∀ (h : ¬p), IsProbabilityMeasure (ν h)
h : ¬p
⊢ IsProbabilityMeasure (ν h)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ ν : Measure α
inst_2 : IsProbabilityMeasure μ
inst_3 : IsProbabilityMeasure ν
isTrue : p → IsProbabilityMeasure μ
isFalse : ¬p → IsProbabilityMeasure ν
⊢ IsProbabilityMeasure (if p then μ else ν)

Tactic:
split
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ ν : Measure α
inst_2 : IsProbabilityMeasure μ
inst_3 : IsProbabilityMeasure ν
h : p
⊢ IsProbabilityMeasure μ

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
p : Prop
inst_1 : Decidable p
μ ν : Measure α
inst_2 : IsProbabilityMeasure μ
inst_3 : IsProbabilityMeasure ν
h : ¬p
⊢ IsProbabilityMeasure ν

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 : Measure α
s : Set α
μ ν : Measure α
inst_1 : IsProbabilityMeasure μ
inst_2 : IsProbabilityMeasure ν
p : (↑I : Type)
⊢ Eq (α := ℝ≥0∞) ((toNNReal p • μ + toNNReal (σ p) • ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [← ENNReal.coe_add]

Premises used: ENNReal.coe_add
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
⊢ μ.real univ = 1

Tactic:
simp [Measure.real]

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsProbabilityMeasure μ ↔ μ.real univ = 1

Tactic:
⟨fun h ↦ probReal_univ, fun h ↦ ⟨(ENNReal.toReal_eq_one_iff (μ univ)).mp h⟩⟩

Premises used: Set.univ, MeasureTheory.probReal_univ, Iff.intro, Iff.mp, MeasureTheory.IsProbabilityMeasure.mk, DFunLike.coe, ENNReal.toReal_eq_one_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
⊢ IsProbabilityMeasure μ ↔ μ.real univ = 1

Tactic:
refine ⟨fun h ↦ probReal_univ, fun h ↦ ⟨(ENNReal.toReal_eq_one_iff (μ univ)).mp h⟩⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : α → β
hf : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [map_apply_of_aemeasurable, hf]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
inst_1 : IsProbabilityMeasure (m0 := inst) (map f μ)
⊢ AEMeasurable f μ

Tactic:
have hf : AEMeasurable f μ := AEMeasurable.of_map_ne_zero (IsProbabilityMeasure.ne_zero _)
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
f : α → β
inst_1 : IsProbabilityMeasure (m0 := inst) (map f μ)
hf : AEMeasurable f μ
rw : Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [← Set.preimage_univ (f := f), ← map_apply_of_aemeasurable hf .univ]

Premises used: MeasureTheory.Measure.map_apply_of_aemeasurable, Set.preimage_univ, MeasurableSet.univ