awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 μ
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
IsProbabilityMeasure.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 β
μ : Measure α
f : α → β
inst_1 : IsProbabilityMeasure (m0 := inst) (map f μ)
hf : AEMeasurable f μ
⊢ Eq (α := ℝ≥0∞) (((map f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
exact IsProbabilityMeasure.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 β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ IsProbabilityMeasure (m0 := inst) (map f μ) ↔ IsProbabilityMeasure μ

Tactic:
⟨fun _ ↦ isProbabilityMeasure_of_map f, fun _ ↦ isProbabilityMeasure_map hf⟩

Premises used: Iff.intro, MeasureTheory.Measure.isProbabilityMeasure_of_map, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : β ≃ᵐ α
rw : IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.map (⇑f.symm : (a : α) → β) μ)
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.comap (⇑f : (a : β) → α) μ)

Tactic:
rw [← MeasurableEquiv.map_symm]

Premises used: MeasurableEquiv.map_symm
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.map (⇑f.symm : (a : α) → β) μ)

Tactic:
isProbabilityMeasure_map f.symm.measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasurableEquiv.symm, MeasurableEquiv.measurable, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : β ≃ᵐ α
⊢ IsProbabilityMeasure.{u_2} (α := β) (m0 := inst) (Measure.map (⇑f.symm : (a : α) → β) μ)

Tactic:
exact isProbabilityMeasure_map f.symm.measurable.aemeasurable

Premises used: Measurable.aemeasurable, MeasurableEquiv.symm, MeasurableEquiv.measurable, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ rw₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [measure_compl₀ h (measure_ne_top _ _), measure_univ]

Premises used: MeasureTheory.measure_ne_top, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.measure_compl₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ = HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
prob_compl_eq_one_sub₀ hs.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.prob_compl_eq_one_sub₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
rw :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) = 0 ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
rw₁ :
  LE.le (α := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [prob_compl_eq_one_sub₀ hs, tsub_eq_zero_iff_le, one_le_prob_iff]

Premises used: MeasureTheory.prob_compl_eq_one_sub₀, tsub_eq_zero_iff_le, MeasureTheory.one_le_prob_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
rw :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (1 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← prob_compl_eq_zero_iff₀ hs.compl, compl_compl]

Premises used: compl_compl, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.prob_compl_eq_zero_iff₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (1 : ℝ≥0∞) ↔
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : NullMeasurableSet s μ
⊢ s ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
mem_ae_iff.trans <| prob_compl_eq_zero_iff₀ hs

Premises used: Iff.trans, MeasureTheory.mem_ae_iff, MeasureTheory.prob_compl_eq_zero_iff₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ s ∈ ae μ ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
mem_ae_iff.trans <| prob_compl_eq_zero_iff hs

Premises used: MeasureTheory.prob_compl_eq_zero_iff, Iff.trans, MeasureTheory.mem_ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsProbabilityMeasure μ
p : α → Prop
hp : Measurable p
⊢ (∀ᵐ (a : α) ∂μ, p a) ↔ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | p a} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
mem_ae_iff_prob_eq_one hp.setOf

Premises used: Filter.Eventually, setOf, Measurable.setOf, MeasureTheory.mem_ae_iff_prob_eq_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
rw : f '' univ ∈ ae μ
⊢ Eq (α := ℝ≥0∞) (((Measure.comap f μ : Measure β) : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [comap_apply _ hf hf'' _ MeasurableSet.univ,
      ← mem_ae_iff_prob_eq_one (hf'' _ MeasurableSet.univ)]

Premises used: MeasureTheory.Measure.comap_apply, MeasureTheory.mem_ae_iff_prob_eq_one, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : β → α
hf : Injective f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
hf'' : ∀ (s : Set β), MeasurableSet s → MeasurableSet (f '' s)
⊢ f '' univ ∈ ae μ

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
inst_1 : IsProbabilityMeasure μ
f : β → α
hf : MeasurableEmbedding f
hf' : ∀ᵐ (a : α) ∂μ, a ∈ range f
⊢ IsProbabilityMeasure (m0 := inst) (Measure.comap f μ)

Tactic:
isProbabilityMeasure_comap hf.injective hf' hf.measurableSet_image'

Premises used: MeasureTheory.isProbabilityMeasure_comap, MeasurableEmbedding.measurableSet_image', MeasurableEmbedding.injective
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f : β → α
⊢ IsProbabilityMeasure (m0 := ULift.instMeasurableSpace) (Measure.map ULift.up μ)

Tactic:
isProbabilityMeasure_map measurable_up.aemeasurable

Premises used: Measurable.aemeasurable, measurable_up, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsProbabilityMeasure μ
p : α → Prop
f : β → α
⊢ ∀ (a : α),
    Membership.mem (γ := Set α)
      (range (ι := ULift.{u_3, u_1} α) (⇑MeasurableEquiv.ulift : (a : ULift.{u_3, u_1} α) → α)) a

Tactic:
simp [Function.Surjective.range_eq <| EquivLike.surjective _]

Premises used: Function.Surjective.range_eq, EquivLike.surjective
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : IsProbabilityMeasure μ
inst_1 : IsProbabilityMeasure ν
hμν : μ ≤ ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inl :
  IsZeroOrProbabilityMeasure
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)
inr :
  ∀ (h : NeZero μ), IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
rcases eq_zero_or_neZero μ with rfl | h

Premises used: eq_zero_or_neZero, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
⊢ IsZeroOrProbabilityMeasure
    (HSMul.hSMul (α := ℝ≥0∞) (β := Measure α) ((((0 : Measure α) : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) 0)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
s : Set α
⊢ IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h : NeZero μ
inr :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
inr₁ :
  ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)),
    IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
rcases eq_top_or_lt_top (μ univ) with h | h

Premises used: Set.univ, DFunLike.coe, eq_top_or_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h_1 : NeZero μ
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
inr : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

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

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h_1 : NeZero μ
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IsFiniteMeasure μ

Tactic:
have : IsFiniteMeasure μ := ⟨h⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
h_1 : NeZero μ
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
this : IsFiniteMeasure μ
⊢ IsZeroOrProbabilityMeasure (HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ)

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)), μ = 0 ∨ IsProbabilityMeasure μ
inr : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (1 : ℝ≥0∞)), μ = 0 ∨ IsProbabilityMeasure μ
⊢ μ = 0 ∨ IsProbabilityMeasure μ

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 μ
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ = 0 ∨ IsProbabilityMeasure μ

