-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem exists_set_sigmaFinite [Zero β] [TopologicalSpace β] [T2Space β]
    (hf : FinStronglyMeasurable f μ) :
    ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
n : ℕ
x : α
hxt : ∀ (x_1 : ℕ), x ∉ T x_1
⊢ (fs n) x = 0

Tactic:
simpa [T] using hxt n

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
refine ⟨t, MeasurableSet.iUnion hT_meas, ?_, ?_⟩

Result:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ∀ x ∈ tᶜ, f x = 0

case intro.intro.refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => (fs n) x) atTop (𝓝 0)

Tactic:
rw [funext fun n => h_fs_zero n x hxt]

Result:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => 0) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
hf : FinStronglyMeasurable f μ
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
rcases hf with ⟨fs, hT_lt_top, h_approx⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)

Result:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ∀ x ∈ tᶜ, f x = 0

Tactic:
have h_fs_zero : ∀ n, ∀ x ∈ tᶜ, fs n x = 0 := by
  intro n x hxt
  rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
  simpa [T] using hxt n

Result:
case intro.intro.refine_1
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
h_fs_zero : ∀ (n : ℕ), ∀ x ∈ tᶜ, (fs n) x = 0
⊢ ∀ x ∈ tᶜ, f x = 0

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Tactic:
let t := ⋃ n, T n

Result:
case intro.intro
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ∃ t, MeasurableSet t ∧ (∀ x ∈ tᶜ, f x = 0) ∧ SigmaFinite (μ.restrict t)

Proof state:
case intro.intro.refine_2.refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ ⋃ i, (fun n => tᶜ ∪ T n) i = univ

Tactic:
rw [← Set.union_iUnion tᶜ T]

Result:
case intro.intro.refine_2.refine_2
α : Type u_1
β : Type u_2
m0 : MeasurableSpace α
μ : Measure α
f : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
fs : ℕ → α →ₛ β
hT_lt_top : ∀ (n : ℕ), μ (support ⇑(fs n)) < ⊤
h_approx : ∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))
T : ℕ → Set α := fun n => support ⇑(fs n)
hT_meas : ∀ (n : ℕ), MeasurableSet (T n)
t : Set α := ⋃ n, T n
⊢ tᶜ ∪ ⋃ i, T i = univ