-- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean
/-- The set of points for which a sequence of measurable functions converges to a given function
is measurable. -/
@[measurability]
lemma measurableSet_tendsto_fun [MeasurableSpace γ] [Countable ι]
    {l : Filter ι} [l.IsCountablyGenerated]
    [TopologicalSpace γ] [SecondCountableTopology γ] [PseudoMetrizableSpace γ]
    [OpensMeasurableSpace γ]
    {f : ι → β → γ} (hf : ∀ i, Measurable (f i)) {g : β → γ} (hg : Measurable g) :
    MeasurableSet { x | Tendsto (fun n ↦ f n x) l (𝓝 (g x)) }

Proof state:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : Countable ι
l : Filter ι
inst✝⁴ : l.IsCountablyGenerated
inst✝³ : TopologicalSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet {x | Tendsto (fun b => dist (f b x) (g x)) l (𝓝 0)}

Tactic:
exact measurableSet_tendsto (𝓝 0) (fun n ↦ (hf n).dist hg)

Result:
no goals

Proof state:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : Countable ι
l : Filter ι
inst✝⁴ : l.IsCountablyGenerated
inst✝³ : TopologicalSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l (𝓝 (g x))}

Tactic:
letI := TopologicalSpace.pseudoMetrizableSpacePseudoMetric γ

Result:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : Countable ι
l : Filter ι
inst✝⁴ : l.IsCountablyGenerated
inst✝³ : TopologicalSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l (𝓝 (g x))}

Proof state:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : Countable ι
l : Filter ι
inst✝⁴ : l.IsCountablyGenerated
inst✝³ : TopologicalSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet {x | Tendsto (fun n => f n x) l (𝓝 (g x))}

Tactic:
simp_rw [tendsto_iff_dist_tendsto_zero (f := fun n ↦ f n _)]

Result:
ι : Type u_2
γ : Type u_3
β : Type u_5
inst✝⁷ : MeasurableSpace β
inst✝⁶ : MeasurableSpace γ
inst✝⁵ : Countable ι
l : Filter ι
inst✝⁴ : l.IsCountablyGenerated
inst✝³ : TopologicalSpace γ
inst✝² : SecondCountableTopology γ
inst✝¹ : PseudoMetrizableSpace γ
inst✝ : OpensMeasurableSpace γ
f : ι → β → γ
hf : ∀ (i : ι), Measurable (f i)
g : β → γ
hg : Measurable g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ MeasurableSet {x | Tendsto (fun b => dist (f b x) (g x)) l (𝓝 0)}