-- 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:
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)

Tactic:
let T n := 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)
⊢ ∃ 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
⊢ tᶜ ∪ ⋃ i, T i = univ

Tactic:
exact Set.compl_union_self _

Result:
no goals

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 ∈ tᶜ
⊢ (fs n) x = 0

Tactic:
rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt

Result:
α : 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

Proof state:
case intro.intro.refine_2.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
n : ℕ
⊢ μ (T n ∩ ⋃ b, T b) < ⊤

Tactic:
exact (measure_mono Set.inter_subset_left).trans_lt (hT_lt_top n)

Result:
no goals

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 ∈ tᶜ, (fs n) x = 0

Tactic:
intro n x hxt

Result:
α : 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 ∈ tᶜ
⊢ (fs n) x = 0

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 ∈ tᶜ, f x = 0

Tactic:
refine fun x hxt => tendsto_nhds_unique (h_approx x) ?_

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 => (fs n) x) atTop (𝓝 0)

Proof state:
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)

Tactic:
refine ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => ?_, ?_⟩⟩⟩

Result:
case intro.intro.refine_2.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
n : ℕ
⊢ (μ.restrict t) ((fun n => tᶜ ∪ T n) n) < ⊤

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

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 => 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
case intro.intro.refine_2.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
n : ℕ
⊢ (μ.restrict t) ((fun n => tᶜ ∪ T n) n) < ⊤

Tactic:
rw [Measure.restrict_apply' (MeasurableSet.iUnion hT_meas), Set.union_inter_distrib_right,
  Set.compl_inter_self t, Set.empty_union]

Result:
case intro.intro.refine_2.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
n : ℕ
⊢ μ (T n ∩ ⋃ b, T b) < ⊤