awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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) ∞
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
⊢ ∃ (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)

Premises used: ENNReal.sub_lt_self, exists_lt_of_lt_ciSup, LT.lt.ne_bot, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
by_contra : ∀ (h_notMem : ¬MeasurableSet t), False
⊢ MeasurableSet t

Tactic:
by_contra h_notMem
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
⊢ (⨆ (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
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 α
h_notMem : ¬MeasurableSet t
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
⊢ False

Tactic:
simp at ht
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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

Tactic:
have ht_meas : MeasurableSet t := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
by_contra : ∀ (h_notMem : ¬SigmaFinite (μ.restrict t)), False
⊢ SigmaFinite (μ.restrict t)

Tactic:
by_contra h_notMem
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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)
⊢ (⨆ (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
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_meas : MeasurableSet t
h_notMem : ¬SigmaFinite (μ.restrict t)
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
⊢ False

Tactic:
simp at ht
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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)

Tactic:
have ht_mem : SigmaFinite (μ.restrict t) := by
      by_contra h_notMem
      simp only [h_notMem] at ht
      simp at ht
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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

Tactic:
⟨t, ht_meas, ht_mem, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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)
pos :
  (⨆ (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

Tactic:
refine ⟨t, ht_meas, ht_mem, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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)
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    (ν : (a : Set α) → ℝ≥0∞) t

Tactic:
simp only [ht_meas, ht_mem, iSup_true] at ht

Premises used: iSup_true
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    (ν : (a : Set α) → ℝ≥0∞) t
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥0∞) t

Tactic:
ht.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_meas : MeasurableSet t
ht_mem : SigmaFinite (μ.restrict t)
ht :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) <
    (ν : (a : Set α) → ℝ≥0∞) t
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥0∞) t

Tactic:
exact ht.le

Premises used: LT.lt.le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
rw : SigmaFinite.{u_1} (α := α) (m0 := mα) 0
⊢ SigmaFinite (μ.restrict ∅)

Tactic:
rw [Measure.restrict_empty]

Premises used: MeasureTheory.Measure.restrict_empty
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
⊢ SigmaFinite.{u_1} (α := α) (m0 := mα) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
neg :
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥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:
refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
neg : LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥0∞) ∅

Tactic:
rw [tsub_eq_zero_of_le hC_lt]

Premises used: tsub_eq_zero_of_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
hC_lt :
  ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s ≤
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ MeasurableSet (μ.sigmaFiniteSetGE ν n)

Tactic:
(exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.1

Premises used: Exists.choose_spec, MeasureTheory.Measure.sigmaFiniteSetGE, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))

Tactic:
(exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.2.1

Premises used: Exists.choose_spec, MeasureTheory.Measure.sigmaFiniteSetGE, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, And.right, And.left
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(le_iSup (f := fun s ↦ _)
    (sigmaFinite_restrict_sigmaFiniteSetGE μ ν n)).trans ?_

Premises used: MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE, le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
refine :
  LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine (le_iSup (f := fun s ↦ _)
    (sigmaFinite_restrict_sigmaFiniteSetGE μ ν n)).trans ?_

Premises used: MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetGE, le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)

Tactic:
le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetGE ν n)
    (measurableSet_sigmaFiniteSetGE n)

Premises used: MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.Measure.sigmaFiniteSetGE, le_iSup₂
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetGE ν n)
    (measurableSet_sigmaFiniteSetGE n)

Premises used: MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.Measure.sigmaFiniteSetGE, le_iSup₂
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
n : ℕ
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n)

Tactic:
(exists_isSigmaFiniteSet_measure_ge μ ν n).choose_spec.2.2

Premises used: Exists.choose_spec, MeasureTheory.Measure.sigmaFiniteSetGE, MeasureTheory.exists_isSigmaFiniteSet_measure_ge, And.right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n)) atTop
    (𝓝 (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s))

Tactic:
tendsto_of_tendsto_of_tendsto_of_le_of_le ?_
    tendsto_const_nhds (measure_sigmaFiniteSetGE_ge μ ν) (measure_sigmaFiniteSetGE_le μ ν)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, MeasureTheory.measure_sigmaFiniteSetGE_le, MeasureTheory.measure_sigmaFiniteSetGE_ge
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
refine :
  Tendsto (β := ℝ≥0∞)
    (fun (i : ℕ) ↦
      (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞))
    atTop (𝓝 (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s))
⊢ Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n)) atTop
    (𝓝 (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s))

Tactic:
refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_
    tendsto_const_nhds (measure_sigmaFiniteSetGE_ge μ ν) (measure_sigmaFiniteSetGE_le μ ν)

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds, MeasureTheory.measure_sigmaFiniteSetGE_le, MeasureTheory.measure_sigmaFiniteSetGE_ge
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
nth_rewrite :
  Tendsto
    (fun (i : ℕ) ↦
      (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞))
    atTop
    (𝓝
      (HSub.hSub (α := ℝ≥0∞)
        (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) 0))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (i : ℕ) ↦
      (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
        HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞))
    atTop (𝓝 (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s))

Tactic:
nth_rewrite 2 [← tsub_zero (⨆ (s) (_ : MeasurableSet s) (_ : SigmaFinite (μ.restrict s)), ν s)]

Premises used: iSup, tsub_zero, DFunLike.coe