awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have inl : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic: rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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₂
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have inr : ∀ (h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)),
  μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
Tactic: rcases eq_top_or_lt_top (μ (s₁ ∪ s₂)) with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have inl : 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₁) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₂)
Tactic: simp only [Measure.real, h, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have A : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have A : μ s₁ ≠ ∞ := measure_ne_top_of_subset subset_union_left h.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
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∞)
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have B : μ s₂ ≠ ∞ := measure_ne_top_of_subset subset_union_right h.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (s₁ ∪ s₂) ≤ μ.real s₁ + μ.real s₂
have inr : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∪ s₂)) ≤
  (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞)).toReal
Tactic: simp only [Measure.real, ← ENNReal.toReal_add A B]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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 (⋃ b ∈ insert a s, f b) ≤ ∑ p ∈ insert a s, μ.real (f p)
have insert : μ.real (f a ∪ ⋃ x ∈ s, f x) ≤ μ.real (f a) + ∑ p ∈ s, μ.real (f p)
Tactic: simp only [hx, Finset.mem_insert, iUnion_iUnion_eq_or_left, not_false_eq_true,
      Finset.sum_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
have empty : μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) ∅ b), f b) ≤ ∑ p ∈ ∅, μ.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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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)
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
have insert : ∀ (a : β) (s : Finset β) (hx : a ∉ s) (IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)),
  μ.real (⋃ b ∈ insert a s, f b) ≤ ∑ p ∈ insert a 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
s : Finset β
f : β → Set α
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
have empty : μ.real (⋃ (b : β), ⋃ (_ : Membership.mem (γ := Finset β) ∅ b), f b) ≤ ∑ p ∈ ∅, μ.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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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)
⊢ μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)
have insert : ∀ (a : β) (s : Finset β) (hx : a ∉ s) (IH : μ.real (⋃ b ∈ s, f b) ≤ ∑ p ∈ s, μ.real (f p)),
  μ.real (⋃ b ∈ insert a s, f b) ≤ ∑ p ∈ insert a 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)
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
β : Type u_2
x : MeasurableSpace α
μ : Measure α
inst : Fintype β
f : β → Set α
⊢ μ.real (⋃ (b : β), f b) ≤ ∑ p : β, μ.real (f p)
have h : ∀ (x : β), f x = ⋃ (_ : Membership.mem (γ := Finset β) Finset.univ x), f x
Tactic: convert! measureReal_biUnion_finset_le Finset.univ f
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (⋃ (b : β), f b) = ∑ p : β, μ.real (f p)
have simp_rw : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (⋃ (b : β), f b)) =
  ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
