awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))

Tactic:
rw [← ENNReal.toReal_add, measure_symmDiff_eq hs.nullMeasurableSet ht.nullMeasurableSet]

Premises used: ENNReal.toReal_add, MeasurableSet.nullMeasurableSet, MeasureTheory.measure_symmDiff_eq
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset diff_subset h₁

Premises used: Set.diff_subset, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top_of_subset diff_subset h₁

Premises used: Set.diff_subset, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset diff_subset h₂

Premises used: Set.diff_subset, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top_of_subset diff_subset h₂

Premises used: Set.diff_subset, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
inl :
  ∀ (hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)),
    μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
inr :
  ∀ (hu : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)),
    μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
rcases eq_top_or_lt_top (μ u) with hu | hu

Premises used: DFunLike.coe, eq_top_or_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u))
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
simp only [measureReal_def, measure_symmDiff_eq_top h₁ hu, ENNReal.toReal_top]

Premises used: MeasureTheory.measure_symmDiff_eq_top, MeasureTheory.measureReal_def, ENNReal.toReal_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u))

Tactic:
add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg

Premises used: add_nonneg, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u))

Tactic:
exact add_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg

Premises used: add_nonneg, ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hu : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)

Tactic:
exact le_trans (measureReal_mono (symmDiff_triangle s t u)
        (measure_union_ne_top (by finiteness) (by finiteness)))
      (measureReal_union_le (s ∆ t) (t ∆ u))

Premises used: MeasureTheory.measureReal_mono, MeasureTheory.measureReal_union_le, symmDiff_triangle, MeasureTheory.measure_union_ne_top, symmDiff, le_trans
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).Pairwise (AEDisjoint μ on f)
hm : ∀ b ∈ s, NullMeasurableSet (f b) μ
h : ∀ b ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)

Tactic:
simp only [measureReal_def, measure_biUnion_finset₀ hd hm, ENNReal.toReal_sum h]

Premises used: MeasureTheory.measure_biUnion_finset₀, MeasureTheory.measureReal_def, ENNReal.toReal_sum
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
s : Finset ι
f : ι → Set α
hd : (↑s : Set ι).PairwiseDisjoint f
hm : ∀ b ∈ s, MeasurableSet (f b)
h : ∀ b ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f b) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (⋃ b ∈ s, f b) = ∑ p ∈ s, μ.real (f p)

Tactic:
measureReal_biUnion_finset₀ hd.aedisjoint (fun b hb ↦ (hm b hb).nullMeasurableSet) h

Premises used: MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint, MeasureTheory.measureReal_biUnion_finset₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
h : ∀ a ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' {a}) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∑ b ∈ s, μ.real (f ⁻¹' {b}) = μ.real (f ⁻¹' (↑s : Set β))

Tactic:
simp only [measureReal_def, ← sum_measure_preimage_singleton s hf, ENNReal.toReal_sum h]

Premises used: MeasureTheory.sum_measure_preimage_singleton, MeasureTheory.measureReal_def, ENNReal.toReal_sum
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
inst : MeasurableSingletonClass α
inst_1 : SigmaFinite μ
s : Finset α
⊢ ∑ b ∈ s, μ.real {b} = μ.real (↑s : Set α)

Tactic:
simp [measureReal_def, ← ENNReal.toReal_sum (fun _ _ ↦ ne_of_lt measure_singleton_lt_top)]

Premises used: MeasureTheory.measure_singleton_lt_top, MeasureTheory.measureReal_def, ENNReal.toReal_sum, ne_of_lt
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₁)

Tactic:
rw [measure_diff_null']

Premises used: MeasureTheory.measure_diff_null'
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
(measureReal_eq_zero_iff (measure_ne_top_of_subset inter_subset_left h')).1 h

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset, Iff.mp, MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact (measureReal_eq_zero_iff (measure_ne_top_of_subset inter_subset_left h')).1 h

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset, Iff.mp, MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
inl : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s₁ \ s₂) = μ.real s₁
inr : ∀ (H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s₁ \ s₂) = μ.real s₁
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
rcases eq_top_or_lt_top (μ s₁) with H | H

Premises used: DFunLike.coe, eq_top_or_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
simp [measureReal_def, H, measure_diff_eq_top H h']

Premises used: MeasureTheory.measure_diff_eq_top, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
measureReal_diff_null' (measureReal_mono_null inter_subset_right h h') H.ne

Premises used: MeasureTheory.measureReal_diff_null', MeasureTheory.measureReal_mono_null, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ \ s₂) = μ.real s₁

Tactic:
exact measureReal_diff_null' (measureReal_mono_null inter_subset_right h h') H.ne

Premises used: MeasureTheory.measureReal_diff_null', MeasureTheory.measureReal_mono_null, Set.inter_subset_right, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (s ∪ t \ s) = μ.real (s ∪ t)
rw₁ rw₂ : μ.real (s ∪ t) = μ.real (s ∪ t)
⊢ μ.real s + μ.real (t \ s) = μ.real (s ∪ t)

Tactic:
rw [← measureReal_union' (@disjoint_sdiff_right _ s t) hs h₁
    (measure_ne_top_of_subset diff_subset h₂), union_diff_self]

Premises used: Set.diff_subset, Set.disjoint_sdiff_right, MeasureTheory.measure_ne_top_of_subset, MeasureTheory.measureReal_union', Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (s \ t) = μ.real t + μ.real (s \ t) - μ.real t
⊢ μ.real (s \ t) = μ.real (s ∪ t) - μ.real t

Tactic:
rw [union_comm, ← measureReal_add_diff hm h₂ h₁]

Premises used: Set.union_comm, MeasureTheory.measureReal_add_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hm : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s \ t) = μ.real t + μ.real (s \ t) - μ.real t

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : MeasurableSet s₂
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (s₁ ∪ s₂) - μ.real s₂ = μ.real s₁ - μ.real s₂
rw₁ rw₂ : μ.real s₁ - μ.real s₂ = μ.real s₁ - μ.real s₂
⊢ μ.real (s₁ \ s₂) = μ.real s₁ - μ.real s₂

Tactic:
rw [measureReal_diff' h₂ h₁ (measure_ne_top_of_subset h h₁), union_eq_self_of_subset_right h]

Premises used: Set.union_eq_self_of_subset_right, MeasureTheory.measure_ne_top_of_subset, MeasureTheory.measureReal_diff'
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
simp : μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)
⊢ μ.real s₁ - μ.real s₂ ≤ μ.real (s₁ \ s₂)

Tactic:
simp only [tsub_le_iff_left]

Premises used: tsub_le_iff_left
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ ≤ μ.real (s₂ ∪ s₁)

Tactic:
measureReal_le_measureReal_union_right h

Premises used: MeasureTheory.measureReal_le_measureReal_union_right
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₂ ∪ s₁) = μ.real (s₂ ∪ s₁ \ s₂)

Tactic:
congr_arg μ.real union_diff_self.symm

Premises used: MeasureTheory.Measure.real, congr_arg, Eq.symm, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₂ ∪ s₁ \ s₂) ≤ μ.real s₂ + μ.real (s₁ \ s₂)

Tactic:
measureReal_union_le _ _

Premises used: MeasureTheory.measureReal_union_le
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ ≤ μ.real s₂ + μ.real (s₁ \ s₂)

Tactic:
calc
    μ.real s₁ ≤ μ.real (s₂ ∪ s₁) := measureReal_le_measureReal_union_right h
    _ = μ.real (s₂ ∪ s₁ \ s₂) := congr_arg μ.real union_diff_self.symm
    _ ≤ μ.real s₂ + μ.real (s₁ \ s₂) := measureReal_union_le _ _

Premises used: MeasureTheory.Measure.real, MeasureTheory.measureReal_union_le, congr_arg, SDiff.sdiff, MeasureTheory.measureReal_le_measureReal_union_right, Union.union, Eq.symm, Set.union_diff_self
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real t - μ.real s < ε
⊢ μ.real (t \ s) < ε

