awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ∀ (a : μ ⟂ₘ ν), Disjoint μ ν

Tactic:
tfae_have 1 → 2
  | h => h.disjoint
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
⊢ Disjoint μ ν

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
⊢ μ ⟂ₘ ν

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
⊢ ∀ (a : Disjoint μ ν), μ ⟂ₘ ν

Tactic:
2 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
⊢ ∀ (a : Disjoint μ ν), μ ⟂ₘ ν

Tactic:
tfae_have 2 → 1
  | h => mutuallySingular_of_disjoint h
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
⊢ μ ⟂ₘ ν

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
⊢ Disjoint (ae μ) (ae ν)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
⊢ ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)

Tactic:
1 → 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
⊢ ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)

Tactic:
tfae_have 1 → 3
  | h => h.disjoint_ae
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
⊢ Disjoint (ae μ) (ae ν)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
⊢ Disjoint μ ν

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
⊢ ∀ (a : Disjoint (ae μ) (ae ν)), Disjoint μ ν

Tactic:
3 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
⊢ ∀ (a : Disjoint (ae μ) (ae ν)), Disjoint μ ν

Tactic:
tfae_have 3 → 2
  | h => disjoint_of_disjoint_ae h
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
tfae_1_to_2 : ∀ (a : μ ⟂ₘ ν), Disjoint μ ν
tfae_2_to_1 : ∀ (a : Disjoint μ ν), μ ⟂ₘ ν
tfae_1_to_3 : ∀ (a : μ ⟂ₘ ν), Disjoint (ae μ) (ae ν)
tfae_3_to_2 : ∀ (a : Disjoint (ae μ) (ae ν)), Disjoint μ ν
⊢ [μ ⟂ₘ ν, Disjoint μ ν, Disjoint (ae μ) (ae ν)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ μ ⟂ₘ ν ↔ Disjoint μ ν

Tactic:
mutuallySingular_tfae.out 0 1

Premises used: MeasureTheory.Measure.mutuallySingular_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MutuallySingular
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ μ ⟂ₘ ν ↔ Disjoint (ae μ) (ae ν)

Tactic:
mutuallySingular_tfae.out 0 2

Premises used: MeasureTheory.Measure.mutuallySingular_tfae, List.TFAE.out, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : Subsingleton α
⊢ Subsingleton.{u_2 + 1} (NullMeasurableSpace α μ)

Tactic:
h

Premises used: MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : MeasurableSet s
⊢ NullMeasurableSet s μ

Tactic:
h.eventuallyMeasurableSet

Premises used: MeasureTheory.NullMeasurableSet, MeasurableSet.eventuallyMeasurableSet, EventuallyMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
⊢ NullMeasurableSet ∅ μ

Tactic:
MeasurableSet.empty

Premises used: MeasurableSet.empty, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
⊢ NullMeasurableSet univ μ

Tactic:
MeasurableSet.univ

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet s μ

Tactic:
⟨∅, MeasurableSet.empty, ae_eq_empty.2 h⟩

Premises used: Iff.mpr, MeasurableSet, MeasurableSet.empty, MeasureTheory.NullMeasurableSet, MeasureTheory.ae_eq_empty, And.intro, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ NullMeasurableSet sᶜ μ

Tactic:
MeasurableSet.compl h

Premises used: Set.Mem, setOf, MeasureTheory.NullMeasurableSet, MeasurableSet.compl, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet sᶜ μ
⊢ NullMeasurableSet s μ

Tactic:
MeasurableSet.of_compl h

Premises used: MeasurableSet.of_compl, MeasureTheory.NullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ NullMeasurableSet sᶜ μ ↔ NullMeasurableSet s μ

Tactic:
MeasurableSet.compl_iff

Premises used: Set.Mem, MeasurableSet.compl_iff, setOf, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : Subsingleton α
⊢ NullMeasurableSet s μ

Tactic:
Subsingleton.measurableSet

Premises used: Subsingleton.measurableSet, MeasureTheory.NullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h : s =ᶠ[ae μ] t
⊢ NullMeasurableSet t μ

Tactic:
EventuallyMeasurableSet.congr hs h.symm

Premises used: MeasureTheory.NullMeasurableSet, EventuallyMeasurableSet, MeasureTheory.NullMeasurableSpace, EventuallyMeasurableSet.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
ι : Sort u_5
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
⊢ NullMeasurableSet (⋃ (i : ι), s i) μ

Tactic:
MeasurableSet.iUnion h

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : ι → Set α
s : Set ι
hs : s.Countable
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ NullMeasurableSet (⋃ b ∈ s, f b) μ

Tactic:
MeasurableSet.biUnion hs h

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
rw : NullMeasurableSet (⋃ i ∈ s, i) μ
⊢ NullMeasurableSet (⋃₀ s) μ

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ

Tactic:
MeasurableSet.biUnion hs h

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋃ i ∈ s, i) μ

Tactic:
exact MeasurableSet.biUnion hs h

Premises used: MeasurableSet.biUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
ι : Sort u_5
inst : Countable ι
f : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (f i) μ
⊢ NullMeasurableSet (⋂ (i : ι), f i) μ

Tactic:
MeasurableSet.iInter h

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.iInter
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
μ : Measure α
f : β → Set α
s : Set β
hs : s.Countable
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ NullMeasurableSet (⋂ b ∈ s, f b) μ

Tactic:
MeasurableSet.biInter hs h

Premises used: MeasureTheory.NullMeasurableSet, MeasurableSet.biInter, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Countable
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋂₀ s) μ

Tactic:
MeasurableSet.sInter hs h

Premises used: MeasurableSet.sInter, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ NullMeasurableSet (s ∪ t) μ

Tactic:
MeasurableSet.union hs ht

Premises used: MeasureTheory.NullMeasurableSet, MeasurableSet.union, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ NullMeasurableSet (s ∪ t) μ

Tactic:
hs.union (of_null ht)

Premises used: MeasureTheory.NullMeasurableSet.of_null, MeasureTheory.NullMeasurableSet.union
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ NullMeasurableSet (s ∩ t) μ

Tactic:
MeasurableSet.inter hs ht

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
⊢ NullMeasurableSet (s \ t) μ

Tactic:
MeasurableSet.diff hs ht

Premises used: MeasurableSet.diff, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : NullMeasurableSet s₁ μ
h₂ : NullMeasurableSet s₂ μ
⊢ NullMeasurableSet (symmDiff s₁ s₂) μ

Tactic:
(h₁.diff h₂).union (h₂.diff h₁)

Premises used: MeasureTheory.NullMeasurableSet.union, MeasureTheory.NullMeasurableSet.diff, symmDiff
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : ℕ → Set α
h : ∀ (i : ℕ), NullMeasurableSet (f i) μ
n : ℕ
⊢ NullMeasurableSet (disjointed f n) μ

Tactic:
MeasurableSet.disjointed h n

Premises used: MeasureTheory.NullMeasurableSet, MeasurableSet.disjointed, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
p : Prop
⊢ NullMeasurableSet {_a : α | p} μ

Tactic:
MeasurableSet.const p

Premises used: setOf, MeasureTheory.NullMeasurableSet, MeasurableSet.const, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
inst : MeasurableSingletonClass α
⊢ MeasurableSingletonClass.{u_2} (NullMeasurableSpace α μ)

Tactic:
eventuallyMeasurableSingleton (m := m0)

Premises used: eventuallyMeasurableSingleton, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst : MeasurableSingletonClass.{u_2} (NullMeasurableSpace α μ)
hs : NullMeasurableSet s μ
a : α
⊢ NullMeasurableSet (insert a s) μ

Tactic:
MeasurableSet.insert hs a

Premises used: MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace, MeasurableSet.insert
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
rcases : ∀ (t : Set α) (htm : MeasurableSet t) (hst : s =ᶠ[ae μ] t), ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
rcases h with ⟨t, htm, hst⟩
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩

Premises used: SDiff.sdiff, MeasureTheory.measurableSet_toMeasurable, And.intro, MeasurableSet.union, Exists.intro, MeasureTheory.toMeasurable, Union.union
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
refine_1 : t ∪ toMeasurable μ (s \ t) ⊇ s
refine_2 : t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s
⊢ ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
refine ⟨t ∪ toMeasurable μ (s \ t), ?_, htm.union (measurableSet_toMeasurable _ _), ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

Tactic:
diff_subset_iff.1 (subset_toMeasurable _ _)

Premises used: Set.diff_subset_iff, MeasureTheory.subset_toMeasurable, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ t ∪ toMeasurable μ (s \ t) ⊇ s

Tactic:
exact diff_subset_iff.1 (subset_toMeasurable _ _)

Premises used: Set.diff_subset_iff, MeasureTheory.subset_toMeasurable, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ toMeasurable μ (s \ t) =ᶠ[ae μ] ∅

Tactic:
simp [ae_le_set.1 hst.le]

Premises used: Filter.EventuallyEq.le, Iff.mp, MeasureTheory.ae_le_set
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
⊢ toMeasurable μ (s \ t) =ᶠ[ae μ] ∅

Tactic:
have : toMeasurable μ (s \ t) =ᵐ[μ] (∅ : Set α) := by simp [ae_le_set.1 hst.le]
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
htm : MeasurableSet t
hst : s =ᶠ[ae μ] t
this : toMeasurable μ (s \ t) =ᶠ[ae μ] ∅
⊢ t ∪ toMeasurable μ (s \ t) =ᶠ[ae μ] s

Tactic:
simpa only [union_empty] using hst.symm.union this

Premises used: Set.union_empty, Filter.EventuallyEq.union, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
rw : ⋯.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s) =ᶠ[ae μ] s
hc : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s
⊢ toMeasurable μ s =ᶠ[ae μ] s

Tactic:
rw [toMeasurable_def, dif_pos]

Premises used: dif_pos, MeasureTheory.toMeasurable_def
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ⋯.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s) =ᶠ[ae μ] s