Tactic: simp_rw [measureReal_def, measure_iUnion hn h, tsum_fintype,
    ENNReal.toReal_sum (fun i _hi ↦ h' i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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))
⊢ μ.real (⋃ (b : β), f b) = ∑ p : β, μ.real (f p)
have simp_rw₁ : ENNReal.toReal (∑' (i : β), (μ : (a : Set α) → ℝ≥0∞) (f i)) =
  ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
Tactic: simp_rw [measureReal_def, measure_iUnion hn h, tsum_fintype,
    ENNReal.toReal_sum (fun i _hi ↦ h' i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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))
⊢ μ.real (⋃ (b : β), f b) = ∑ p : β, μ.real (f p)
have simp_rw₂ : ENNReal.toReal (∑ i : β, (μ : (a : Set α) → ℝ≥0∞) (f i)) = ∑ x_1 : β, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (f x_1))
Tactic: simp_rw [measureReal_def, measure_iUnion hn h, tsum_fintype,
    ENNReal.toReal_sum (fun i _hi ↦ h' i)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : NullMeasurableSet t μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
have ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_inter_add_diff₀ s ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
have hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_inter_add_diff₀ s ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (hypothesis)
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∞)
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have this : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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 (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have rw : μ.real t + μ.real (s \ t) + μ.real (s ∩ t) = μ.real (s ∩ t) + μ.real (s \ t) + μ.real t
Tactic: rw [← measureReal_inter_add_diff₀ ht this, Set.union_inter_cancel_right, union_diff_right,
    ← measureReal_inter_add_diff₀ ht h₁]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have rw : μ.real (t ∪ s) + μ.real (s ∩ t) = μ.real s + μ.real t
Tactic: rw [union_comm, inter_comm, measureReal_union_add_inter₀ hs h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have rw₁ : μ.real (t ∪ s) + μ.real (t ∩ s) = μ.real s + μ.real t
Tactic: rw [union_comm, inter_comm, measureReal_union_add_inter₀ hs h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have rw₂ : μ.real t + μ.real s = μ.real s + μ.real t
Tactic: rw [union_comm, inter_comm, measureReal_union_add_inter₀ hs h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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
⊢ μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
have rw₃ : μ.real s + μ.real t = μ.real s + μ.real t
Tactic: rw [union_comm, inter_comm, measureReal_union_add_inter₀ hs h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
have 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)
Tactic: rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∪ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
have 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)
Tactic: rw [measure_union₀ ht hd, ENNReal.toReal_add h₁ h₂]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
have rw : μ.real (t ∪ s) = μ.real s + μ.real t
Tactic: rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
have rw₁ : μ.real t + μ.real s = μ.real s + μ.real t
Tactic: rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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
⊢ μ.real (s ∪ t) = μ.real s + μ.real t
have rw₂ : μ.real s + μ.real t = μ.real s + μ.real t
Tactic: rw [union_comm, measureReal_union₀ hs (AEDisjoint.symm hd) h₂ h₁, add_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
⊢ μ.real s + μ.real sᶜ = μ.real univ
have rw : μ.real (s ∪ sᶜ) = μ.real univ
Tactic: rw [← measureReal_union₀' hs aedisjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsFiniteMeasure μ
hs : NullMeasurableSet s μ
rw : μ.real (s ∪ sᶜ) = μ.real univ
⊢ μ.real s + μ.real sᶜ = μ.real univ
have rw₁ : μ.real univ = μ.real univ
Tactic: rw [← measureReal_union₀' hs aedisjoint_compl_right, union_compl_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t : Set α
ht : MeasurableSet t
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
have ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_inter_add_diff _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∩ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s)
have hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_inter_add_diff _ ht]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
have ha : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s \ t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_symmDiff_eq hs.nullMeasurableSet ht.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) =
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s \ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t \ s))
have hb : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← ENNReal.toReal_add, measure_symmDiff_eq hs.nullMeasurableSet ht.nullMeasurableSet]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
have inl : ∀ (hu : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic: rcases eq_top_or_lt_top (μ u) with hu | hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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)
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
have inr : ∀ (hu : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)),
  μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
Tactic: rcases eq_top_or_lt_top (μ u) with hu | hu
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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∞)
⊢ μ.real (s ∆ u) ≤ μ.real (s ∆ t) + μ.real (t ∆ u)
have inl : 0 ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s ∆ t)) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t ∆ u))
Tactic: simp only [measureReal_def, measure_symmDiff_eq_top h₁ hu, ENNReal.toReal_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real (s₁ ∩ s₂) = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (s₁ \ s₂)) = ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s₁)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s₁ ∩ s₂) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [measure_diff_null']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : μ.real s₂ = 0
h' : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₂ : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real (s₁ \ s₂) = μ.real s₁
have inl : ∀ (H : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s₁ \ s₂) = μ.real s₁
Tactic: rcases eq_top_or_lt_top (μ s₁) with H | H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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₁
⊢ μ.real (s₁ \ s₂) = μ.real s₁
have inr : ∀ (H : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞) (∞ : ℝ≥0∞)), μ.real (s₁ \ s₂) = μ.real s₁
Tactic: rcases eq_top_or_lt_top (μ s₁) with H | H
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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 + μ.real (t \ s) = μ.real (s ∪ t)
have rw : μ.real (s ∪ 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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)
⊢ μ.real s + μ.real (t \ s) = μ.real (s ∪ t)
have rw₁ : μ.real (s ∪ t) = μ.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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Real (goal)
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 (s ∪ t) - μ.real t
have rw : μ.real (s \ t) = μ.real t + μ.real (s \ t) - μ.real t
Tactic: rw [union_comm, ← measureReal_add_diff hm h₂ h₁]