awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
hs' : (↑s' : Set α) ∈ measurableAtom '' s
h₁ :
  ∀ (x : α) (hxs : x ∈ s) (hx : measurableAtom x = (↑s' : Set α)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)

Tactic:
obtain ⟨x, hxs, hx⟩ := hs'
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
x : α
hxs : x ∈ s
hx : measurableAtom x = (↑s' : Set α)
h₁ :
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (↑s' : Set α) : ℝ≥0∞)

Tactic:
rw [← hx]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
x : α
hxs : x ∈ s
hx : measurableAtom x = (↑s' : Set α)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)

Tactic:
h x
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m : MeasurableSpace α
inst : Countable α
μ ν : Measure α
h :
  ∀ (x : α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
h1 : s = ⋃₀ (measurableAtom '' s)
h_count : (measurableAtom '' s).Countable
h_disj : (measurableAtom '' s).Pairwise Disjoint
h_meas : ∀ (t : Set α) (ht : t ∈ measurableAtom '' s), MeasurableSet t
s' : (↑(measurableAtom '' s) : Type u_1)
x : α
hxs : x ∈ s
hx : measurableAtom x = (↑s' : Set α)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (measurableAtom x) : ℝ≥0∞)

Tactic:
exact h x
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : Measure α
⊢ ms ≤ μ.caratheodory

Tactic:
fun _s hs _t => (measure_inter_add_diff _ hs).symm

Premises used: MeasurableSet, MeasureTheory.OuterMeasure.IsCaratheodory, MeasureTheory.measure_inter_add_diff, Eq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
⊢ (m.toMeasure h).toOuterMeasure = m.trim

Tactic:
rfl

Premises used: MeasureTheory.inducedOuterMeasure, MeasureTheory.OuterMeasure.trim, rfl, MeasureTheory.OuterMeasure.ofFunction
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
m.trim_eq hs

Premises used: MeasureTheory.OuterMeasure.trim_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
m.le_trim s

Premises used: MeasureTheory.OuterMeasure.le_trim
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_antisymm ?_ (le_toMeasure_apply _ _ _)

Premises used: le_antisymm, MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
refine : LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: le_antisymm, MeasureTheory.le_toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
rcases :
  ∀ (t : Set α) (hts : t ⊆ s) (htm : MeasurableSet t) (heq : t =ᶠ[ae (m.toMeasure h)] s),
    LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases hs.exists_measurable_subset_ae_eq with ⟨t, hts, htm, heq⟩

Premises used: MeasureTheory.NullMeasurableSet.exists_measurable_subset_ae_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
measure_congr heq.symm

Premises used: MeasureTheory.measure_congr, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ Eq (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
toMeasure_apply m h htm

Premises used: MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ LE.le (α := ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
m.mono hts

Premises used: MeasureTheory.OuterMeasure.mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
m : OuterMeasure α
h : ms ≤ m.caratheodory
s : Set α
hs : NullMeasurableSet s (m.toMeasure h)
t : Set α
hts : t ⊆ s
htm : MeasurableSet t
heq : t =ᶠ[ae (m.toMeasure h)] s
⊢ LE.le (α := ℝ≥0∞) ((m.toMeasure h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    m.toMeasure h s = m.toMeasure h t := measure_congr heq.symm
    _ = m t := toMeasure_apply m h htm
    _ ≤ m s := m.mono hts

Premises used: MeasureTheory.measure_congr, MeasureTheory.OuterMeasure.mono, MeasureTheory.OuterMeasure.toMeasure, MeasureTheory.toMeasure_apply, DFunLike.coe, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : Measure α
⊢ μ.toMeasure ⋯ = μ

Tactic:
Measure.ext fun _s => μ.toOuterMeasure.trim_eq

Premises used: MeasureTheory.Measure.toOuterMeasure, MeasureTheory.OuterMeasure.trim_eq, MeasureTheory.Measure.ext
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : Measure α
⊢ OuterMeasure.boundedBy (⇑μ : (a : Set α) → ℝ≥0∞) = μ.toOuterMeasure

Tactic:
μ.toOuterMeasure.boundedBy_eq_self

Premises used: MeasureTheory.OuterMeasure.boundedBy_eq_self, MeasureTheory.Measure.toOuterMeasure
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [h] at ht_ne_top
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)

Tactic:
refine le_antisymm (by gcongr) ?_

Premises used: le_antisymm
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (t \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)

Tactic:
have A : μ (u ∩ s) + μ (u \ s) ≤ μ (t ∩ s) + μ (u \ s) :=
    calc
      μ (u ∩ s) + μ (u \ s) = μ u := measure_inter_add_diff _ hs
      _ = μ t := h.symm
      _ = μ (t ∩ s) + μ (t \ s) := (measure_inter_add_diff _ hs).symm
      _ ≤ μ (t ∩ s) + μ (u \ s) := by gcongr
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have B : μ (u \ s) ≠ ∞ := (lt_of_le_of_lt (measure_mono diff_subset) ht_ne_top.lt_top).ne
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
ENNReal.le_of_add_le_add_right B A

Premises used: ENNReal.le_of_add_le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞)
htu : t ⊆ u
ht_ne_top : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
A :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
B : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
exact ENNReal.le_of_add_le_add_right B A

Premises used: ENNReal.le_of_add_le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_antisymm (measure_mono inter_subset_right) ?_

Premises used: le_antisymm, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine le_antisymm (measure_mono inter_subset_right) ?_

Premises used: le_antisymm, MeasureTheory.measure_mono, Set.inter_subset_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
H : s ≤ᶠ[ae μ] t ∩ s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
apply EventuallyLE.measure_le

Premises used: Filter.EventuallyLE.measure_le
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
x : α
hx : x ∈ t
h'x : s x
⊢ (t ∩ s) x

Tactic:
⟨hx, h'x⟩

Premises used: setOf, Set.inter, And.intro
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ s x ≤ (t ∩ s) x) x} x}
      a
h₂ : ∀ a ∈ t, s a ≤ (t ∩ s) a
h₃ : ∀ (x : α) (hx : x ∈ t) (h'x : s x), (t ∩ s) x
⊢ s ≤ᶠ[ae μ] t ∩ s

Tactic:
filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ t ∩ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
(measure_inter_eq_of_measure_eq hs (measure_toMeasurable t).symm (subset_toMeasurable μ t)
      ht).symm

Premises used: MeasureTheory.subset_toMeasurable, MeasureTheory.measure_toMeasurable, Eq.symm, MeasureTheory.Measure.measure_inter_eq_of_measure_eq
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := OuterMeasure α) (toOuterMeasure 0) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
_m : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := (a : Set α) → ℝ≥0∞) (⇑0 : (a : Set α) → ℝ≥0∞) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
h₁ :
  ∀ (s : Set α) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞) ((OuterMeasure.toMeasure 0 h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ OuterMeasure.toMeasure 0 h = 0

Tactic:
ext s hs
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((OuterMeasure.toMeasure 0 h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [hs]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
h₁ :
  ∀ (s : Set α),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = 0

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)

Premises used: le_bot_iff, LE.le.trans_eq, congrArg, id, MeasureTheory.le_toMeasure_apply, Iff.mp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact le_bot_iff.1 <| (le_toMeasure_apply _ _ _).trans_eq congr($hμ s)

Premises used: le_bot_iff, LE.le.trans_eq, congrArg, id, MeasureTheory.le_toMeasure_apply, Iff.mp, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
inst : IsEmpty α
x : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [eq_empty_of_isEmpty s, measure_empty]

Premises used: MeasureTheory.measure_empty, Set.eq_empty_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν_1 ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ μ = ν

Tactic:
ext1 s _
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν_1 ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
inst_1 : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_1 : MeasurableSet s
h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h₁ h₂ : Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]

Premises used: MeasureTheory.Measure.apply_eq_zero_of_isEmpty
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
inst : IsEmpty α
_m : MeasurableSpace α
μ : Measure α
⊢ μ = 0

Tactic:
Subsingleton.elim μ 0

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
⊢ ∀ ⦃f : ℕ → Set α⦄ (h : ∀ (i : ℕ), MeasurableSet (f i)),
    Pairwise (Disjoint on f) →
      Eq (α := ℝ≥0∞) ((fun (x : Set α) (x_1 : MeasurableSet x) ↦ (0 : ℝ≥0∞)) (⋃ (i : ℕ), f i) ⋯)
        (∑' (i : ℕ), (fun (x : Set α) (x_1 : MeasurableSet x) ↦ (0 : ℝ≥0∞)) (f i) ⋯)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
h :
  ∀ (s : Set α),
    MeasurableSet s →
      Eq (α := ℝ≥0∞)
        (((ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) ↦ 0) ⋯ ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
        (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Measure α) (ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) ↦ 0) ⋯ ⋯) 0

Tactic:
ext s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) ↦ 0) ⋯ ⋯ : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp [ofMeasurable, ← toOuterMeasure_apply, inducedOuterMeasure_zero MeasurableSet.iUnion]

Premises used: MeasureTheory.Measure.toOuterMeasure_apply, MeasureTheory.inducedOuterMeasure_zero, MeasureTheory.Measure.ofMeasurable, MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
rw₂ rw₃ :
  HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (i : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s i)) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
        ((μ₂ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [ENNReal.tsum_add, measure_iUnion hd hs, measure_iUnion hd hs]

Premises used: ENNReal.tsum_add, MeasureTheory.measure_iUnion