case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
inst✝² : Zero β
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
hf : FinStronglyMeasurable f μ
⊢ ∃ t, MeasurableSet t ∧ (∀ (x : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
rcases hf with ⟨fs, hT_lt_top, h_approx⟩
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
let T n := support (fs n)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
have hT_meas : ∀ n, MeasurableSet (T n) := fun n => SimpleFunc.measurableSet_support (fs n)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
let t := ⋃ n, T n
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0

case intro.intro.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 (Measure.restrict μ t)
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0) ∧ SigmaFinite (Measure.restrict μ t)
refine' ⟨t, MeasurableSet.iUnion hT_meas, _, _⟩
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
⊢ ∀ (x : α), x ∈ tᶜ → f x = 0
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → f x = 0
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 using hxt n
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 0)
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
⊢ ∀ (x : α), x ∈ tᶜ → f x = 0
refine' fun x hxt => tendsto_nhds_unique (h_approx x) _
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => ↑(fs n) x) atTop (𝓝 0)
rw [funext fun n => h_fs_zero n x hxt]
no goals
case intro.intro.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
x : α
hxt : x ∈ tᶜ
⊢ Tendsto (fun n => 0) atTop (𝓝 0)
exact tendsto_const_nhds
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : α), x ∈ tᶜ → ↑(fs n) x = 0
intro n x hxt
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
rw [Set.mem_compl_iff, Set.mem_iUnion, not_exists] at hxt
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
simpa using hxt n
case intro.intro.refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : ℕ
⊢ ↑↑(Measure.restrict μ t) ((fun n => tᶜ ∪ T n) n) < ⊤

case intro.intro.refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
case intro.intro.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 (Measure.restrict μ t)
refine' ⟨⟨⟨fun n => tᶜ ∪ T n, fun _ => trivial, fun n => _, _⟩⟩⟩
case intro.intro.refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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) < ⊤
case intro.intro.refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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 : ℕ
⊢ ↑↑(Measure.restrict μ t) ((fun n => tᶜ ∪ T n) n) < ⊤
rw [Measure.restrict_apply' (MeasurableSet.iUnion hT_meas), Set.union_inter_distrib_right,
  Set.compl_inter_self t, Set.empty_union]
no goals
case intro.intro.refine'_2.refine'_1
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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) < ⊤
exact (measure_mono (Set.inter_subset_left _ _)).trans_lt (hT_lt_top n)
case intro.intro.refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
case intro.intro.refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
rw [← Set.union_iUnion (tᶜ) T]
no goals
case intro.intro.refine'_2.refine'_2
α : Type u_2
β : Type u_1
γ : Type ?u.240396
ι : Type ?u.240399
inst✝³ : Countable ι
m0 : MeasurableSpace α
μ : Measure α
f g : α → β
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
exact Set.compl_union_self _