awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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∞)
rw :
  ∀ (ht : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable (ν + μ) t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
rw [add_comm] at ht ⊢

Premises used: add_comm
-- 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_toMeasurable_add_inter_left hs ht

Premises used: MeasureTheory.Measure.measure_toMeasurable_add_inter_left
-- 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:
exact measure_toMeasurable_add_inter_left hs ht

Premises used: MeasureTheory.Measure.measure_toMeasurable_add_inter_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁ ≤ μ₂ ↔
    ∀ (s : Set α),
      MeasurableSet s → LE.le (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
outerMeasure_le_iff

Premises used: MeasureTheory.Measure.outerMeasure_le_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h :
  ∀ (s : Set α),
    MeasurableSet s →
      s.Nonempty → LE.le (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
hs : MeasurableSet.{u_1} (α := α) ∅
⊢ LE.le (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ μ₁ ≤ μ₂ ↔ ∀ (s : Set α), LE.le (α := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ₂ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ≤ ν
s : Set α
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
h s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h₁ : μ ≤ ν
h₂ : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
(h₁ s).trans (measure_mono h₂)

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ¬ν ≤ μ ↔
    ∃ (s : Set α),
      MeasurableSet s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [le_iff, not_forall, not_le, exists_prop]

Premises used: not_le, exists_prop, MeasureTheory.Measure.le_iff, Classical.not_forall
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
⊢ ¬ν ≤ μ ↔ ∃ (s : Set α), LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [le_iff', not_forall, not_le]

Premises used: not_le, MeasureTheory.Measure.le_iff', Classical.not_forall
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν ν' : Measure α
h : μ ≤ ν
⊢ μ ≤ ν' + ν

Tactic:
fun s => le_add_left (h s)

Premises used: WithTop.map₂, Option.map₂, le_add_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν ν' : Measure α
h : μ ≤ ν
⊢ μ ≤ ν + ν'

Tactic:
fun s => le_add_right (h s)

Premises used: WithTop.map₂, Option.map₂, le_add_right
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
rw : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [OuterMeasure.sInf_eq_boundedBy_sInfGen]

Premises used: MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
OuterMeasure.boundedBy_caratheodory fun t => ?_

Premises used: MeasureTheory.OuterMeasure.boundedBy_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
refine :
  ∀ (t : Set α),
    OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
      OuterMeasure.sInfGen (toOuterMeasure '' m) t
⊢ MeasurableSet s

Tactic:
refine OuterMeasure.boundedBy_caratheodory fun t => ?_

Premises used: MeasureTheory.OuterMeasure.boundedBy_caratheodory
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
simp :
  ∀ ⦃x : Measure α⦄,
    x ∈ m →
      ∀ (i : Set α) (i_1 : t ⊆ i) (i_2 : MeasurableSet i),
        HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
            (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
          (x : (a : Set α) → ℝ≥0∞) i
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t

Tactic:
simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, measure_eq_iInf t,
    coe_toOuterMeasure]

Premises used: MeasureTheory.OuterMeasure.sInfGen, MeasureTheory.Measure.coe_toOuterMeasure, le_iInf_iff, MeasureTheory.measure_eq_iInf, Set.forall_mem_image
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s_1 : Set α
hs : MeasurableSet s_1
t_1 : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t_1 ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
rw : LE.le (α := ℝ≥0∞) (⨅ b ∈ m, (b.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
rw [OuterMeasure.sInfGen_def, iInf_image]

Premises used: iInf_image, MeasureTheory.OuterMeasure.sInfGen_def
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s_1 : Set α
hs : MeasurableSet s_1
t_1 : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t_1 ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) (⨅ b ∈ m, (b.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
iInf₂_le_of_le μ hμ <| measure_mono hst

Premises used: iInf₂_le_of_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s_1 : Set α
hs : MeasurableSet s_1
t_1 : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t_1 ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ LE.le (α := ℝ≥0∞) (⨅ b ∈ m, (b.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)

Tactic:
exact iInf₂_le_of_le μ hμ <| measure_mono hst

Premises used: iInf₂_le_of_le, MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
⊢ ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t

Tactic:
have hm : ∀ {s t}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ μ t := by
    intro s t hst
    rw [OuterMeasure.sInfGen_def, iInf_image]
    exact iInf₂_le_of_le μ hμ <| measure_mono hst
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t
rw :
  HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
      (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
      (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
    (μ : (a : Set α) → ℝ≥0∞) u

Tactic:
rw [← measure_inter_add_diff u hs]

Premises used: MeasureTheory.measure_inter_add_diff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
      (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)

Tactic:
add_le_add (hm <| inter_subset_inter_left _ htu) (hm <| diff_subset_diff_left htu)

Premises used: add_le_add, Set.diff_subset_diff_left, Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t ⊆ u
_hu : MeasurableSet u
hm : ∀ {s t : Set α}, s ⊆ t → OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
      (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (u ∩ s) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (u \ s) : ℝ≥0∞)

Tactic:
exact add_le_add (hm <| inter_subset_inter_left _ htu) (hm <| diff_subset_diff_left htu)

Premises used: add_le_add, Set.diff_subset_diff_left, Set.inter_subset_inter_left
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
s : Set α
m : Set (Measure α)
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
toMeasure_apply _ _ hs

Premises used: MeasureTheory.toMeasure_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
rw : LE.le (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [sInf_apply hs]

Premises used: MeasureTheory.Measure.sInf_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
this s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : μ ∈ m
this : sInf (toOuterMeasure '' m) ≤ μ.toOuterMeasure
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact this s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [sInf_apply hs]

Premises used: MeasureTheory.Measure.sInf_apply
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
this s
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
m : Set (Measure α)
h : ∀ μ' ∈ m, μ ≤ μ'
this : μ.toOuterMeasure ≤ sInf (toOuterMeasure '' m)
s : Set α
hs : MeasurableSet s
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact this 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 γ
μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
_ :
  (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Disjoint on f) →
      Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ (∀ (i : ℕ), MeasurableSet (f i)) →
    Pairwise (Disjoint on f) →
      Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
        (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
_
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
_ :
  Pairwise (Disjoint on f) →
    Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ Pairwise (Disjoint on f) →
    Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
_
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
(measure_iUnion_le _).antisymm ?_

Premises used: LE.le.antisymm, MeasureTheory.measure_iUnion_le
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
refine :
  LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
refine (measure_iUnion_le _).antisymm ?_

Premises used: LE.le.antisymm, MeasureTheory.measure_iUnion_le
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
hne : Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)
rw : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i)) ∞
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
rw [OuterMeasure.top_apply hne]

Premises used: MeasureTheory.OuterMeasure.top_apply
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
hne : Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i)) ∞

Tactic:
le_top

Premises used: le_top
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
hne : Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i)) ∞

Tactic:
exact le_top

Premises used: le_top
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
hne : ¬Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
simp_all [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty
-- 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 α
m : Set (Measure α)
x : MeasurableSpace α
f : ℕ → Set α
h : ∀ (i : ℕ), MeasurableSet (f i)
h_1 : Pairwise (Disjoint on f)
if :
  ∀ (hne : Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)),
    LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
if₁ :
  ∀ (hne : ¬Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)),
    LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
if₂ :
  ∀ (hne : Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)),
    LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
if₃ if₄ :
  ∀ (hne : ¬Set.Nonempty.{u_1} (α := α) (⋃ (i : ℕ), f i)),
    LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
      (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)

Tactic:
if hne : (⋃ i, f i).Nonempty then
            rw [OuterMeasure.top_apply hne]
            exact le_top
          else
            simp_all [Set.not_nonempty_iff_eq_empty]

Premises used: Set.not_nonempty_iff_eq_empty, Set.Nonempty, le_top, Set.iUnion
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
rw :
  Eq (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n))
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)})
⊢ Eq (α := ℝ≥0∞) ((μ ⊓ ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (sInf
        {m : ℝ≥0∞ |
          ∃ (t : Set α),
            m =
              HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)} :
      ℝ≥0∞)

Tactic:
rw [← sInf_pair, Measure.sInf_apply hs, OuterMeasure.sInf_apply
    (image_nonempty.2 <| insert_nonempty μ {ν})]

Premises used: Iff.mpr, Set.image_nonempty, sInf_pair, Set.insert_nonempty, MeasureTheory.Measure.sInf_apply, MeasureTheory.OuterMeasure.sInf_apply, Singleton.singleton
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n))
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)})

Tactic:
le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)

Premises used: iInf, _private.0.MeasureTheory.Measure.inf_apply.match_1, LE.le, le_iInf₂, le_antisymm, tsum, Nat, le_sInf, DFunLike.coe, SummationFilter.unconditional