awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
refine_1 :
  ∀ (m : ℝ≥0∞),
    Membership.mem (γ := Set ℝ≥0∞)
        {m : ℝ≥0∞ |
          ∃ (t : Set α),
            m =
              HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)}
        m →
      ∀ (t : Set α)
        (ht₁ :
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)),
        ⨅ (t : ℕ → Set α),
            ⨅ (_ : s ⊆ iUnion t),
              ∑' (n : ℕ),
                ⨅ (μ_1 : OuterMeasure α),
                  ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
                    (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
          m
refine_2 :
  ∀ (t' : ℕ → Set α) (ht' : s ⊆ iUnion t'),
    LE.le (α := ℝ≥0∞)
      (sInf
        {m : ℝ≥0∞ |
          ∃ (t : Set α),
            m =
              HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
                ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)})
      (∑' (n : ℕ),
        ⨅ (μ_1 : OuterMeasure α),
          ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
            (μ_1 : (a : Set α) → ℝ≥0∞) (t' n))
⊢ 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:
refine le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
m : ℝ≥0∞
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
            ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)}
    m
t : Set α
ht₁ :
  m =
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
refine_1 :
  Membership.mem (γ := Set ℝ≥0∞)
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            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∞) (tᶜ ∩ s) : ℝ≥0∞)) →
    ⨅ (t : ℕ → Set α),
        ⨅ (_ : s ⊆ iUnion t),
          ∑' (n : ℕ),
            ⨅ (μ_1 : OuterMeasure α),
              ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
                (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
        ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
⊢ ⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
    m

Tactic:
subst ht₁
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
⊢ let t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅;
  t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅

Tactic:
set t' : ℕ → Set α := fun n ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅ with ht'

Premises used: Compl.compl, Inter.inter, EmptyCollection.emptyCollection, OfNat.ofNat, Eq, ite
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ ⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
(iInf₂_le t' fun x hx ↦ ?_).trans ?_

Premises used: iInf₂_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
refine_1 : ∀ (x : α) (hx : x ∈ s), x ∈ iUnion t'
refine_1₁ :
  ∑' (n : ℕ),
      ⨅ (μ_1 : OuterMeasure α),
        ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
          (μ_1 : (a : Set α) → ℝ≥0∞) (t' n) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
⊢ ⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_

Premises used: iInf₂_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
pos : ∀ (hxt : x ∈ t), x ∈ iUnion t'
neg : ∀ (hxt : x ∉ t), x ∈ iUnion t'
⊢ x ∈ iUnion t'

Tactic:
by_cases hxt : x ∈ t
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ iUnion t'

Tactic:
mem_iUnion.2 ⟨0, ?_⟩

Premises used: Iff.mpr, Set.Mem, Set.mem_iUnion, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
pos : x ∈ if Eq (α := ℕ) 0 0 then t ∩ s else if Eq (α := ℕ) 0 1 then tᶜ ∩ s else ∅
⊢ x ∈ iUnion t'

Tactic:
refine mem_iUnion.2 ⟨0, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∈ t
⊢ x ∈ if Eq (α := ℕ) 0 0 then t ∩ s else if Eq (α := ℕ) 0 1 then tᶜ ∩ s else ∅

Tactic:
simp [hx, hxt]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ iUnion t'

Tactic:
mem_iUnion.2 ⟨1, ?_⟩

Premises used: Iff.mpr, Set.Mem, Set.mem_iUnion, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
neg : x ∈ if Eq (α := ℕ) 1 0 then t ∩ s else if Eq (α := ℕ) 1 1 then tᶜ ∩ s else ∅
⊢ x ∈ iUnion t'

Tactic:
refine mem_iUnion.2 ⟨1, ?_⟩

Premises used: Iff.mpr, Set.mem_iUnion, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
x : α
hx : x ∈ s
hxt : x ∉ t
⊢ x ∈ if Eq (α := ℕ) 1 0 then t ∩ s else if Eq (α := ℕ) 1 1 then tᶜ ∩ s else ∅

Tactic:
simp [hx, hxt]
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
refine_1 :
  ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
⊢ ∑' (n : ℕ),
      ⨅ (μ_1 : OuterMeasure α),
        ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
          (μ_1 : (a : Set α) → ℝ≥0∞) (t' n) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
simp only [iInf_image, coe_toOuterMeasure, iInf_pair]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, iInf_image, iInf_pair
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
refine_1 :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (min ((μ : (a : Set α) → ℝ≥0∞) (t' 0)) ((ν : (a : Set α) → ℝ≥0∞) (t' 0)) : ℝ≥0∞)
      (min ((μ : (a : Set α) → ℝ≥0∞) (t' 1)) ((ν : (a : Set α) → ℝ≥0∞) (t' 1)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
rw :
  ∀ (x : ℕ),
    Eq (α := ℝ≥0∞)
      (if x = 1 then 0
        else if x = 0 then 0 else min ((μ : (a : Set α) → ℝ≥0∞) (t' x)) ((ν : (a : Set α) → ℝ≥0∞) (t' x)) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)
⊢ ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n)) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
rw [tsum_eq_add_tsum_ite 0, tsum_eq_add_tsum_ite 1, if_neg zero_ne_one.symm,
        ENNReal.summable.tsum_eq_zero_iff.2 _, add_zero]

Premises used: Iff.mpr, zero_ne_one, ENNReal.summable, Ne.symm, Summable.tsum_eq_zero_iff, add_zero, OfNat.ofNat, if_neg, ENNReal.tsum_eq_add_tsum_ite
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' 0) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)

Tactic:
simp [ht']
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' 1) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
simp [ht']
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (min ((μ : (a : Set α) → ℝ≥0∞) (t' 0)) ((ν : (a : Set α) → ℝ≥0∞) (t' 0)) : ℝ≥0∞)
      (min ((μ : (a : Set α) → ℝ≥0∞) (t' 1)) ((ν : (a : Set α) → ℝ≥0∞) (t' 1)) : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)

Tactic:
exact add_le_add (inf_le_left.trans <| by simp [ht']) (inf_le_right.trans <| by simp [ht'])

Premises used: add_le_add, inf_le_right, inf_le_left, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
simp :
  ∀ (x : ℕ),
    ¬x = 1 →
      ¬x = 0 →
        Eq (α := ℝ≥0∞) (min ((μ : (a : Set α) → ℝ≥0∞) (t' x)) ((ν : (a : Set α) → ℝ≥0∞) (t' x)) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∀ (x : ℕ),
    Eq (α := ℝ≥0∞)
      (if x = 1 then 0
        else if x = 0 then 0 else min ((μ : (a : Set α) → ℝ≥0∞) (t' x)) ((ν : (a : Set α) → ℝ≥0∞) (t' x)) :
        ℝ≥0∞)
      (0 : ℝ≥0∞)

Tactic:
simp only [ite_eq_left_iff]

Premises used: ite_eq_left_iff
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t : Set α
h :
  Membership.mem (γ := Set ℝ≥0∞)
    {m : ℝ≥0∞ |
      ∃ (t : Set α),
        m =
          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∞) (tᶜ ∩ s) : ℝ≥0∞))
t' : ℕ → Set α := fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
ht' : t' = fun (n : ℕ) ↦ if n = 0 then t ∩ s else if n = 1 then tᶜ ∩ s else ∅
n : ℕ
hn₁ : ¬n = 1
hn₀ : ¬n = 0
⊢ Eq (α := ℝ≥0∞) (min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n)) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [ht', if_neg hn₀, if_neg hn₁, measure_empty, le_refl, inf_of_le_left]

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

Tactic:
simp only [iInf_image, coe_toOuterMeasure, iInf_pair]

Premises used: MeasureTheory.Measure.coe_toOuterMeasure, iInf_image, iInf_pair
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
⊢ let t : Set α :=
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n;
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n

Tactic:
set t := ⋃ n ∈ {k : ℕ | μ (t' k) ≤ ν (t' k)}, t' n with ht
-- Module: Mathlib.MeasureTheory.Measure.MeasureSpace
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hadd :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞) ≤
    ∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n))
⊢ LE.le (α := ℝ≥0∞)
    (sInf
      {m : ℝ≥0∞ |
        ∃ (t : Set α),
          m =
            HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
              ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)})
    (∑' (n : ℕ), min ((μ : (a : Set α) → ℝ≥0∞) (t' n)) ((ν : (a : Set α) → ℝ≥0∞) (t' n)))

Tactic:
le_trans (sInf_le ⟨t, rfl⟩) hadd

Premises used: sInf_le, Exists.intro, rfl, le_trans