awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x

Tactic:
have : ∀ n, ∀ᵐ x ∂μ, x ∈ spanningSets (μ + ν) n → P x := by
    intro n
    have := h
      (spanningSets (μ + ν) n) (measurableSet_spanningSets _ _)
      ((self_le_add_right _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
      ((self_le_add_left _ _).trans_lt (measure_spanningSets_lt_top (μ + ν) _))
    exact (ae_restrict_iff' (measurableSet_spanningSets _ _)).mp this
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
a : α
hx : ∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a
⊢ P a

Tactic:
hx _ (mem_spanningSetsIndex _ _)

Premises used: MeasureTheory.mem_spanningSetsIndex
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, x ∈ spanningSets (μ + ν) n → P x
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ P x) x} x}
      a
h₂ h₃ : ∀ (a : α) (hx : ∀ (i : ℕ), a ∈ spanningSets (μ + ν) i → P a), P a
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
filter_upwards [ae_all_iff.2 this] with _ hx using hx _ (mem_spanningSetsIndex _ _)

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
P : α → Prop
h :
  ∀ (s : Set α),
    MeasurableSet s → LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) → ∀ᵐ (x : α) ∂μ.restrict s, P x
⊢ ∀ᵐ (x : α) ∂μ, P x

Tactic:
ae_of_forall_measure_lt_top_ae_restrict' μ P fun s hs h2s _ => h s hs h2s

Premises used: MeasureTheory.ae_of_forall_measure_lt_top_ae_restrict'
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ_1 ν : Measure α
s t : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SigmaCompactSpace α
μ : Measure α
inst_3 : IsFiniteMeasureOnCompacts μ
⊢ SigmaFinite μ

Tactic:
⟨⟨{   set := compactCovering α
        set_mem := fun _ => trivial
        finite := fun n => (isCompact_compactCovering α n).measure_lt_top
        spanning := iUnion_compactCovering α }⟩⟩

Premises used: compactCovering, trivial, iUnion_compactCovering, MeasureTheory.Measure.FiniteSpanningSetsIn.mk, isCompact_compactCovering, Nonempty.intro, IsCompact.measure_lt_top, MeasureTheory.SigmaFinite.mk
-- 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 : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
choose :
  ∀ (s : (x : α) → Set α) (hsx : ∀ (x : α), s x ∈ 𝓝 x)
    (hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)), SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
choose s hsx hsμ using μ.finiteAt_nhds

Premises used: MeasureTheory.Measure.finiteAt_nhds
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
rcases : ∀ (t : Set α) (htc : t.Countable) (htU : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ t, s x) univ), SigmaFinite μ
⊢ SigmaFinite μ

Tactic:
rcases TopologicalSpace.countable_cover_nhds hsx with ⟨t, htc, htU⟩

Premises used: TopologicalSpace.countable_cover_nhds
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t_1 : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ t, s x) univ
⊢ SigmaFinite μ

Tactic:
Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_

Premises used: Iff.mpr, Set.Countable.image, MeasureTheory.Measure.sigmaFinite_of_countable, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t_1 : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
htc : t.Countable
htU : Eq.{u_1 + 1} (α := Set α) (⋃ x ∈ t, s x) univ
refine : ⋃₀ (s '' t) = univ
⊢ SigmaFinite μ

Tactic:
refine Measure.sigmaFinite_of_countable (htc.image s) (forall_mem_image.2 fun x _ => hsμ x) ?_

Premises used: Iff.mpr, Set.Countable.image, MeasureTheory.Measure.sigmaFinite_of_countable, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSpace β
μ ν : Measure α
s_1 t_1 : Set α
a : α
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : IsLocallyFiniteMeasure μ
s : (x : α) → Set α
hsx : ∀ (x : α), s x ∈ 𝓝 x
hsμ : ∀ (x : α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s x) : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
htc : t.Countable
htU rwa rwa₁ rwa₂ rwa₃ : Eq.{u_1 + 1} (α := Set α) (⋃ a ∈ t, s a) univ
⊢ ⋃₀ (s '' t) = univ

Tactic:
rwa [sUnion_image]

Premises used: Set.sUnion_image
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}
⊢ S.disjointed.set (C := {s : Set α | MeasurableSet s}) = disjointed (S.set (C := {s : Set α | MeasurableSet s}))

Tactic:
rfl

