awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact (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
-- 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∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)

Tactic:
(ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ

Premises used: MeasureTheory.measure_ne_top_of_subset, Iff.mp, ENNReal.toReal_le_toReal
-- 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∞) s₂ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s₁ : ℝ≥0∞)

Tactic:
exact (ENNReal.toReal_le_toReal h₁ (measure_ne_top_of_subset hs h₁)).1 hsμ

Premises used: MeasureTheory.measure_ne_top_of_subset, Iff.mp, ENNReal.toReal_le_toReal
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ ∀ a ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
rw : ENNReal.toReal (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)
⊢ ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)

Tactic:
rw [← ENNReal.toReal_sum (by finiteness)]

Premises used: ENNReal.toReal_sum
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
apply : LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
⊢ ENNReal.toReal (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a)) ≤ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ)

Tactic:
apply ENNReal.toReal_mono (by finiteness)

Premises used: ENNReal.toReal_mono
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
sum_measure_le_measure_univ (fun i mi ↦ (h i mi).nullMeasurableSet) H.aedisjoint

Premises used: MeasurableSet.nullMeasurableSet, Set.PairwiseDisjoint.aedisjoint, MeasureTheory.sum_measure_le_measure_univ
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : (↑s : Set ι).PairwiseDisjoint t
⊢ LE.le (α := ℝ≥0∞) (∑ a ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)

Tactic:
exact sum_measure_le_measure_univ (fun i mi ↦ (h i mi).nullMeasurableSet) H.aedisjoint

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

Tactic:
simp only [measureReal_def, add_apply, ENNReal.toReal_add h₁ h₂]

Premises used: ENNReal.toReal_add, MeasureTheory.Measure.add_apply, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
apply : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ ∃ i ∈ s, ∃ j ∈ s, ∃ (_ : i ≠ j), (t i ∩ t j).Nonempty

Tactic:
apply exists_nonempty_inter_of_measure_univ_lt_sum_measure μ
    (fun i mi ↦ (h i mi).nullMeasurableSet)

Premises used: MeasurableSet.nullMeasurableSet, MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_sum_measure
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : μ.real univ < ∑ i ∈ s, μ.real (t i)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))

Tactic:
simp only [Measure.real] at H

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
apply : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i))
apply₁ : Ne (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) ∞
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
apply (ENNReal.toReal_lt_toReal (by finiteness) _).1

Premises used: ENNReal.toReal_lt_toReal, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))

Tactic:
H
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
h₁ :
  ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) =
    ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i))

Tactic:
convert! H
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ ∀ a ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t a) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
h₁ h₂ :
  Eq (α := ℝ) (∑ a ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t a)))
    (∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1)))
⊢ ENNReal.toReal (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) =
    ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))

Tactic:
rw [ENNReal.toReal_sum (by finiteness)]

Premises used: ENNReal.toReal_sum
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) ∞

Tactic:
(ENNReal.sum_lt_top.mpr (fun i hi ↦ measure_lt_top ..)).ne

Premises used: Iff.mpr, MeasureTheory.measure_lt_top, ENNReal.sum_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
ι : Type u_3
x : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s : Finset ι
t : ι → Set α
h : ∀ i ∈ s, MeasurableSet (t i)
H : ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) univ) < ∑ x_1 ∈ s, ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) (t x_1))
⊢ Ne (α := ℝ≥0∞) (∑ i ∈ s, (μ : (a : Set α) → ℝ≥0∞) (t i)) ∞

Tactic:
exact (ENNReal.sum_lt_top.mpr (fun i hi ↦ measure_lt_top ..)).ne

Premises used: Iff.mpr, MeasureTheory.measure_lt_top, ENNReal.sum_lt_top, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
apply :
  (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ (s ∩ t).Nonempty

Tactic:
apply nonempty_inter_of_measure_lt_add μ ht h's h't ?_

Premises used: MeasureTheory.nonempty_inter_of_measure_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
apply :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal
apply₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≠ ∞
⊢ (μ : (a : Set α) → ℝ≥0∞) u <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
apply (ENNReal.toReal_lt_toReal hu _).1

Premises used: ENNReal.toReal_lt_toReal, Iff.mp
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
rw :
  ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    (HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)).toReal

Tactic:
rw [ENNReal.toReal_add (measure_ne_top_of_subset h's hu) (measure_ne_top_of_subset h't hu)]

Premises used: ENNReal.toReal_add, MeasureTheory.measure_ne_top_of_subset
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
h

Premises used: MeasureTheory.Measure.real
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) u) <
    ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) s) + ENNReal.toReal ((μ : (a : Set α) → ℝ≥0∞) t)

Tactic:
exact h
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≠ ∞

Tactic:
ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.measure_ne_top_of_subset, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
ht : MeasurableSet t
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≠ ∞

Tactic:
exact ENNReal.add_ne_top.2 ⟨measure_ne_top_of_subset h's hu, measure_ne_top_of_subset h't hu⟩