Tactic:
(exists_measurable_superset_ae_eq h).choose_spec.2.2

Premises used: Exists.choose_spec, And.right, MeasureTheory.NullMeasurableSet.exists_measurable_superset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ (toMeasurable μ sᶜ)ᶜ =ᶠ[ae μ] s

Tactic:
Iff.mpr ae_eq_set_compl <| toMeasurable_ae_eq h.compl

Premises used: Iff.mpr, MeasureTheory.ae_eq_set_compl, MeasureTheory.NullMeasurableSet.compl, MeasureTheory.NullMeasurableSet.toMeasurable_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
h : NullMeasurableSet s μ
⊢ ∃ t ⊆ s, MeasurableSet t ∧ t =ᶠ[ae μ] s

Tactic:
⟨(toMeasurable μ sᶜ)ᶜ, compl_subset_comm.2 <| subset_toMeasurable _ _,
    (measurableSet_toMeasurable _ _).compl, compl_toMeasurable_compl_ae_eq h⟩

Premises used: Iff.mpr, MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq, Compl.compl, Set.compl_subset_comm, MeasureTheory.subset_toMeasurable, MeasurableSet.compl, MeasureTheory.measurableSet_toMeasurable, And.intro, Exists.intro, MeasureTheory.toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
choose :
  ∀ (t : (i : ι) → Set α) (ht_sub : ∀ (i : ι), t i ⊆ s i) (htm : ∀ (i : ι), MeasurableSet (t i))
    (ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i),
    ∃ (t : ι → Set α),
      (∀ (i : ι), t i ⊆ s i) ∧
        (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
choose t ht_sub htm ht_eq using fun i => exists_measurable_subset_ae_eq (h i)

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : (i : ι) → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
rcases :
  ∀ (u : ι → Set α) (hum : ∀ (i : ι), MeasurableSet (u i))
    (hu₀ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u i) : ℝ≥0∞) (0 : ℝ≥0∞))
    (hud :
      Pairwise.{u_1} (α := ι) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ u i)),
    ∃ (t : ι → Set α),
      (∀ (i : ι), t i ⊆ s i) ∧
        (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
rcases exists_null_pairwise_disjoint_diff hd with ⟨u, hum, hu₀, hud⟩

Premises used: MeasureTheory.exists_null_pairwise_disjoint_diff
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : (i : ι) → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u i) : ℝ≥0∞) (0 : ℝ≥0∞)
hud : Pairwise.{u_1} (α := ι) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ u i)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
⟨fun i => t i \ u i, fun i => diff_subset.trans (ht_sub _), fun i =>
      (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
      hud.mono fun i j h =>
        h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩

Premises used: MeasurableSet.diff, Set.diff_subset, Filter.EventuallyEq.trans, MeasureTheory.diff_null_ae_eq_self, HasSubset.Subset.trans, Set.diff_subset_diff_left, SDiff.sdiff, And.intro, Exists.intro, Disjoint.mono, Filter.EventuallyEq.symm, Pairwise.mono
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
s : ι → Set α
h : ∀ (i : ι), NullMeasurableSet (s i) μ
hd : Pairwise (AEDisjoint μ on s)
t : (i : ι) → Set α
ht_sub : ∀ (i : ι), t i ⊆ s i
htm : ∀ (i : ι), MeasurableSet (t i)
ht_eq : ∀ (i : ι), t i =ᶠ[ae μ] s i
u : ι → Set α
hum : ∀ (i : ι), MeasurableSet (u i)
hu₀ : ∀ (i : ι), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u i) : ℝ≥0∞) (0 : ℝ≥0∞)
hud : Pairwise.{u_1} (α := ι) (Function.onFun.{u_1 + 1, u_2 + 1, 1} (β := Set α) Disjoint fun (i : ι) ↦ s i \ u i)
⊢ ∃ (t : ι → Set α),
    (∀ (i : ι), t i ⊆ s i) ∧ (∀ (i : ι), s i =ᶠ[ae μ] t i) ∧ (∀ (i : ι), MeasurableSet (t i)) ∧ Pairwise (Disjoint on t)

Tactic:
exact
    ⟨fun i => t i \ u i, fun i => diff_subset.trans (ht_sub _), fun i =>
      (ht_eq _).symm.trans (diff_null_ae_eq_self (hu₀ i)).symm, fun i => (htm i).diff (hum i),
      hud.mono fun i j h =>
        h.mono (diff_subset_diff_left (ht_sub i)) (diff_subset_diff_left (ht_sub j))⟩
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : ι), MeasurableSet (f i)
rw :
  Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      extend (P := MeasurableSet) (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) (f i))
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))
rw₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ :
  ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑' (i : ℕ), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
rw [measure_eq_extend (MeasurableSet.iUnion h),
    extend_iUnion MeasurableSet.empty _ MeasurableSet.iUnion _ hn h]

Premises used: MeasurableSet.empty, MeasureTheory.extend_iUnion, MeasurableSet.iUnion, MeasureTheory.measure_eq_extend