-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
/-- For all sets `s` in `(μ.sigmaFiniteSetWRT ν)ᶜ`, if `ν s ≠ 0` then `μ s = ∞`. -/
lemma measure_eq_top_of_subset_compl_sigmaFiniteSetWRT [SFinite ν]
    (hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ) (hνs : ν s ≠ 0) :
    μ s = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
⊢ μ s = ⊤

Tactic:
have ⟨ν', hν', hνν', _⟩ := exists_isFiniteMeasure_absolutelyContinuous ν

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
⊢ μ s = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ
hνt : ν t ≠ 0
⊢ ν' t ≠ 0

Tactic:
exact fun hν't ↦ hνt (hνν' hν't)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
⊢ μ s = ⊤

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)

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ μ s = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
⊢ ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤

Tactic:
refine ⟨μ.sigmaFiniteSetWRT' ν', measurableSet_sigmaFiniteSetWRT',
  sigmaFinite_restrict_sigmaFiniteSetWRT' _ _,
  fun t ht_subset hνt ↦ measure_eq_top_of_subset_compl_sigmaFiniteSetWRT' ht_subset ?_⟩

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν')ᶜ
hνt : ν t ≠ 0
⊢ ν' t ≠ 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
hs_subset : s ⊆ h.chooseᶜ
⊢ μ s = ⊤

Tactic:
exact h.choose_spec.2.2 s hs_subset hνs

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT ν)ᶜ
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
⊢ μ s = ⊤

Tactic:
rw [Measure.sigmaFiniteSetWRT, dif_pos h] at hs_subset

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : SFinite ν
hνs : ν s ≠ 0
ν' : Measure α
hν' : IsFiniteMeasure ν'
hνν' : ν ≪ ν'
right✝ : ν' ≪ ν
h : ∃ s, MeasurableSet s ∧ SigmaFinite (μ.restrict s) ∧ ∀ t ⊆ sᶜ, ν t ≠ 0 → μ t = ⊤
hs_subset : s ⊆ h.chooseᶜ
⊢ μ s = ⊤