awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))
⊢ MeasurableSet.{u_1} (α := α)
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have pos₁ : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  MeasurableSet
    (h's.choose (p := fun (t : Set α) ↦
      t ⊇ s ∧
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)))
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    MeasurableSet (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s))
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    MeasurableSet
      (h's.choose (p := fun (t : Set α) ↦
        t ⊇ s ∧
          MeasurableSet t ∧
            ∀ (u : Set α),
              MeasurableSet u →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)))
⊢ MeasurableSet.{u_1} (α := α)
    (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
      h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
    else
      if h' :
          ∃ t ⊇ s,
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                    ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
        h'.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
      else
        ⋯.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
have neg : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ¬∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  MeasurableSet
    (sorry.choose (p := fun (t : Set α) ↦
      s ⊆ t ∧ MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)))
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable μ s) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
        h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
      else
        if h' :
            ∃ t ⊇ s,
              MeasurableSet t ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
          h'.choose (p := fun (t : Set α) ↦
            t ⊇ s ∧
              MeasurableSet t ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
        else
          sorry.choose (p := fun (t : Set α) ↦
            s ⊆ t ∧
              MeasurableSet t ∧
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
    ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [toMeasurable_def]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
          h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
        else
          if h' :
              ∃ t ⊇ s,
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
            h'.choose (p := fun (t : Set α) ↦
              t ⊇ s ∧
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
          else
            ⋯.choose (p := fun (t : Set α) ↦
              s ⊆ t ∧
                MeasurableSet t ∧
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
          h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
        else
          if h' :
              ∃ t ⊇ s,
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
            h'.choose (p := fun (t : Set α) ↦
              t ⊇ s ∧
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
          else
            ⋯.choose (p := fun (t : Set α) ↦
              s ⊆ t ∧
                MeasurableSet t ∧
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have pos₁ : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ∃ t ⊇ s,
      MeasurableSet t ∧
        ∀ (u : Set α),
          MeasurableSet u →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (h's.choose (p := fun (t : Set α) ↦
          t ⊇ s ∧
            MeasurableSet t ∧
              ∀ (u : Set α),
                MeasurableSet u →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
s : Set α
pos :
  ∀ (hs : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (hs.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
pos₁ :
  ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
    (h's :
      ∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
    Eq (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (h's.choose (p := fun (t : Set α) ↦
            t ⊇ s ∧
              MeasurableSet t ∧
                ∀ (u : Set α),
                  MeasurableSet u →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                      ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))) :
        ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (if h : ∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s then
          h.choose (p := fun (t : Set α) ↦ t ⊇ s ∧ MeasurableSet t ∧ t =ᶠ[ae μ] s)
        else
          if h' :
              ∃ t ⊇ s,
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞) then
            h'.choose (p := fun (t : Set α) ↦
              t ⊇ s ∧
                MeasurableSet t ∧
                  ∀ (u : Set α),
                    MeasurableSet u →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
                        ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞))
          else
            ⋯.choose (p := fun (t : Set α) ↦
              s ⊆ t ∧
                MeasurableSet t ∧
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (hs : ¬∃ t ⊇ s, MeasurableSet t ∧ t =ᶠ[ae μ] s)
  (h's :
    ¬∃ t ⊇ s,
        MeasurableSet t ∧
          ∀ (u : Set α),
            MeasurableSet u →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ u) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (sorry.choose (p := fun (t : Set α) ↦
          s ⊆ t ∧
            MeasurableSet t ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞))) :
      ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: split_ifs with hs h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
g : α → (a : δ) → X a
hg : AEMeasurable g μ
a : δ
⊢ AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
have right : EventuallyEq.{u_1, u_7} (β := X a) (ae μ) (fun (x : α) ↦ g x a) fun (x : α) ↦ mk g hg x a
Tactic: use fun x ↦ hg.mk g x a, hg.measurable_mk.eval
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
have mp : AEMeasurable g μ → ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
mp : AEMeasurable g μ → ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
⊢ AEMeasurable g μ ↔ ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
have mpr : (∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ) → AEMeasurable g μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpaceDef (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
δ : Type u_6
X : δ → Type u_7
mX : (a : δ) → MeasurableSpace (X a)
inst : Countable δ
g : α → (a : δ) → X a
h : ∀ (a : δ), AEMeasurable.{u_1, u_7} (β := X a) (fun (x : α) ↦ g x a) μ
⊢ AEMeasurable g μ
have right : g =ᶠ[ae μ] fun (x : α) (a : δ) ↦ AEMeasurable.mk (fun (x : α) ↦ g x a) sorry x
Tactic: use fun x a ↦ (h a).mk _ x, measurable_pi_lambda _ fun a ↦ (h a).measurable_mk
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
⊢ Continuous (Y := ℝ≥0∞) fun (s : MeasuredSets μ) ↦ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α)
have refine : ∀ (s t : MeasuredSets μ),
  (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) (1 * edist s t)
Tactic: refine continuous_of_le_add_edist 1 ENNReal.one_ne_top fun s t ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
s t : MeasuredSets μ
⊢ (μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) ≤
    HAdd.hAdd (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) (1 * edist s t)
have rw : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞) ≤
  edist s t
Tactic: rw [one_mul, ← tsub_le_iff_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
⊢ μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤ dist s t
have grw : μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤
  (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)).toReal
Tactic: grw [dist_edist, ← sub_le_edist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
s t : MeasuredSets μ
grw :
  μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤
    (HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞)
        ((μ : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)).toReal
⊢ μ.real (↑s : Set α) - μ.real (↑t : Set α) ≤ dist s t
have h₂ : Ne (α := ℝ≥0∞) (edist s t) ∞
Tactic: grw [dist_edist, ← sub_le_edist]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε
Tactic: apply MeasurableSpace.induction_on_inter (C := fun s hs ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ t ∈ C, μ (t ∆ s) < ε) h hC.isSetSemiring.isPiSystem ?_ ?_ ?_ ?_ s hs ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply₁ : ∀ (t : Set α) (ht : t ∈ C),
  (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε) t
    sorry
Tactic: apply MeasurableSpace.induction_on_inter (C := fun s hs ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ t ∈ C, μ (t ∆ s) < ε) h hC.isSetSemiring.isPiSystem ?_ ?_ ?_ ?_ s hs ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε
apply₁ :
  ∀ (t : Set α) (ht : t ∈ C),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      t ⋯
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply₂ : ∀ (t : Set α) (htm : MeasurableSet t),
  (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε) t
      htm →
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      tᶜ sorry
Tactic: apply MeasurableSpace.induction_on_inter (C := fun s hs ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ t ∈ C, μ (t ∆ s) < ε) h hC.isSetSemiring.isPiSystem ?_ ?_ ?_ ?_ s hs ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s : Set α
hs : MeasurableSet s
ε : ℝ≥0∞
hε : 0 < ε
apply : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ ∅) < ε
apply₁ :
  ∀ (t : Set α) (ht : t ∈ C),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
      t ⋯
apply₂ :
  ∀ (t : Set α) (htm : MeasurableSet t),
    (fun (s : Set α) (hs : MeasurableSet s) ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
        t htm →
      (fun (s : Set α) (hs : MeasurableSet s) ↦
          ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
        tᶜ ⋯
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
have apply₃ : ∀ (f : ℕ → Set α),
  Pairwise (Function.onFun Disjoint f) →
    ∀ (hfm : ∀ (i : ℕ), MeasurableSet (f i)),
      (∀ (i : ℕ),
          (fun (s : Set α) (hs : MeasurableSet s) ↦
              ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
            (f i) sorry) →
        (fun (s : Set α) (hs : MeasurableSet s) ↦
            ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε)
          (⋃ (i : ℕ), f i) sorry
Tactic: apply MeasurableSpace.induction_on_inter (C := fun s hs ↦ ∀ (ε : ℝ≥0∞) (hε : 0 < ε),
    ∃ t ∈ C, μ (t ∆ s) < ε) h hC.isSetSemiring.isPiSystem ?_ ?_ ?_ ?_ s hs ε hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
⊢ ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
have obtain : ∀ (t : Set α) (tC : t ∈ C) (ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2),
  ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ sᶜ) < ε
Tactic: obtain ⟨t, tC, ht⟩ : ∃ t ∈ C, μ (t ∆ s) < ε / 2 := h's _ (ENNReal.half_pos εpos.ne')
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h'C : ∃ (D : Set (Set α)), D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty
have rcases : ∀ (D : Set (Set α)) (D_count : D.Countable) (DC : D ⊆ C)
  (hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ (D : Set (Set α)),
    D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty
Tactic: rcases h'C with ⟨D, D_count, DC, hD⟩
Cleared hypotheses: h'C
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ (D : Set (Set α)),
    D.Countable ∧ D ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ D.Nonempty
have refine : D ∪ {∅} ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty
Tactic: refine ⟨D ∪ {∅}, D_count.union (by simp), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasuredSets (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hC : IsSetRing C
h : mα = generateFrom C
s_1 : Set α
hs_1 : MeasurableSet s_1
ε_1 : ℝ≥0∞
hε : 0 < ε_1
s : Set α
hs : MeasurableSet s
h's : ∀ (ε : ℝ≥0∞) (hε : 0 < ε), ∃ t ∈ C, (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε
ε : ℝ≥0∞
εpos : 0 < ε
t : Set α
tC : t ∈ C
ht : (μ : (a : Set α) → ℝ≥0∞) (t ∆ s) < ε / 2
D : Set (Set α)
D_count : D.Countable
DC : D ⊆ C
hD : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ D)ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ D ∪ {∅} ⊆ C ∧ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty
have simp : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃₀ (D ∪ {∅}))ᶜ : ℝ≥0∞) (0 : ℝ≥0∞) ∧ (D ∪ {∅}).Nonempty
Tactic: simp only [union_subset_iff, DC, singleton_subset_iff, true_and, and_true, hC.empty_mem]