-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem exists_set_sigmaFinite (hf : AEFinStronglyMeasurable f μ) :
    ∃ t, MeasurableSet t ∧ f =ᵐ[μ.restrict tᶜ] 0 ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ f =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
refine EventuallyEq.trans (ae_restrict_of_ae hfg) ?_

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ g =ᶠ[ae (μ.restrict tᶜ)] 0

Tactic:
rw [EventuallyEq, ae_restrict_iff' ht.compl]

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
hf : AEFinStronglyMeasurable f μ
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
rcases hf with ⟨g, hg, hfg⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
obtain ⟨t, ht, hgt_zero, htμ⟩ := hg.exists_set_sigmaFinite

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∀ᵐ (x : α) ∂μ, x ∈ tᶜ → g x = 0 x

Tactic:
exact Eventually.of_forall hgt_zero

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ ∃ t, MeasurableSet t ∧ f =ᶠ[ae (μ.restrict tᶜ)] 0 ∧ SigmaFinite (μ.restrict t)

Tactic:
refine ⟨t, ht, ?_, htμ⟩

Result:
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : Zero β
inst✝ : T2Space β
g : α → β
hg : FinStronglyMeasurable g μ
hfg : f =ᶠ[ae μ] g
t : Set α
ht : MeasurableSet t
hgt_zero : ∀ x ∈ tᶜ, g x = 0
htμ : SigmaFinite (μ.restrict t)
⊢ f =ᶠ[ae (μ.restrict tᶜ)] 0