-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
theorem measurable_of_tendsto_metrizable' {ι} {f : ι → α → β} {g : α → β} (u : Filter ι) [NeBot u]
    [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
    Measurable g

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ Measurable g

Tactic:
letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable g

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ Measurable g

Tactic:
apply measurable_of_isClosed'

Result:
case hf
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
⊢ ∀ (s : Set β), IsClosed s → s.Nonempty → s ≠ Set.univ → MeasurableSet (g ⁻¹' s)

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x => infNndist (g x) s
x : α
⊢ x ∈ g ⁻¹' s ↔ x ∈ (fun x => infNndist (g x) s) ⁻¹' {0}

Tactic:
simp [h1s, ← h1s.mem_iff_infDist_zero h2s, ← NNReal.coe_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ Measurable fun x => infNndist (g x) s

Tactic:
suffices Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s) from
  NNReal.measurable_of_tendsto' u (fun i => (hf i).infNndist) this

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ Tendsto (fun i x => infNndist (f i x) s) u (𝓝 fun x => infNndist (g x) s)

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x => infNndist (g x) s
⊢ MeasurableSet (g ⁻¹' s)

Tactic:
have h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0} := by
  ext x
  simp [h1s, ← h1s.mem_iff_infDist_zero h2s, ← NNReal.coe_eq_zero]

Result:
case hf
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x => infNndist (g x) s
h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0}
⊢ MeasurableSet (g ⁻¹' s)

Proof state:
case hf
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this✝ : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable fun x => infNndist (g x) s
h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0}
⊢ MeasurableSet ((fun x => infNndist (g x) s) ⁻¹' {0})

Tactic:
exact this (measurableSet_singleton 0)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : PseudoMetrizableSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed s
h2s : s.Nonempty
h3s : s ≠ Set.univ
x : α
⊢ Tendsto (fun i => infNndist (f i x) s) u (𝓝 (infNndist (g x) s))

Tactic:
exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x)

Result:
no goals