Tactic:
apply Or.inl (measure_univ_eq_zero.mp h)

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

Tactic:
Or.inr ⟨h⟩

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

Tactic:
exact Or.inr ⟨h⟩

Premises used: Or.inr
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsZeroOrProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : α → β
pos : ∀ (hf : AEMeasurable f μ), IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
neg : ∀ (hf : ¬AEMeasurable f μ), IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)
⊢ IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)

Tactic:
by_cases hf : AEMeasurable f μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsZeroOrProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : α → β
hf : AEMeasurable f μ
⊢ IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)

Tactic:
simpa [isZeroOrProbabilityMeasure_iff, hf] using IsZeroOrProbabilityMeasure.measure_univ

Premises used: MeasureTheory.IsZeroOrProbabilityMeasure.measure_univ, MeasureTheory.isZeroOrProbabilityMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ : Measure α
s : Set α
inst_1 : IsZeroOrProbabilityMeasure μ
p : α → Prop
f_1 : β → α
f : α → β
hf : ¬AEMeasurable f μ
⊢ IsZeroOrProbabilityMeasure (m0 := inst) (Measure.map f μ)

Tactic:
simp [isZeroOrProbabilityMeasure_iff, hf]

Premises used: MeasureTheory.isZeroOrProbabilityMeasure_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
inl :
  ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p < ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
    ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
inr : ∀ (h : IsProbabilityMeasure μ), (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
hμs : p < ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p

Tactic:
simp at hμs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
inr : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < 1 - p
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ < 1 - p

Tactic:
rw [prob_compl_eq_one_sub s_mble]

Premises used: MeasureTheory.prob_compl_eq_one_sub
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
inr : 1 - (1 - p) < (μ : (a : Set α) → ℝ≥0∞) s
⊢ HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) < 1 - p

Tactic:
apply ENNReal.sub_lt_of_sub_lt prob_le_one (Or.inl one_ne_top)

Premises used: ENNReal.sub_lt_of_sub_lt, MeasureTheory.prob_le_one, Or.inl, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ p < (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
hμs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
h₁ : 1 - (1 - p) = p
⊢ 1 - (1 - p) < (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
convert! hμs
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) = p

Tactic:
ENNReal.sub_sub_cancel one_ne_top (lt_of_lt_of_le hμs prob_le_one).le

Premises used: MeasureTheory.prob_le_one, LT.lt.le, ENNReal.sub_sub_cancel, lt_of_lt_of_le, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p < (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ 1 - (1 - p) = p

Tactic:
exact ENNReal.sub_sub_cancel one_ne_top (lt_of_lt_of_le hμs prob_le_one).le

Premises used: MeasureTheory.prob_le_one, LT.lt.le, ENNReal.sub_sub_cancel, lt_of_lt_of_le, ENNReal.one_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
inl :
  ∀ [IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0] (hμs : p ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s),
    ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
inr : ∀ (h : IsProbabilityMeasure μ), (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with rfl | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
p : ℝ≥0∞
s_mble : MeasurableSet s
inst : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := m0) 0
hμs : p ≤ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) s
⊢ ((0 : Measure α) : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsZeroOrProbabilityMeasure μ
p : ℝ≥0∞
hμs : p ≤ (μ : (a : Set α) → ℝ≥0∞) s
s_mble : MeasurableSet s
h : IsProbabilityMeasure μ
⊢ (μ : (a : Set α) → ℝ≥0∞) sᶜ ≤ 1 - p

Tactic:
simpa [prob_compl_eq_one_sub s_mble] using tsub_le_tsub_left hμs 1

Premises used: tsub_le_tsub_left, MeasureTheory.prob_compl_eq_one_sub, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
inl : ∀ (h : μ = 0), HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
inr : ∀ (h : IsProbabilityMeasure μ), HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ

Tactic:
rcases eq_zero_or_isProbabilityMeasure μ with h | h

Premises used: MeasureTheory.eq_zero_or_isProbabilityMeasure
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
h : μ = 0
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.Probability
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : IsZeroOrProbabilityMeasure μ
h : IsProbabilityMeasure μ
⊢ HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) univ)⁻¹ : ℝ≥0∞) μ = μ

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s t : Set α
a : α
h : SFinite μ
n : ℕ
⊢ IsFiniteMeasure (sfiniteSeq μ n)

Tactic:
h.1.choose_spec.1 n

Premises used: Exists.choose_spec, And.left, MeasureTheory.SFinite.out', MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
h : SFinite μ
⊢ sum (sfiniteSeq μ) = μ

Tactic:
h.1.choose_spec.2.symm

Premises used: Exists.choose_spec, And.right, Eq.symm, MeasureTheory.SFinite.out', MeasureTheory.sfiniteSeq
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SFinite μ
n : ℕ
⊢ sfiniteSeq μ n ≤ μ

Tactic:
(le_sum _ n).trans (sum_sfiniteSeq μ).le

Premises used: Eq.le, MeasureTheory.sum_sfiniteSeq, MeasureTheory.Measure.le_sum, LE.le.trans