-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
@[simp]
lemma measure_compl_sigmaFiniteSetWRT (hμν : μ ≪ ν) [SigmaFinite μ] [SFinite ν] :
    ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⊤ = 0

Tactic:
rw [← h h0, ← Measure.iSup_restrict_spanningSets]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ∀ (i : ℕ), μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0

Tactic:
intro i

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
⊢ μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⨆ i, (μ.restrict (spanningSets μ i)) (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
simp_rw [Measure.restrict_apply' (measurableSet_spanningSets μ _), ENNReal.iSup_eq_zero]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ∀ (i : ℕ), μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0

Proof state:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ ν ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) ≠ 0

Tactic:
exact fun h ↦ h_ne_zero (hμν h)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) < ⊤

Tactic:
exact (measure_mono Set.inter_subset_right).trans_lt (measure_spanningSets_lt_top μ i)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
have h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ :=
  measure_eq_top_of_subset_compl_sigmaFiniteSetWRT subset_rfl

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ False

case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ ν ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) ≠ 0

Tactic:
swap

Result:
case refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ ν ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) ≠ 0

case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ False

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
⊢ μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0

Tactic:
by_contra h_ne_zero

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
⊢ False

Proof state:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ False

Tactic:
refine absurd h_zero_top (ne_of_lt ?_)

Result:
case refine_2
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
i : ℕ
h_ne_zero : ¬μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = 0
h_zero_top : μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) = ⊤
⊢ μ ((μ.sigmaFiniteSetWRT ν)ᶜ ∩ spanningSets μ i) < ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
⊢ ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0

Tactic:
by_contra h0

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ False

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ False

Tactic:
refine ENNReal.top_ne_zero ?_

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
hμν : μ ≪ ν
inst✝¹ : SigmaFinite μ
inst✝ : SFinite ν
h : ν (μ.sigmaFiniteSetWRT ν)ᶜ ≠ 0 → μ (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤
h0 : ¬ν (μ.sigmaFiniteSetWRT ν)ᶜ = 0
⊢ ⊤ = 0