awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
⊢ Eq (α := ℝ≥0∞)
    (∑' (i : ι),
      extend (P := MeasurableSet) (fun (t : Set α) (_ht : MeasurableSet t) ↦ (μ : (a : Set α) → ℝ≥0∞) t) (f i))
    (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
simp [measure_eq_extend, h]

Premises used: MeasureTheory.measure_eq_extend
-- 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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
μ.empty

Premises used: MeasureTheory.OuterMeasure.empty, MeasureTheory.Measure.toOuterMeasure
-- 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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact μ.empty

Premises used: MeasureTheory.OuterMeasure.empty, MeasureTheory.Measure.toOuterMeasure
-- 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)
⊢ ∀ ⦃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∞)

Tactic:
μ.m_iUnion

Premises used: MeasureTheory.Measure.m_iUnion
-- 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)
⊢ ∀ ⦃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∞)

Tactic:
exact μ.m_iUnion

Premises used: MeasureTheory.Measure.m_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
rcases :
  ∀ (t : ι → Set α) (_ht_sub : ∀ (i : ι), t i ⊆ f i) (ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i)
    (htm : ∀ (i : ι), MeasurableSet (t i)) (htd : Pairwise (Disjoint on t)),
    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:
rcases exists_subordinate_pairwise_disjoint h hd with ⟨t, _ht_sub, ht_eq, htm, htd⟩

Premises used: MeasureTheory.exists_subordinate_pairwise_disjoint
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞)

Tactic:
measure_congr (.countable_iUnion ht_eq)

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.countable_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), t i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
measure_iUnion htd htm

Premises used: MeasureTheory.measure_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ Eq (α := ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (t i)) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i))

Tactic:
tsum_congr fun i => measure_congr (ht_eq _).symm

Premises used: MeasureTheory.measure_congr, tsum_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : Countable ι
f : ι → Set α
hd : Pairwise (AEDisjoint μ on f)
h : ∀ (i : ι), NullMeasurableSet (f i) μ
t : ι → Set α
_ht_sub : ∀ (i : ι), t i ⊆ f i
ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i
htm : ∀ (i : ι), MeasurableSet (t i)
htd : Pairwise (Disjoint on t)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ι), f i) : ℝ≥0∞) (∑' (i : ι), (μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
calc
    μ (⋃ i, f i) = μ (⋃ i, t i) := measure_congr (.countable_iUnion ht_eq)
    _ = ∑' i, μ (t i) := measure_iUnion htd htm
    _ = ∑' i, μ (f i) := tsum_congr fun i => measure_congr (ht_eq _).symm

Premises used: MeasureTheory.measure_congr, tsum_congr, Filter.EventuallyEq.countable_iUnion, MeasureTheory.measure_iUnion, DFunLike.coe, Set.iUnion, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
hd₁ : Pairwise (α := Bool) (AEDisjoint μ on fun (b : Bool) ↦ bif b then s else t)
h : ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [union_eq_iUnion, measure_iUnion₀, tsum_fintype, Fintype.sum_bool, cond, cond]

Premises used: cond, MeasureTheory.measure_iUnion₀, Fintype.sum_bool, tsum_fintype, Set.union_eq_iUnion
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (α := Bool) (AEDisjoint μ on fun (b : Bool) ↦ bif b then s else t)

Tactic:
(pairwise_on_bool AEDisjoint.symmetric).2 hd

Premises used: Iff.mpr, pairwise_on_bool, MeasureTheory.AEDisjoint.symmetric
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ ∀ (i : Bool), NullMeasurableSet (bif i then s else t) μ

Tactic:
fun b => Bool.casesOn b ht hs

Premises used: Bool.casesOn
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
⊢ Pairwise (α := Bool) (AEDisjoint μ on fun (b : Bool) ↦ bif b then s else t)

Tactic:
exacts [(pairwise_on_bool AEDisjoint.symmetric).2 hd, fun b => Bool.casesOn b ht hs]

Premises used: Iff.mpr, pairwise_on_bool, MeasureTheory.AEDisjoint.symmetric
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
le_antisymm ?_ (measure_le_inter_add_diff _ _ _)

Premises used: MeasureTheory.measure_le_inter_add_diff, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
refine :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
refine le_antisymm ?_ (measure_le_inter_add_diff _ _ _)

Premises used: MeasureTheory.measure_le_inter_add_diff, le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
rcases :
  ∀ (s' : Set α) (hsub : s ⊆ s') (hs'm : MeasurableSet s')
    (hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)),
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
      (μ : (a : Set α) → ℝ≥0∞) s
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩

Premises used: MeasureTheory.exists_measurable_superset
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ NullMeasurableSet s' μ

Tactic:
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs'm : NullMeasurableSet s' μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s' ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s' \ t) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs'm : NullMeasurableSet s' μ
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s' ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s' \ t) : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s' ∩ t ∪ s' \ t)

Tactic:
(measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm

Premises used: MeasureTheory.measure_union₀_aux, MeasureTheory.NullMeasurableSet.inter, Disjoint.aedisjoint, disjoint_inf_sdiff, MeasureTheory.NullMeasurableSet.diff, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs'm : NullMeasurableSet s' μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s' ∩ t ∪ s' \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞)