Premises used: Iff.mpr, And.intro, MeasureTheory.measure_ne_top_of_subset, ENNReal.add_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.real u < μ.real t + μ.real s

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real s + μ.real t
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
h₁ : μ.real u < μ.real t + μ.real s
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [add_comm] at h

Premises used: add_comm
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : (t ∩ s).Nonempty
⊢ (s ∩ t).Nonempty

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (t ∩ s).Nonempty

Tactic:
nonempty_inter_of_measureReal_lt_add hs h't h's h hu

Premises used: MeasureTheory.nonempty_inter_of_measureReal_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s t u : Set α
hs : MeasurableSet s
h's : s ⊆ u
h't : t ⊆ u
h : μ.real u < μ.real t + μ.real s
hu : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) u : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ (t ∩ s).Nonempty

Tactic:
exact nonempty_inter_of_measureReal_lt_add hs h't h's h hu

Premises used: MeasureTheory.nonempty_inter_of_measureReal_lt_add
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
h : NullMeasurableSet s μ
rw : μ.real univ - μ.real s = 1 - μ.real s
rw₁ rw₂ : 1 - μ.real s = 1 - μ.real s
⊢ μ.real sᶜ = 1 - μ.real s

Tactic:
rw [measureReal_compl₀ h, probReal_univ]

Premises used: MeasureTheory.measureReal_compl₀, MeasureTheory.probReal_univ
-- Module: Mathlib.MeasureTheory.Measure.Real
Goal:
α : Type u_1
x : MeasurableSpace α
μ : Measure α
s : Set α
inst : IsProbabilityMeasure μ
hs : MeasurableSet s
⊢ μ.real sᶜ = 1 - μ.real s

Tactic:
probReal_compl_eq_one_sub₀ hs.nullMeasurableSet

Premises used: MeasureTheory.probReal_compl_eq_one_sub₀, MeasurableSet.nullMeasurableSet
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)

Premises used: iSup₂_le, MeasureTheory.OuterMeasure.mono, le_of_forall_lt, MeasureTheory.Measure.toOuterMeasure, le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
le_antisymm :
  ∀ (r : ℝ≥0∞) (hr : r < (μ : (a : Set α) → ℝ≥0∞) U),
    r < ⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞)

Tactic:
refine
    le_antisymm (le_of_forall_lt fun r hr => ?_) (iSup₂_le fun K hK => iSup_le fun _ => μ.mono hK)

Premises used: iSup₂_le, MeasureTheory.OuterMeasure.mono, le_of_forall_lt, MeasureTheory.Measure.toOuterMeasure, le_antisymm, iSup_le
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
H : μ.InnerRegularWRT p q
hU : q U
r : ℝ≥0∞
hr : r < (μ : (a : Set α) → ℝ≥0∞) U
⊢ r < ⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K

Tactic:
simpa only [lt_iSup_iff, exists_prop] using H hU r hr

Premises used: exists_prop, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
rw :
  Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (ν : (a : Set α) → ℝ≥0∞) K)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)

Tactic:
rw [hμ.measure_eq_iSup hU, hν.measure_eq_iSup hU]

Premises used: MeasureTheory.Measure.InnerRegularWRT.measure_eq_iSup
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
h : ∀ t ⊆ U, ∀ (ht2 : p t), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (μ : (a : Set α) → ℝ≥0∞) K)
    (⨆ (K : Set α), ⨆ (_ : K ⊆ U), ⨆ (_ : p K), (ν : (a : Set α) → ℝ≥0∞) K)

Tactic:
congr! 4 with t _ ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
t : Set α
h : t ⊆ U
ht2 : p t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
hμν t ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
ν : Measure α
hμ : μ.InnerRegularWRT p q
hν : ν.InnerRegularWRT p q
hμν : ∀ (U : Set α), p U → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞)
U : Set α
hU : q U
t : Set α
h : t ⊆ U
ht2 : p t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact hμν t ht2
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
inl :
  ∀ (h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
inr :
  ∀ (h₀ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
rcases eq_or_ne (μ U) 0 with h₀ | h₀

Premises used: eq_or_ne, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
⟨∅, empty_subset _, h0, ?_⟩

Premises used: And.intro, Set.empty_subset, Exists.intro, EmptyCollection.emptyCollection
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
inl : (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε
⊢ ∃ K ⊆ U, p K ∧ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ε

Tactic:
refine ⟨∅, empty_subset _, h0, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Regular
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p q : Set α → Prop
U : Set α
ε : ℝ≥0∞
H : μ.InnerRegularWRT p q
h0 : p ∅
hU : q U
hμU : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
hε : ε ≠ 0
h₀ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (0 : ℝ≥0∞)
inl : (μ : (a : Set α) → ℝ≥0∞) U < 0 + ε
inl₁ : 0 < 0 + ε
inl₂ : 0 < ε
inl₃ inl₄ inl₅ inl₆ : ε ≠ 0
⊢ (μ : (a : Set α) → ℝ≥0∞) U < HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ε

Tactic:
rwa [measure_empty, h₀, zero_add, pos_iff_ne_zero]

Premises used: MeasureTheory.measure_empty, zero_add, pos_iff_ne_zero