awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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
⊢ HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
      (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
    (μ : (a : Set α) → ℝ≥0∞) u
have hm : ∀ {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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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)) ≤
    (μ : (a : Set α) → ℝ≥0∞) u
have 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∞)
Tactic: rw [← measure_inter_add_diff u hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [sInf_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 m : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((sInf (toOuterMeasure '' m) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [sInf_apply hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
  (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: refine (measure_iUnion_le _).antisymm ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have rw : LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i)) ∞
Tactic: rw [OuterMeasure.top_apply hne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ LE.le (α := ℝ≥0∞) (∑' (i : ℕ), ((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)
    (((⊤ : OuterMeasure α) : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
⊢ 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∞)
have 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∞)})
Tactic: rw [← sInf_pair, Measure.sInf_apply hs, OuterMeasure.sInf_apply
    (image_nonempty.2 <| insert_nonempty μ {ν})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)})
have 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
Tactic: refine le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ 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∞)})
have 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))
Tactic: refine le_antisymm (le_sInf fun m ⟨t, ht₁⟩ ↦ ?_) (le_iInf₂ fun t' ht' ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ ⨅ (t : ℕ → Set α),
      ⨅ (_ : s ⊆ iUnion t),
        ∑' (n : ℕ),
          ⨅ (μ_1 : OuterMeasure α),
            ⨅ (_ : Membership.mem (γ := Set (OuterMeasure α)) (image (α := Measure α) toOuterMeasure {μ, ν}) μ_1),
              (μ_1 : (a : Set α) → ℝ≥0∞) (t n) ≤
    m
have 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∞)
Tactic: subst ht₁
Cleared hypotheses: m, h, ht₁
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
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 α),
      ⨅ (_ : 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∞)
have ht' : 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'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
have refine_1 : ∀ (x : α) (hx : x ∈ s), x ∈ iUnion t'
Tactic: refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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'
⊢ ⨅ (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∞)
have 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∞)
Tactic: refine (iInf₂_le t' fun x hx ↦ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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
⊢ x ∈ iUnion t'
have pos : ∀ (hxt : x ∈ t), x ∈ iUnion t'
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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'
⊢ x ∈ iUnion t'
have neg : ∀ (hxt : x ∉ t), x ∈ iUnion t'
Tactic: by_cases hxt : x ∈ t
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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'
have pos : x ∈ if Eq (α := ℕ) 0 0 then t ∩ s else if Eq (α := ℕ) 0 1 then tᶜ ∩ s else ∅
Tactic: refine mem_iUnion.2 ⟨0, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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'
have neg : x ∈ if Eq (α := ℕ) 1 0 then t ∩ s else if Eq (α := ℕ) 1 1 then tᶜ ∩ s else ∅
Tactic: refine mem_iUnion.2 ⟨1, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ℕ),
      ⨅ (μ_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∞)
have 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∞)
Tactic: simp only [iInf_image, coe_toOuterMeasure, iInf_pair]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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 : ℕ), 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
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∞)
⊢ ∑' (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∞)
have 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∞)
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]