Tactic:
congr_arg μ (inter_union_diff _ _)

Premises used: congr_arg, Set.inter_union_diff, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs'm : NullMeasurableSet s' μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
hs'
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s' : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs'm : NullMeasurableSet s' μ
μ₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s' ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s' \ t) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ≤
    (μ : (a : Set α) → ℝ≥0∞) s

Tactic:
calc
    μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
    _ = μ (s' ∩ t ∪ s' \ t) :=
      (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
          (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
    _ = μ s' := congr_arg μ (inter_union_diff _ _)
    _ = μ s := hs'

Premises used: MeasureTheory.measure_union₀_aux, MeasureTheory.NullMeasurableSet.inter, Inter.inter, congr_arg, SDiff.sdiff, Disjoint.aedisjoint, disjoint_inf_sdiff, Set.inter_union_diff, Union.union, MeasureTheory.NullMeasurableSet.diff, Eq.symm, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
ht : NullMeasurableSet t μ
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
hfin : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
rw₁ :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
rw₂ :
  (μ : (a : Set α) → ℝ≥0∞) s =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)
rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₄ rw₅ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞)

Tactic:
rw [← ENNReal.add_right_inj hfin, measure_inter_add_diff₀ _ ht, inter_comm,
    measure_inter_add_diff₀ _ hs, h]

Premises used: MeasureTheory.measure_inter_add_diff₀, ENNReal.add_right_inj, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
t : Set α
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∪ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₃ rw₄ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [union_comm, inter_comm, measure_union_add_inter₀ t hs, add_comm]

Premises used: Set.union_comm, add_comm, Set.inter_comm, MeasureTheory.measure_union_add_inter₀
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞)
rw₁ :
  (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (0 : ℝ≥0∞)
rw₂ rw₃ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [← measure_union_add_inter₀ s ht, hd, add_zero]

Premises used: add_zero, MeasureTheory.measure_union_add_inter₀
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
rw :
  (μ : (a : Set α) → ℝ≥0∞) (t ∪ s) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
rw₂ rw₃ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∪ t) =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
rw [union_comm, measure_union₀ hs (AEDisjoint.symm hd), add_comm]

Premises used: MeasureTheory.AEDisjoint.symm, Set.union_comm, add_comm, MeasureTheory.measure_union₀
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : NullMeasurableSet s μ
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ sᶜ) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) univ

Tactic:
rw [← measure_union₀' hs aedisjoint_compl_right, union_compl_self]

Premises used: MeasureTheory.aedisjoint_compl_right, Set.union_compl_self, MeasureTheory.measure_union₀'
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) sᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
simpa [hs] using measure_add_measure_compl₀ <| .of_compl <| .of_null hs

Premises used: MeasureTheory.measure_add_measure_compl₀
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass.{u_2} (NullMeasurableSpace α μ)
x : α
⊢ NullMeasurableSet {x} μ

Tactic:
@measurableSet_singleton _ _ _ _

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

Tactic:
measurableSet_insert

Premises used: MeasureTheory.NullMeasurableSet, measurableSet_insert, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass.{u_2} (NullMeasurableSpace α μ)
a : α
⊢ NullMeasurableSet {x : α | x = a} μ

Tactic:
nullMeasurableSet_singleton a

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

Tactic:
Finite.measurableSet hs

Premises used: MeasureTheory.NullMeasurableSet, Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass.{u_2} (NullMeasurableSpace α μ)
s : Finset α
⊢ NullMeasurableSet (↑s : Set α) μ

Tactic:
apply Finset.measurableSet

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

Tactic:
Finite.measurableSet_biUnion hs h

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

Tactic:
Finset.measurableSet_biUnion s h

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

Tactic:
Finite.measurableSet_sUnion hs h

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

Tactic:
Finite.measurableSet_biInter hs h

Premises used: Set.Finite.measurableSet_biInter, MeasureTheory.NullMeasurableSet, MeasureTheory.NullMeasurableSpace
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
ι : Type u_1
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : ι → Set α
s : Finset ι
h : ∀ b ∈ s, NullMeasurableSet (f b) μ
⊢ NullMeasurableSet (⋂ b ∈ s, f b) μ

Tactic:
s.finite_toSet.nullMeasurableSet_biInter h

Premises used: Set.Finite.nullMeasurableSet_biInter, Finset.finite_toSet
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set (Set α)
hs : s.Finite
h : ∀ t ∈ s, NullMeasurableSet t μ
⊢ NullMeasurableSet (⋂₀ s) μ

Tactic:
NullMeasurableSet.sInter (Finite.countable hs) h

Premises used: MeasureTheory.NullMeasurableSet.sInter, Set.Finite.countable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ NullMeasurableSet (toMeasurable μ s) μ

Tactic:
(measurableSet_toMeasurable _ _).nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measurableSet_toMeasurable
-- Module: Mathlib.MeasureTheory.Measure.NullMeasurable
Goal:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst_1 : MeasurableSingletonClass β
inst_2 : Countable β
μ : Measure (α × β)
x : α
⊢ Pairwise.{u_3} (α := β) (Function.onFun (β := Set (α × β)) Disjoint fun (x_1 : β) ↦ {(x, x_1)})

Tactic:
simp [Pairwise]

Premises used: Pairwise