awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
a :
  LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

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

Tactic:
le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
      measurableSet_sigmaFiniteSetWRT'

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

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict s)), ν s) (μ.sigmaFiniteSetWRT' ν)
      measurableSet_sigmaFiniteSetWRT'

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

Tactic:
le_of_tendsto' (tendsto_measure_sigmaFiniteSetGE μ ν)
      (fun _ ↦ measure_mono (Set.subset_iUnion _ _))

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

Tactic:
exact le_of_tendsto' (tendsto_measure_sigmaFiniteSetGE μ ν)
      (fun _ ↦ measure_mono (Set.subset_iUnion _ _))

Premises used: MeasureTheory.Measure.sigmaFiniteSetGE, Set.subset_iUnion, MeasureTheory.tendsto_measure_sigmaFiniteSetGE, MeasureTheory.measure_mono, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ¬SigmaFinite (μ.restrict s)
by_contra : ∀ (h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), False
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
by_contra h
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ¬SigmaFinite (μ.restrict s)
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))

Tactic:
have h_lt_top : Fact (μ s < ∞) := ⟨Ne.lt_top h⟩
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ¬SigmaFinite (μ.restrict s)
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_lt_top : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ False

Tactic:
this inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this : ¬SigmaFinite (μ.restrict s)
h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
h_lt_top : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
⊢ False

Tactic:
exact this inferInstance

Premises used: inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
suffices : ¬SigmaFinite (μ.restrict s)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices ¬ SigmaFinite (μ.restrict s) by
    by_contra h
    have h_lt_top : Fact (μ s < ∞) := ⟨Ne.lt_top h⟩
    exact this inferInstance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
rw :
  (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
rw₁ : Disjoint (μ.sigmaFiniteSetWRT' ν) s
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)

Tactic:
rw [measure_union _ hs]

Premises used: MeasureTheory.measure_union
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
⊢ (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
ENNReal.lt_add_right (measure_ne_top _ _) hνs

Premises used: ENNReal.lt_add_right, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
⊢ (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) <
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
exact ENNReal.lt_add_right (measure_ne_top _ _) hνs

Premises used: ENNReal.lt_add_right, MeasureTheory.measure_ne_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
⊢ Disjoint (μ.sigmaFiniteSetWRT' ν) s

Tactic:
disjoint_compl_right.mono_right hs_subset

Premises used: disjoint_compl_right, Disjoint.mono_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
⊢ Disjoint (μ.sigmaFiniteSetWRT' ν) s

Tactic:
exact disjoint_compl_right.mono_right hs_subset

Premises used: disjoint_compl_right, Disjoint.mono_right
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)

Tactic:
have h_lt : ν (μ.sigmaFiniteSetWRT' ν) < ν (μ.sigmaFiniteSetWRT' ν ∪ s) := by
    rw [measure_union _ hs]
    · exact ENNReal.lt_add_right (measure_ne_top _ _) hνs
    · exact disjoint_compl_right.mono_right hs_subset
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
rw : ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
| ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)

Tactic:
rw [measure_sigmaFiniteSetWRT']

Premises used: MeasureTheory.measure_sigmaFiniteSetWRT'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
conv_rhs :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)

Tactic:
conv_rhs => rw [measure_sigmaFiniteSetWRT']

Premises used: MeasureTheory.measure_sigmaFiniteSetWRT'
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
(le_iSup
      (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_

Premises used: le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
refine_1 : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))
refine_2 :
  LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))),
      (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
refine (le_iSup
      (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_

Premises used: le_iSup, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))

Tactic:
have := sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
this : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
⊢ SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))),
      (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)

Tactic:
le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict _)), ν s)
        (μ.sigmaFiniteSetWRT' ν ∪ s) (measurableSet_sigmaFiniteSetWRT'.union hs)

Premises used: le_iSup₂, MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.Measure.sigmaFiniteSetWRT', MeasurableSet.union, Union.union
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))),
      (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s))
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)

Tactic:
exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict _)), ν s)
        (μ.sigmaFiniteSetWRT' ν ∪ s) (measurableSet_sigmaFiniteSetWRT'.union hs)

Premises used: le_iSup₂, MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.Measure.sigmaFiniteSetWRT', MeasurableSet.union, Union.union
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)

Tactic:
have h_le : ν (μ.sigmaFiniteSetWRT' ν ∪ s) ≤ ν (μ.sigmaFiniteSetWRT' ν) := by
    conv_rhs => rw [measure_sigmaFiniteSetWRT']
    refine (le_iSup
      (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_
    · have := sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν
      infer_instance
    · exact le_iSup₂ (f := fun s _ ↦ ⨆ (_ : SigmaFinite (μ.restrict _)), ν s)
        (μ.sigmaFiniteSetWRT' ν ∪ s) (measurableSet_sigmaFiniteSetWRT'.union hs)
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
⊢ False

Tactic:
h_lt.not_ge h_le

Premises used: LT.lt.not_ge
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs : MeasurableSet s
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hsσ : SigmaFinite (μ.restrict s)
h_lt :
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
h_le :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
⊢ False

Tactic:
exact h_lt.not_ge h_le

Premises used: LT.lt.not_ge
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
rw : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t) ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [measure_eq_iInf]

Premises used: MeasureTheory.measure_eq_iInf
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw :
  ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t) ∞

Tactic:
simp_rw [iInf_eq_top]

Premises used: iInf_eq_top
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ,
    s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
      measure_mono_top Set.inter_subset_left this
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ,
    s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ

Tactic:
have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ,
    s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)

Premises used: Compl.compl, MeasurableSet.compl, Inter.inter, MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.Measure.sigmaFiniteSetWRT', Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
this :
  ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ,
    s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
exact this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)

Premises used: Compl.compl, MeasurableSet.compl, Inter.inter, MeasureTheory.measurableSet_sigmaFiniteSetWRT', MeasureTheory.Measure.sigmaFiniteSetWRT', Set.inter_subset_right, MeasurableSet.inter
-- Module: Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
suffices :
  ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ,
    s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
suffices ∀ t, t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ → s ⊆ t → MeasurableSet t → μ t = ∞ by
    intro t hts ht
    suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
      measure_mono_top Set.inter_subset_left this
    have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
    exact this (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) Set.inter_subset_right hs_subset_t
      (ht.inter measurableSet_sigmaFiniteSetWRT'.compl)