Tactic:
rw [measureReal_diff hst hs ht']

Premises used: MeasureTheory.measureReal_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
h : μ.real t < μ.real s + ε
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
linarith : ε ≤ μ.real t - μ.real s → μ.real t - (μ.real s + ε) + (ε - (μ.real t - μ.real s)) = 0
⊢ μ.real t - μ.real s < ε

Tactic:
linarith
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
hst : s ⊆ t
ε : ℝ
ht' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real t - μ.real s ≤ ε ↔ μ.real t ≤ μ.real s + ε
rw₁ rw₂ : μ.real t ≤ μ.real s + ε ↔ μ.real t ≤ μ.real s + ε
⊢ μ.real (t \ s) ≤ ε ↔ μ.real t ≤ μ.real s + ε

Tactic:
rw [measureReal_diff hst hs ht', tsub_le_iff_left]

Premises used: MeasureTheory.measureReal_diff, tsub_le_iff_left
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : μ.real (t \ s) = 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [measureReal_eq_zero_iff h] at h_nulldiff

Premises used: MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : μ.real (t \ s) = 0
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_nulldiff₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measureReal_eq_zero_iff h] at h_nulldiff

Premises used: MeasureTheory.measureReal_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hst : s ⊆ t
h_nulldiff : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s = μ.real t

Tactic:
simp [measureReal_def, measure_eq_measure_of_null_diff hst h_nulldiff]

Premises used: MeasureTheory.measureReal_def, MeasureTheory.measure_eq_measure_of_null_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)

Tactic:
have A : μ s₁ = μ s₂ ∧ μ s₂ = μ s₃ :=
    measure_eq_measure_of_between_null_diff h12 h23 ((measureReal_eq_zero_iff h').1 h_nulldiff)
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ∧
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₃ : ℝ≥0∞)
⊢ μ.real s₁ = μ.real s₂ ∧ μ.real s₂ = μ.real s₃

Tactic:
simp [measureReal_def, A.1, A.2]

Premises used: And.right, And.left, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₁ = μ.real s₂

Tactic:
(measureReal_eq_measureReal_of_between_null_diff h12 h23 h_nulldiff h').1

Premises used: MeasureTheory.measureReal_eq_measureReal_of_between_null_diff, And.left
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ s₃ : Set α
h12 : s₁ ⊆ s₂
h23 : s₂ ⊆ s₃
h_nulldiff : μ.real (s₃ \ s₁) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₃ \ s₁) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s₂ = μ.real s₃

Tactic:
(measureReal_eq_measureReal_of_between_null_diff h12 h23 h_nulldiff h').2

Premises used: MeasureTheory.measureReal_eq_measureReal_of_between_null_diff, And.right
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : MeasurableSet s
rw : μ.real (univ \ s) = μ.real univ - μ.real s
⊢ μ.real sᶜ = μ.real univ - μ.real s

Tactic:
rw [compl_eq_univ_diff]

Premises used: Set.compl_eq_univ_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real (univ \ s) = μ.real univ - μ.real s

Tactic:
measureReal_diff (subset_univ s) h₁

Premises used: Set.subset_univ, MeasureTheory.measureReal_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : MeasurableSet s
⊢ μ.real (univ \ s) = μ.real univ - μ.real s

Tactic:
exact measureReal_diff (subset_univ s) h₁

Premises used: Set.subset_univ, MeasureTheory.measureReal_diff
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h₁ : NullMeasurableSet s μ
linarith :
  μ.real sᶜ < μ.real univ - μ.real s → μ.real sᶜ - (μ.real univ - μ.real s) + -(μ.real s + μ.real sᶜ - μ.real univ) = 0
linarith₁ :
  μ.real univ - μ.real s < μ.real sᶜ → μ.real univ - μ.real s - μ.real sᶜ + (μ.real s + μ.real sᶜ - μ.real univ) = 0
⊢ μ.real sᶜ = μ.real univ - μ.real s

Tactic:
linarith [measureReal_add_measureReal_compl₀ h₁]

Premises used: MeasureTheory.measureReal_add_measureReal_compl₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)
rw₁ : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ t₁)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₂ ∪ t₂))

Tactic:
rw [measure_union_congr_of_subset hs _ ht]

Premises used: MeasureTheory.measure_union_congr_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ t₁ t₂ : Set α
hs : s₁ ⊆ s₂
hsμ : μ.real s₂ ≤ μ.real s₁
ht : t₁ ⊆ t₂
htμ : μ.real t₂ ≤ μ.real t₁
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t₁ : ℝ≥0∞)

Tactic:
(ENNReal.toReal_le_toReal h₂ (measure_ne_top_of_subset ht h₂)).1 htμ

Premises used: MeasureTheory.measure_ne_top_of_subset, Iff.mp, ENNReal.toReal_le_toReal