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

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ μ t = ⊤

Tactic:
refine measure_eq_top_of_subset_compl_sigmaFiniteSetWRT'_of_measurableSet ht ht_subset ?_

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

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

Tactic:
rw [measure_eq_iInf]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ⊤

Tactic:
have hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ := Set.subset_inter hts hs_subset

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
⊢ ∀ (i : Set α), s ⊆ i → MeasurableSet i → μ i = ⊤

Tactic:
intro t hts ht

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ μ t = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ μ t = ⊤

Tactic:
suffices μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ∞ from
  measure_mono_top Set.inter_subset_left this

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ⊤

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

Tactic:
exact fun hνt ↦ hνs (measure_mono_null hst hνt)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
this : ∀ t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ, s ⊆ t → MeasurableSet t → μ t = ⊤
t : Set α
hts : s ⊆ t
ht : MeasurableSet t
hs_subset_t : s ⊆ t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ
⊢ μ (t ∩ (μ.sigmaFiniteSetWRT' ν)ᶜ) = ⊤

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

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), μ t = ⊤

Tactic:
simp_rw [iInf_eq_top]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ∀ (i : Set α), s ⊆ i → MeasurableSet i → μ i = ⊤

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

Tactic:
intro t ht_subset hst ht

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
t : Set α
ht_subset : t ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hst : s ⊆ t
ht : MeasurableSet t
⊢ μ t = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
hs_subset : s ⊆ (μ.sigmaFiniteSetWRT' ν)ᶜ
hνs : ν s ≠ 0
⊢ ∀ (i : Set α), s ⊆ i → MeasurableSet i → μ i = ⊤

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)

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