awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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
have ht₁ : (⨆ (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
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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 (μ.restrict ∅)
have rw : 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 : ℕ
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
have neg : (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
    HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
  (ν : (a : Set α) → ℝ≥0∞) ∅
Tactic: refine ⟨∅, MeasurableSet.empty, by rw [Measure.restrict_empty]; infer_instance, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s) -
      HDiv.hDiv (α := ℝ≥0∞) 1 (↑n : ℝ≥0∞) ≤
    (ν : (a : Set α) → ℝ≥0∞) ∅
have neg : LE.le (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: rw [tsub_eq_zero_of_le hC_lt]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
have refine : LE.le (α := ℝ≥0∞)
  (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetGE ν n))
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)
Tactic: refine (le_iSup (f := fun s ↦ _)
    (sigmaFinite_restrict_sigmaFiniteSetGE μ ν n)).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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))
have 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))
Tactic: refine tendsto_of_tendsto_of_tendsto_of_le_of_le ?_
    tendsto_const_nhds (measure_sigmaFiniteSetGE_ge μ ν) (measure_sigmaFiniteSetGE_le μ ν)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ 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))
have 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))
Tactic: nth_rewrite 2 [← tsub_zero (⨆ (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 ν
⊢ 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))
have refine : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞)) atTop (𝓝 0)
Tactic: refine ENNReal.Tendsto.sub tendsto_const_nhds ?_ (Or.inr ENNReal.zero_ne_top)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞)) atTop (𝓝 0)
have simp : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ (↑i : ℝ≥0∞)⁻¹) atTop (𝓝 0)
Tactic: simp only [one_div]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
have this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
Tactic: have := sigmaFinite_restrict_sigmaFiniteSetGE μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
have suffices : (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)
Tactic: suffices (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f) from
    this.sigmaFinite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)
have refine_1 : ∀ (n : ℕ),
  LT.lt (α := ℝ≥0∞)
    ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: refine ⟨fun n ↦ f (e n), fun _ ↦ by simp, fun n ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
refine_1 :
  ∀ (n : ℕ),
    LT.lt (α := ℝ≥0∞)
      ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) n) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)
have refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) i) Set.univ
Tactic: refine ⟨fun n ↦ f (e n), fun _ ↦ by simp, fun n ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν)ᶜ : ℝ≥0∞)
    (∞ : ℝ≥0∞) ∧
  LT.lt (α := ℝ≥0∞)
    ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair n).1) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: simp only [Nat.pairEquiv_symm_apply, measure_union_lt_top_iff, f, e]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν)ᶜ : ℝ≥0∞)
      (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞)
      ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞)
          (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
            μ.sigmaFiniteSetGE ν (Nat.unpair n).1) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
            μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
          μ.sigmaFiniteSetWRT' ν) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self,
      Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
    LT.lt (α := ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞)
          (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
              μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
            μ.sigmaFiniteSetWRT' ν) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
        μ.sigmaFiniteSetWRT' ν) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: simp only [measure_empty, ENNReal.zero_lt_top, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
            μ.sigmaFiniteSetGE ν (Nat.unpair n).1 ∩
          μ.sigmaFiniteSetWRT' ν) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞)
  ((μ : (a : Set α) → ℝ≥0∞)
      (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: refine (measure_mono Set.inter_subset_left).trans_lt ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ LT.lt (α := ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair n).1) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)
have refine_1 : LT.lt (α := ℝ≥0∞)
  ((μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1) : (a : Set α) → ℝ≥0∞)
      (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2) :
    ℝ≥0∞)
  (∞ : ℝ≥0∞)
Tactic: rw [← Measure.restrict_apply' (measurableSet_sigmaFiniteSetGE _)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) i) Set.univ
have refine_2 : Eq.{u_1 + 1} (α := Set α)
  (⋃ (i : ℕ),
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair i).1)
  Set.univ
Tactic: simp only [Nat.pairEquiv_symm_apply, f, e]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (i : ℕ),
      (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1)
    Set.univ
have refine_2 : (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
    ⋃ (i : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
  Set.univ
Tactic: rw [← Set.union_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this_1 : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
this :
  ⋃ (n : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ (i : ℕ),
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
have rw : (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ μ.sigmaFiniteSetWRT' ν = Set.univ
Tactic: rw [this, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this_1 : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
this :
  ⋃ (n : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν
rw : (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ μ.sigmaFiniteSetWRT' ν = Set.univ
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ (i : ℕ),
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
have rw₁ : Eq.{u_1 + 1} (α := Set α) Set.univ Set.univ
Tactic: rw [this, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ (i : ℕ),
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
have refine_2 : ⋃ (n : ℕ),
    spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
      μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
  μ.sigmaFiniteSetWRT' ν
Tactic: suffices ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1) = μ.sigmaFiniteSetWRT' ν by
      rw [this, Set.compl_union_self]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (n : ℕ), ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n)
    (⋃ (n : ℕ), μ.sigmaFiniteSetGE ν n)
have refine : ∀ (n : ℕ),
  ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Tactic: refine Set.iUnion_congr (fun n ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
⊢ ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
have rw : (⋃ (i : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) i) ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Tactic: rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
rw : (⋃ (i : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) i) ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
⊢ ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
have rw₁ : Set.univ ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Tactic: rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
n : ℕ
rw : (⋃ (i : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) i) ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
rw₁ : Set.univ ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
⊢ ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
have rw₂ : μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
Tactic: rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
this : ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))
f : ℕ × ℕ → Set α :=
  fun (p : ℕ × ℕ) ↦
    (μ.sigmaFiniteSetWRT' ν)ᶜ ∪ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν p.1)) p.2 ∩ μ.sigmaFiniteSetGE ν p.1
e : ℕ ≃ ℕ × ℕ := Nat.pairEquiv.symm
⊢ ⋃ (n : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν
have calc : Eq.{u_1 + 1} (α := Set α)
  (⋃ (n : ℕ), ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n)
  (⋃ (n : ℕ), μ.sigmaFiniteSetGE ν n)
Tactic: calc ⋃ n, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) n.unpair.2
        ∩ μ.sigmaFiniteSetGE ν n.unpair.1)
      = ⋃ n, ⋃ m, (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n) :=
          Set.iUnion_unpair (fun n m ↦ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n)
    _ = ⋃ n, μ.sigmaFiniteSetGE ν n := by
        refine Set.iUnion_congr (fun n ↦ ?_)
        rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]
    _ = μ.sigmaFiniteSetWRT' ν := rfl