awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
hs : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real s ≤ μ.real (s ∪ t)

Tactic:
exact measureReal_mono subset_union_left (measure_union_lt_top hs h.lt_top).ne

Premises used: MeasureTheory.measure_union_lt_top, MeasureTheory.measureReal_mono, Set.subset_union_left, Ne.lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real t ≤ μ.real (t ∪ s)
⊢ μ.real t ≤ μ.real (s ∪ t)

Tactic:
rw [union_comm]

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

Tactic:
measureReal_le_measureReal_union_left h

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

Tactic:
exact measureReal_le_measureReal_union_left h

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

Tactic:
rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h

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

Tactic:
simp only [Measure.real, h, ENNReal.toReal_top]

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

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₁ s₂ : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₁) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₂)

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₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
inr :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂)) ≤
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)).toReal
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂

Tactic:
simp only [Measure.real, ← ENNReal.toReal_add A B]

Premises used: ENNReal.toReal_add, MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) ≠ ∞

Tactic:
simp [A, B]
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂)) ≤
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)).toReal

Tactic:
exact ENNReal.toReal_mono (by simp [A, B]) (measure_union_le _ _)

Premises used: ENNReal.toReal_mono, MeasureTheory.measure_union_le
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
f : β → Set α
⊢ μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) ∅ b), f b) ≤ ∑ p ∈ ∅, μ.real (f p)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
f : β → Set α
a : β
s : Finset β
hx : a ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
insert : μ.real (f a ∪ ⋃ x ∈ s, f x) ≤ μ.real (f a) + ∑ p ∈ s, μ.real (f p)
⊢ μ.real (⋃ b ∈ Insert.insert a s, f b) ≤ ∑ p ∈ Insert.insert a s, μ.real (f p)

Tactic:
simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]

Premises used: Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
f : β → Set α
a : β
s : Finset β
hx : a ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f a) + μ.real (⋃ x ∈ s, f x) ≤ μ.real (f a) + ∑ p ∈ s, μ.real (f p)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
f : β → Set α
a : β
s : Finset β
hx : a ∉ s
IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
⊢ μ.real (f a ∪ ⋃ x ∈ s, f x) ≤ μ.real (f a) + ∑ p ∈ s, μ.real (f p)

Tactic:
exact (measureReal_union_le _ _).trans (by gcongr)

Premises used: MeasureTheory.measureReal_union_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
empty : μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) ∅ b), f b) ≤ ∑ p ∈ ∅, μ.real (f p)
insert :
  ∀ (a : β) (s : Finset β) (hx : a ∉ s) (IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)),
    μ.real (⋃ b ∈ Insert.insert a s, f b) ≤ ∑ p ∈ Insert.insert a s, μ.real (f p)
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)

Tactic:
induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hx IH =>
    simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]
    exact (measureReal_union_le _ _).trans (by gcongr)

Premises used: MeasureTheory.measureReal_union_le, Insert.insert, Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, LE.le.trans, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
empty : μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) ∅ b), f b) ≤ ∑ p ∈ ∅, μ.real (f p)
insert :
  ∀ (a : β) (s : Finset β) (hx : a ∉ s) (IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)),
    μ.real (⋃ b ∈ Insert.insert a s, f b) ≤ ∑ p ∈ Insert.insert a s, μ.real (f p)
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)

Tactic:
classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hx IH =>
    simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]
    exact (measureReal_union_le _ _).trans (by gcongr)

Premises used: MeasureTheory.measureReal_union_le, Insert.insert, Finset.mem_insert, Set.iUnion_iUnion_eq_or_left, LE.le.trans, Finset.sum_insert, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : Fintype β
f : β → Set α
⊢ μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) Finset.univ b), f b) ≤ ∑ p : β, μ.real (f p)

Tactic:
measureReal_biUnion_finset_le Finset.univ f

Premises used: Finset.univ, MeasureTheory.measureReal_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : Fintype β
f : β → Set α
h : ∀ (x : β), f x = ⋃ (_ : Membership.mem (γ := Finset β) Finset.univ x), f x
⊢ μ.real (⋃ (b : β), f b) ≤ ∑ p : β, μ.real (f p)

Tactic:
convert! measureReal_biUnion_finset_le Finset.univ f

Premises used: Finset.univ, MeasureTheory.measureReal_biUnion_finset_le
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : Fintype β
f : β → Set α
x_1 : β
⊢ f x_1 = ⋃ (_ : Membership.mem (γ := Finset β) Finset.univ x_1), f x_1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : Fintype β
f : β → Set α
hn : Pairwise (Disjoint on f)
h : ∀ (i : β), MeasurableSet (f i)
h' : ∀ (i : β), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) (∞ : ℝ≥0∞)
simp_rw :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : β), f b)) =
    ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
