-- Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean
theorem stronglyMeasurable_in_set {m : MeasurableSpace α} [TopologicalSpace β] [Zero β] {s : Set α}
    {f : α → β} (hs : MeasurableSet s) (hf : StronglyMeasurable f)
    (hf_zero : ∀ x, x ∉ s → f x = 0) :
    ∃ fs : ℕ → α →ₛ β,
      (∀ x, Tendsto (fun n => fs n x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ n, fs n x = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
have hg_zero : ∀ x ∉ s, ∀ n, g_seq_s n x = 0 := by
  intro x hx n
  rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_not_mem hx]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
⊢ ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x

Tactic:
intro x hx n

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
x : α
hx : x ∈ s
n : ℕ
⊢ (g_seq_s n) x = (hf.approx n) x

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∉ s
⊢ Tendsto (fun n => 0) atTop (𝓝 0)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

Tactic:
by_cases hx : x ∈ s

Result:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∉ s
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

Proof state:
case pos
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∈ s
⊢ Tendsto (fun n => (hf.approx n) x) atTop (𝓝 (f x))

Tactic:
exact hf.tendsto_approx x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
refine ⟨g_seq_s, fun x => ?_, hg_zero⟩

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
⊢ ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0

Tactic:
intro x hx n

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
x : α
hx : x ∉ s
n : ℕ
⊢ (g_seq_s n) x = 0

Proof state:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∉ s
⊢ Tendsto (fun n => (g_seq_s n) x) atTop (𝓝 (f x))

Tactic:
simp_rw [hg_zero x hx, hf_zero x hx]

Result:
case neg
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
hg_zero : ∀ x ∉ s, ∀ (n : ℕ), (g_seq_s n) x = 0
x : α
hx : x ∉ s
⊢ Tendsto (fun n => 0) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0

Tactic:
have hg_eq : ∀ x ∈ s, ∀ n, g_seq_s n x = hf.approx n x := by
  intro x hx n
  rw [SimpleFunc.coe_restrict _ hs, Set.indicator_of_mem hx]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
inst✝¹ : TopologicalSpace β
inst✝ : Zero β
s : Set α
f : α → β
hs : MeasurableSet s
hf : StronglyMeasurable f
hf_zero : ∀ x ∉ s, f x = 0
g_seq_s : ℕ → α →ₛ β := fun n => (hf.approx n).restrict s
hg_eq : ∀ x ∈ s, ∀ (n : ℕ), (g_seq_s n) x = (hf.approx n) x
⊢ ∃ fs, (∀ (x : α), Tendsto (fun n => (fs n) x) atTop (𝓝 (f x))) ∧ ∀ x ∉ s, ∀ (n : ℕ), (fs n) x = 0