awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have a₁ : LE.le (α := ℝ≥0∞)
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
have a : LE.le (α := ℝ≥0∞)
  (⨆ (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))), (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν))
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s)
Tactic: refine (le_iSup (f := fun _ ↦ _)
      (sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν)).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have by_contra : ∀ (h : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
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∞)
⊢ False
have h_lt_top : Fact (LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞))
Tactic: have h_lt_top : Fact (μ s < ∞) := ⟨Ne.lt_top h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have suffices : ¬SigmaFinite (μ.restrict s)
Tactic: suffices ¬ SigmaFinite (μ.restrict s) by
    by_contra h
    have h_lt_top : Fact (μ s < ∞) := ⟨Ne.lt_top h⟩
    exact this inferInstance
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
have rw : (ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) <
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [measure_union _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
have rw₁ : Disjoint (μ.sigmaFiniteSetWRT' ν) s
Tactic: rw [measure_union _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
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)
⊢ False
have h_lt : 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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
| ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν) : ℝ≥0∞)
have rw : ⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s
Tactic: rw [measure_sigmaFiniteSetWRT']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
have conv_rhs : LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
  (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: conv_rhs => rw [measure_sigmaFiniteSetWRT']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
have refine_1 : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))
Tactic: refine (le_iSup
      (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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))
⊢ LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (μ.sigmaFiniteSetWRT' ν ∪ s) : ℝ≥0∞)
    (⨆ (s : Set α), ⨆ (_ : MeasurableSet s), ⨆ (_ : SigmaFinite (μ.restrict s)), (ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have 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)
Tactic: refine (le_iSup
      (f := fun (_ : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν ∪ s))) ↦ _) ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
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' ν ∪ s))
have this : SigmaFinite (μ.restrict (μ.sigmaFiniteSetWRT' ν))
Tactic: have := sigmaFinite_restrict_sigmaFiniteSetWRT' μ ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
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∞)
⊢ False
have h_le : 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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t) ∞
Tactic: rw [measure_eq_iInf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (μ : (a : Set α) → ℝ≥0∞) t) ∞
have simp_rw : ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp_rw [iInf_eq_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have suffices : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
      measure_mono_top Set.inter_subset_left this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
Tactic: have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
⊢ ∀ (i : Set α) (i_1 : s ⊆ i) (i_2 : MeasurableSet i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (∞ : ℝ≥0∞)
have suffices : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥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)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
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∞)
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have have : ∀ (ν' : Measure α) (hν' : IsFiniteMeasure ν') (hνν' : ν ≪ ν'),
  ν' ≪ ν → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have ⟨ν', hν', hνν', _⟩ := exists_isFiniteMeasure_absolutelyContinuous ν
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
⊢ ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (t : Set α) (ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ)
  (hνt : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)),
  Ne (α := ℝ≥0∞) ((ν' : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine ⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
      sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
      fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have h : ∃ (s : Set α),
  MeasurableSet s ∧
    SigmaFinite (μ.restrict s) ∧
      ∀ t ⊆ sᶜ,
        Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
          Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: have h : ∃ s : Set α, MeasurableSet s ∧ SigmaFinite (μ.restrict s)
      ∧ (∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ∞) := by
    refine ⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
      sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
      fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩
    exact fun hν't ↦ hνt (hνν' hν't)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right : ν' ≪ ν
h :
  ∃ (s : Set α),
    MeasurableSet s ∧
      SigmaFinite (μ.restrict s) ∧
        ∀ t ⊆ sᶜ,
          Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
            Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have rw : ∀ (hνs : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)) (ν' : Measure α) (hν' : IsFiniteMeasure ν')
  (hνν' : ν ≪ ν'),
  ν' ≪ ν →
    ∀
      (h :
        ∃ (s : Set α),
          MeasurableSet s ∧
            SigmaFinite (μ.restrict s) ∧
              ∀ t ⊆ sᶜ,
                Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞))
      (hs_subset :
        s ⊆
          (h.choose (p := fun (s : Set α) ↦
              MeasurableSet s ∧
                SigmaFinite (μ.restrict s) ∧
                  ∀ t ⊆ sᶜ,
                    Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (0 : ℝ≥0∞) →
                      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)))ᶜ),
      Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [Measure.sigmaFiniteSetWRT, dif_pos h] at hs_subset
Cleared hypotheses: hs_subset, hνs, ν', hν', hνν', right, h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
⊢ μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ)
have h : ∀ (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      ((HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((HSMul.hSMul (α := ℝ≥0∞) ∞ (ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
Tactic: rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl,
    Measure.smul_apply, smul_eq_mul,
    Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
have pos : ∀ (hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
Tactic: by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
pos :
  ∀ (hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
have neg : ∀ (hνs : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
  (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
Tactic: by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
have pos : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [hνs, mul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SFinite ν
hμν : μ ≪ ν
s : Set α
h : MeasurableSet s
hνs : ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [ENNReal.top_mul hνs, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
      Set.inter_subset_right hνs]