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

Tactic:
ENNReal.Tendsto.sub tendsto_const_nhds ?_ (Or.inr ENNReal.zero_ne_top)

Premises used: tendsto_const_nhds, ENNReal.zero_ne_top, ENNReal.Tendsto.sub, Or.inr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
refine : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞)) atTop (𝓝 0)
⊢ 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:
refine ENNReal.Tendsto.sub tendsto_const_nhds ?_ (Or.inr ENNReal.zero_ne_top)

Premises used: tendsto_const_nhds, ENNReal.zero_ne_top, ENNReal.Tendsto.sub, Or.inr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
simp : Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ (↑i : ℝ≥0∞)⁻¹) atTop (𝓝 0)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ HDiv.hDiv (α := ℝ≥0∞) 1 (↑i : ℝ≥0∞)) atTop (𝓝 0)

Tactic:
simp only [one_div]

Premises used: one_div
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ (↑i : ℝ≥0∞)⁻¹) atTop (𝓝 0)

Tactic:
ENNReal.tendsto_inv_nat_nhds_zero

Premises used: ENNReal.tendsto_inv_nat_nhds_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ℕ) ↦ (↑i : ℝ≥0∞)⁻¹) atTop (𝓝 0)

Tactic:
exact ENNReal.tendsto_inv_nat_nhds_zero

Premises used: ENNReal.tendsto_inv_nat_nhds_zero
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ MeasurableSet (μ.sigmaFiniteSetWRT' ν)

Tactic:
MeasurableSet.iUnion measurableSet_sigmaFiniteSetGE

Premises used: MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.Measure.sigmaFiniteSetWRT', MeasurableSet.iUnion
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ ∀ (n : ℕ), SigmaFinite (μ.restrict (μ.sigmaFiniteSetGE ν n))

Tactic:
have := sigmaFinite_restrict_sigmaFiniteSetGE μ ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
suffices : (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))

Tactic:
suffices (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f) from
    this.sigmaFinite
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
x : ℕ
⊢ (fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) x ∈ Set.range f

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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∞)
refine_2 : Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) i) Set.univ
⊢ (μ.restrict (μ.sigmaFiniteSetWRT' ν)).FiniteSpanningSetsIn (Set.range f)

Tactic:
refine ⟨fun n ↦ f (e n), fun _ ↦ by simp, fun n ↦ ?_, ?_⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ
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∞)
⊢ LT.lt (α := ℝ≥0∞)
    ((μ.restrict (μ.sigmaFiniteSetWRT' ν) : (a : Set α) → ℝ≥0∞) ((fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) n) : ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
simp only [Nat.pairEquiv_symm_apply, measure_union_lt_top_iff, f, e]

Premises used: MeasureTheory.measure_union_lt_top_iff, Nat.pairEquiv_symm_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ
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∞)
⊢ 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:
rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self,
      Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT']

Premises used: MeasureTheory.measurableSet_sigmaFiniteSetWRT', Set.compl_inter_self, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ
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∞)
⊢ 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:
simp only [measure_empty, ENNReal.zero_lt_top, true_and]

Premises used: ENNReal.zero_lt_top, MeasureTheory.measure_empty, true_and
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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∞)

Tactic:
(measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ
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∞)
⊢ 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:
refine (measure_mono Set.inter_subset_left).trans_lt ?_

Premises used: Set.inter_subset_left, MeasureTheory.measure_mono, LE.le.trans_lt
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ
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∞)
⊢ 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:
rw [← Measure.restrict_apply' (measurableSet_sigmaFiniteSetGE _)]

Premises used: MeasureTheory.measurableSet_sigmaFiniteSetGE, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 (μ.sigmaFiniteSetGE ν (Nat.unpair n).1) : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
measure_spanningSets_lt_top _ _

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 (μ.sigmaFiniteSetGE ν (Nat.unpair n).1) : (a : Set α) → ℝ≥0∞)
        (spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
exact measure_spanningSets_lt_top _ _

Premises used: MeasureTheory.measure_spanningSets_lt_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_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
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ℕ), (fun (n : ℕ) ↦ f ((e : (a : ℕ) → ℕ × ℕ) n)) i) Set.univ

Tactic:
simp only [Nat.pairEquiv_symm_apply, f, e]

Premises used: Nat.pairEquiv_symm_apply
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_2 :
  (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ (i : ℕ),
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ
⊢ 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:
rw [← Set.union_iUnion]

Premises used: Set.union_iUnion
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := Set α) Set.univ Set.univ
⊢ (μ.sigmaFiniteSetWRT' ν)ᶜ ∪
      ⋃ (i : ℕ),
        spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair i).1)) (Nat.unpair i).2 ∩
          μ.sigmaFiniteSetGE ν (Nat.unpair i).1 =
    Set.univ

Tactic:
rw [this, Set.compl_union_self]

Premises used: Set.compl_union_self
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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_2 :
  ⋃ (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

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]
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1)
    (⋃ (n : ℕ), ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n)

Tactic:
Set.iUnion_unpair (fun n m ↦ spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m
            ∩ μ.sigmaFiniteSetGE ν n)

Premises used: MeasureTheory.Measure.sigmaFiniteSetGE, MeasureTheory.Measure.restrict, Inter.inter, MeasureTheory.spanningSets, Set.iUnion_unpair
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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)

Tactic:
Set.iUnion_congr (fun n ↦ ?_)

Premises used: Set.iUnion_congr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 :
  ∀ (n : ℕ),
    ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
⊢ Eq.{u_1 + 1} (α := Set α)
    (⋃ (n : ℕ), ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n)
    (⋃ (n : ℕ), μ.sigmaFiniteSetGE ν n)

Tactic:
refine Set.iUnion_congr (fun n ↦ ?_)

Premises used: Set.iUnion_congr
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
rw₂ rw₃ : μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n
⊢ ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetGE ν n

Tactic:
rw [← Set.iUnion_inter, iUnion_spanningSets, Set.univ_inter]

Premises used: Set.univ_inter, Set.iUnion_inter, MeasureTheory.iUnion_spanningSets
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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 : ℕ), μ.sigmaFiniteSetGE ν n = μ.sigmaFiniteSetWRT' ν

Tactic:
rfl

Premises used: MeasureTheory.Measure.sigmaFiniteSetWRT', rfl
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
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
calc :
  Eq.{u_1 + 1} (α := Set α)
    (⋃ (n : ℕ), ⋃ (m : ℕ), spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν n)) m ∩ μ.sigmaFiniteSetGE ν n)
    (⋃ (n : ℕ), μ.sigmaFiniteSetGE ν n)
⊢ ⋃ (n : ℕ),
      spanningSets (μ.restrict (μ.sigmaFiniteSetGE ν (Nat.unpair n).1)) (Nat.unpair n).2 ∩
        μ.sigmaFiniteSetGE ν (Nat.unpair n).1 =
    μ.sigmaFiniteSetWRT' ν

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

Premises used: MeasureTheory.Measure.sigmaFiniteSetGE, MeasureTheory.Measure.restrict, Inter.inter, MeasureTheory.Measure.sigmaFiniteSetWRT', MeasureTheory.spanningSets, rfl, Set.iUnion_unpair
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
a :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
a₁ :
  LE.le (α := ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
apply le_antisymm

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

Tactic:
(le_iSup (f := fun _ ↦ _)
      (sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν)).trans ?_

Premises used: le_iSup, LE.le.trans, MeasureTheory.sigmaFinite_restrict_sigmaFiniteSetWRT'