awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq (α := Set α) univ {i}
have e_s : ∀ (j : α), Membership.mem (γ := Set α) univ j ↔ Membership.mem (γ := Set α) {i} j
Tactic: ext j
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq (α := Measure α) count (dirac i)
have calc : Eq.{u_1 + 1} (α := Measure α) count (restrict count univ)
Tactic: calc count
      = count.restrict univ := by simp
    _ = count.restrict {i} := by congr; ext j; simp [Subsingleton.elim j i]
    _ = dirac i := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
calc : Eq.{u_1 + 1} (α := Measure α) count (restrict count univ)
⊢ Eq (α := Measure α) count (dirac i)
have calc₁ : Eq (α := Measure α) (restrict count univ) (restrict count {i})
Tactic: calc count
      = count.restrict univ := by simp
    _ = count.restrict {i} := by congr; ext j; simp [Subsingleton.elim j i]
    _ = dirac i := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
calc : Eq.{u_1 + 1} (α := Measure α) count (restrict count univ)
calc₁ : Eq (α := Measure α) (restrict count univ) (restrict count {i})
⊢ Eq (α := Measure α) count (dirac i)
have calc₂ : Eq (α := Measure α) (restrict count {i}) (dirac i)
Tactic: calc count
      = count.restrict univ := by simp
    _ = count.restrict {i} := by congr; ext j; simp [Subsingleton.elim j i]
    _ = dirac i := by simp
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
⊢ LE.le (α := Measure β) (map f count) count
have refine : ∀ (s : Set β) (hs : MeasurableSet s),
  s.Nonempty →
    LE.le (α := ℝ≥0∞) (((map f count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_intro fun s hs _ ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
h : s.Nonempty
⊢ LE.le (α := ℝ≥0∞) (((map f count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have rw : (↑(f '' f ⁻¹' s).encard : ℝ≥0∞) ≤ (↑s.encard : ℝ≥0∞)
Tactic: rw [map_apply h2f hs, count_apply (hs.preimage h2f), count_apply hs, ← hf.encard_image]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : α → β
hf : Function.Injective f
h2f : Measurable f
s : Set β
hs : MeasurableSet s
h : s.Nonempty
⊢ (↑(f '' f ⁻¹' s).encard : ℝ≥0∞) ≤ (↑s.encard : ℝ≥0∞)
have this : f '' f ⁻¹' s ⊆ s
Tactic: have := image_preimage_subset f s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
⊢ MeasurableSet.{u_1} (α := α)
    (if h :
        ∃ (s : Set α),
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) then
      h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
    else ∅)
have pos : ∀
  (h :
    ∃ (s : Set α),
      MeasurableSet s ∧
        SigmaFinite (μ.restrict s) ∧
          ∀ t ⊆ sᶜ,
            Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  MeasurableSet
    (h.choose (p := fun (s : Set α) ↦
      MeasurableSet s ∧
        SigmaFinite (μ.restrict s) ∧
          ∀ t ⊆ sᶜ,
            Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
pos :
  ∀
    (h :
      ∃ (s : Set α),
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    MeasurableSet
      (h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))
⊢ MeasurableSet.{u_1} (α := α)
    (if h :
        ∃ (s : Set α),
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) then
      h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
    else ∅)
have neg : ∀
  (h :
    ¬∃ (s : Set α),
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  MeasurableSet.{u_1} (α := α) ∅
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
⊢ SigmaFinite
    (μ.restrict
      (if h :
          ∃ (s : Set α),
            MeasurableSet s ∧
              SigmaFinite (μ.restrict s) ∧
                ∀ t ⊆ sᶜ,
                  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) then
        h.choose (p := fun (s : Set α) ↦
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
      else ∅))
have pos : ∀
  (h :
    ∃ (s : Set α),
      MeasurableSet s ∧
        SigmaFinite (μ.restrict s) ∧
          ∀ t ⊆ sᶜ,
            Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  SigmaFinite
    (μ.restrict
      (h.choose (p := fun (s : Set α) ↦
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))))
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
pos :
  ∀
    (h :
      ∃ (s : Set α),
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
    SigmaFinite
      (μ.restrict
        (h.choose (p := fun (s : Set α) ↦
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))))
⊢ SigmaFinite
    (μ.restrict
      (if h :
          ∃ (s : Set α),
            MeasurableSet s ∧
              SigmaFinite (μ.restrict s) ∧
                ∀ t ⊆ sᶜ,
                  Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) then
        h.choose (p := fun (s : Set α) ↦
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
      else ∅))
have neg : ∀
  (h :
    ¬∃ (s : Set α),
        MeasurableSet s ∧
          SigmaFinite (μ.restrict s) ∧
            ∀ t ⊆ sᶜ,
              Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  SigmaFinite (μ.restrict ∅)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s t : Set α
h :
  ¬∃ (s : Set α),
      MeasurableSet s ∧
        SigmaFinite (μ.restrict s) ∧
          ∀ t ⊆ sᶜ,
            Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
              Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ SigmaFinite (μ.restrict ∅)
have neg : SigmaFinite.{u_1} (α := α) (m0 := mα) 0
Tactic: rw [Measure.restrict_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have pos : ∀
  (hC_lt :
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
      ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s),
  ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
Tactic: by_cases! hC_lt : 1 / n < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
pos :
  ∀
    (hC_lt :
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
        ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s),
    ∃ (t : Set α),
      MeasurableSet t ∧
        SigmaFinite (μ.restrict t) ∧
          (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
              HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
            (ν : (a : Set α) → ℝ≥0∞) t
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have neg : ∀
  (hC_lt :
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)),
  ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
Tactic: by_cases! hC_lt : 1 / n < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
have refine : LE.le (α := ℝ≥0∞)
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine (?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
have refine : ∀ (s : Set α),
  LE.le (α := ℝ≥0∞) (⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞)
Tactic: refine iSup_le (fun s ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have h_lt_top : LT.lt (α := ℝ≥0∞)
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
Tactic: have h_lt_top : ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s < ∞ := by
      refine (?_ : ⨆ (s) (_ : MeasurableSet s)
        (_ : SigmaFinite (μ.restrict s)), ν s ≤ ν Set.univ).trans_lt (measure_lt_top _ _)
      refine iSup_le (fun s ↦ ?_)
      exact iSup_le (fun _ ↦ iSup_le (fun _ ↦ measure_mono (Set.subset_univ s)))
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have pos : ∀ (t : Set α)
  (ht :
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
      ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t),
  ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
Tactic: obtain ⟨t, ht⟩ := exists_lt_of_lt_ciSup
      (ENNReal.sub_lt_self h_lt_top.ne hC_lt.ne_bot (by simp) :
          (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s) - 1 / n
        < ⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
⊢ MeasurableSet t
have by_contra : ∀ (h_notMem : ¬MeasurableSet t), False
Tactic: by_contra h_notMem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
h_notMem : ¬MeasurableSet t
⊢ False
have ht₁ : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
  ⨆ (_ : False), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
Tactic: simp only [h_notMem] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have ht_meas : MeasurableSet t
Tactic: have ht_meas : MeasurableSet t := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
ht_meas : MeasurableSet t
⊢ SigmaFinite (μ.restrict t)
have by_contra : ∀ (h_notMem : ¬SigmaFinite (μ.restrict t)), False
Tactic: by_contra h_notMem
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
ht_meas : MeasurableSet t
h_notMem : ¬SigmaFinite (μ.restrict t)
⊢ False
have ht₁ : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
  ⨆ (_ : MeasurableSet t), ⨆ (_ : False), (ν : (a : Set α) → ℝ≥0∞) t
Tactic: simp only [h_notMem] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
ht_meas : MeasurableSet t
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have ht_mem : SigmaFinite (μ.restrict t)
Tactic: have ht_mem : SigmaFinite (μ.restrict t) := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
h_lt_top :
  LT.lt (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) ∞
t : Set α
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    ⨆ (_ : MeasurableSet t), ⨆ (_ : SigmaFinite (μ.restrict t)), (ν : (a : Set α) → ℝ≥0∞) t
ht_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
⊢ ∃ (t : Set α),
    MeasurableSet t ∧
      SigmaFinite (μ.restrict t) ∧
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
            HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
          (ν : (a : Set α) → ℝ≥0∞) t
have pos : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
  (ν : (a : Set α) → ℝ≥0∞) t
Tactic: refine ⟨t, ht_meas, ht_mem, ?_⟩