Premises used: disjointed, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
⊢ ∃ (S : μ.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}) (T :
    ν.FiniteSpanningSetsIn {s : Set α | MeasurableSet s}),
    S.set (C := {s : Set α | MeasurableSet s}) = T.set (C := {s : Set α | MeasurableSet s}) ∧
      Pairwise (Disjoint on S.set (C := {s : Set α | MeasurableSet s}))

Tactic:
let S := (μ + ν).toFiniteSpanningSetsIn.disjointed
  ⟨S.ofLE (Measure.le_add_right le_rfl), S.ofLE (Measure.le_add_left le_rfl), rfl,
    disjoint_disjointed _⟩

Premises used: MeasureTheory.Measure.FiniteSpanningSetsIn.ofLE, le_rfl, MeasureTheory.Measure.FiniteSpanningSetsIn.set, HAdd.hAdd, And.intro, Exists.intro, MeasureTheory.Measure.toFiniteSpanningSetsIn, MeasureTheory.Measure.le_add_right, MeasureTheory.Measure.le_add_left, disjoint_disjointed, MeasureTheory.Measure.FiniteSpanningSetsIn.disjointed, rfl
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
pos :
  ∀ (hs : MeasurableSet s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
neg :
  ∀ (hs : ¬MeasurableSet s),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
      Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
by_cases hs : MeasurableSet s

Premises used: MeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
IsZeroOneMeasure.zero_one₀ hs

Premises used: MeasureTheory.IsZeroOneMeasure.zero_one₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
exact IsZeroOneMeasure.zero_one₀ hs

Premises used: MeasureTheory.IsZeroOneMeasure.zero_one₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
neg :
  ∀ (t : Set α),
    s ⊆ t →
      ∀ (mt : MeasurableSet t)
        (ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)),
        Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
          Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
obtain ⟨t, _, mt, ht⟩ := exists_measurable_superset μ s

Premises used: mt, MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
neg :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
rw [← ht]
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)

Tactic:
IsZeroOneMeasure.zero_one₀ mt

Premises used: MeasureTheory.IsZeroOneMeasure.zero_one₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hs : ¬MeasurableSet s
t : Set α
left : s ⊆ t
mt : MeasurableSet t
ht : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) ∨
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)

Tactic:
exact IsZeroOneMeasure.zero_one₀ mt

Premises used: MeasureTheory.IsZeroOneMeasure.zero_one₀
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
mp :
  (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
mpr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal) →
    ∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ (∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)) ↔
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
mp :
  ∀ (h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
mp₁ :
  ∀ (h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
rcases μ.zero_one univ with (h₀ | h₁)

Premises used: Set.univ, MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)

Tactic:
have := measure_mono (μ := μ) <| subset_univ s
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)
⊢ LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)

Tactic:
rw [h] at this
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₀ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (0 : ENNReal)
this : LE.le (α := ENNReal) (1 : ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
h₁
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
h₁ : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
exact h₁
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ ∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
⟨univ, h⟩

Premises used: Set.univ, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)
⊢ ∃ (s : Set α), Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
exact ⟨univ, h⟩
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s : Set α
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) univ : ENNReal) (1 : ENNReal)

Tactic:
(exists_measure_eq_one_iff_measure_univ_eq_one).mp ⟨s, hμs⟩

Premises used: MeasureTheory.IsZeroOneMeasure.exists_measure_eq_one_iff_measure_univ_eq_one, Exists.intro, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)

Tactic:
have : μ (s ∩ t) ≤ μ s := measure_mono inter_subset_left
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
⊢ LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)

Tactic:
have : μ (s ∩ t) ≤ μ t := measure_mono inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
inr :
  ∀ (hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)

Tactic:
rcases μ.zero_one s with (_ | hμs)

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
inl₁ :
  ∀ (hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)

Tactic:
rcases μ.zero_one t with (_ | hμt)

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
inr :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
inr₁ :
  ∀ (hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)),
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)

Tactic:
rcases μ.zero_one t with (_ | hμt)

Premises used: MeasureTheory.Measure.zero_one
-- Module: Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsZeroOneMeasure μ
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
hμs : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (1 : ENNReal)
hμt : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (1 : ENNReal)
this_1 : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal)
this : LE.le (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal)
h : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) s : ENNReal) (0 : ENNReal)
h_1 : Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) t : ENNReal) (0 : ENNReal)
inl :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (0 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
inl₁ :
  Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal) →
    Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (s ∩ t) : ENNReal) (1 : ENNReal)

Tactic:
rcases μ.zero_one (s ∩ t)

Premises used: Inter.inter, MeasureTheory.Measure.zero_one