simp_rw₁ :
  ENNReal.toReal (∑' (i : β), (μ : (a : Set α) → ℝ≥0∞) (f i)) =
    ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
simp_rw₂ :
  ENNReal.toReal (∑ i : β, (μ : (a : Set α) → ℝ≥0∞) (f i)) =
    ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
⊢ μ.real (⋃ (b : β), f b) = ∑ p : β, μ.real (f p)

Tactic:
simp_rw [measureReal_def, measure_iUnion hn h, tsum_fintype,
    ENNReal.toReal_sum (fun i _hi ↦ h' i)]

Premises used: MeasureTheory.measure_iUnion, tsum_fintype, MeasureTheory.measureReal_def, ENNReal.toReal_sum
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : μ.real s₁ = 0
h₂ : μ.real s₂ = 0
⊢ μ.real s₁ + μ.real s₂ ≤ 0

Tactic:
simp [h₁, h₂]
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
h : μ.real (s₁ ∪ s₂) = 0
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
H : s =ᶠ[ae μ] t
⊢ μ.real s = μ.real t

Tactic:
simp [Measure.real, measure_congr H]

Premises used: MeasureTheory.measure_congr, MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [← ENNReal.toReal_add, measure_inter_add_diff₀ s ht]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_inter_add_diff₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
measure_ne_top_of_subset inter_subset_left h

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact measure_ne_top_of_subset inter_subset_left h

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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 α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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 α
ht : NullMeasurableSet 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:
have : μ (s ∪ t) ≠ ∞ :=
    ((measure_union_le _ _).trans_lt (ENNReal.add_lt_top.2 ⟨h₁.lt_top, h₂.lt_top⟩ )).ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
rw [← measureReal_inter_add_diff₀ ht this, Set.union_inter_cancel_right, union_diff_right,
    ← measureReal_inter_add_diff₀ ht h₁]

Premises used: MeasureTheory.measureReal_inter_add_diff₀, Set.union_diff_right, Set.union_inter_cancel_right
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
this : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t

Tactic:
ac_rfl
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (t ∪ s) + μ.real (s ∩ t) = μ.real s + μ.real t
rw₁ : μ.real (t ∪ s) + μ.real (t ∩ s) = μ.real s + μ.real t
rw₂ : μ.real t + μ.real s = μ.real s + μ.real t
rw₃ rw₄ : μ.real s + μ.real t = μ.real s + μ.real t
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
rw [union_comm, inter_comm, measureReal_union_add_inter₀ hs h₂ h₁, add_comm]

Premises used: Set.union_comm, add_comm, MeasureTheory.measureReal_union_add_inter₀, Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
hd : AEDisjoint μ s t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
rw₁ rw₂ :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_union₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
hs : NullMeasurableSet s μ
hd : AEDisjoint μ s t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : μ.real (t ∪ s) = μ.real s + μ.real t
rw₁ : μ.real t + μ.real s = μ.real s + μ.real t
rw₂ rw₃ : μ.real s + μ.real t = μ.real s + μ.real t
⊢ μ.real (s ∪ t) = μ.real s + μ.real t

Tactic:
rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]

Premises used: MeasureTheory.AEDisjoint.symm, Set.union_comm, add_comm, MeasureTheory.measureReal_union₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
rw : μ.real (s ∪ sᶜ) = μ.real univ
rw₁ rw₂ : μ.real univ = μ.real univ
⊢ μ.real s + μ.real sᶜ = μ.real univ

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

Premises used: MeasureTheory.aedisjoint_compl_right, MeasureTheory.measureReal_union₀', Set.union_compl_self
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
h : MeasurableSet s
⊢ μ.real s + μ.real sᶜ = μ.real univ

Tactic:
measureReal_add_measureReal_compl₀ h.nullMeasurableSet

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measureReal_add_measureReal_compl₀
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h : MeasurableSet s₂
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

Tactic:
measureReal_union₀ h.nullMeasurableSet hd.aedisjoint h₁ h₂

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measureReal_union₀, Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
hd : Disjoint s₁ s₂
h : MeasurableSet s₁
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ ∪ s₂) = μ.real s₁ + μ.real s₂

Tactic:
measureReal_union₀' h.nullMeasurableSet hd.aedisjoint h₁ h₂

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measureReal_union₀', Disjoint.aedisjoint
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)

Tactic:
rw [← ENNReal.toReal_add, measure_inter_add_diff _ ht]

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

Tactic:
measure_ne_top_of_subset inter_subset_left h

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

Tactic:
exact measure_ne_top_of_subset inter_subset_left h

Premises used: Set.inter_subset_left, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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 α
ht : MeasurableSet t
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥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 α
ht : MeasurableSet t
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s \ t) + μ.real (s ∩ t) = μ.real s

Tactic:
(add_comm _ _).trans (measureReal_inter_add_diff ht h)

Premises used: add_comm, MeasureTheory.measureReal_inter_add_diff, Eq.trans
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h₂ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
measureReal_union_add_inter₀ ht.nullMeasurableSet h₁ h₂

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measureReal_union_add_inter₀
-- 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∞)
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t

Tactic:
measureReal_union_add_inter₀' hs.nullMeasurableSet h₁ h₂

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.measureReal_union_add_inter₀'