-- Mathlib/MeasureTheory/Measure/WithDensityFinite.lean
lemma restrict_compl_sigmaFiniteSet [SFinite μ] :
    μ.restrict μ.sigmaFiniteSetᶜ = ∞ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) ≠ 0

Tactic:
exact fun h ↦ hμt (absolutelyContinuous_toFinite μ h)

Result:
no goals

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
rw [hμt, toFinite_absolutelyContinuous μ hμt]

Result:
no goals

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ⊤ * (μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t = ⊤ * (μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t

Tactic:
rw [Measure.restrict_apply ht, Measure.restrict_apply ht]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ μ.restrict μ.sigmaFiniteSetᶜ = ⊤ • μ.toFinite.restrict μ.sigmaFiniteSetᶜ

Tactic:
rw [Measure.sigmaFiniteSet,
  restrict_compl_sigmaFiniteSetWRT (Measure.AbsolutelyContinuous.refl μ)]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ⊤ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ = ⊤ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
rw [ENNReal.top_mul hμt, ENNReal.top_mul]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) ≠ 0

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
⊢ ⊤ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ = ⊤ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ

Tactic:
ext t ht

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ (⊤ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t = (⊤ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ (⊤ • μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t = (⊤ • μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t

Tactic:
simp only [Measure.smul_apply, smul_eq_mul]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ⊤ * (μ.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t = ⊤ * (μ.toFinite.restrict (μ.sigmaFiniteSetWRT μ)ᶜ) t

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

Tactic:
by_cases hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0
⊢ ⊤ * μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = ⊤ * μ.toFinite (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ)