awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : SecondCountableTopology α
f g : β → α
hf : Measurable f
hg : Measurable g
⊢ Measurable (β := ℝ≥0∞) fun (b : β) ↦ EDist.edist (f b) (g b)

Tactic:
continuous_edist.measurable2 hf hg

Premises used: continuous_edist, Continuous.measurable2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : PseudoEMetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
inst_4 : SecondCountableTopology α
f g : β → α
μ : Measure β
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (a : β) ↦ EDist.edist (f a) (g a)) μ

Tactic:
continuous_edist.aemeasurable2 hf hg

Premises used: continuous_edist, Continuous.aemeasurable2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : MetricSpace α
inst_1 : MeasurableSpace α
inst_2 : OpensMeasurableSpace α
inst_3 : ProperSpace α
μ : Measure α
inst_4 : IsFiniteMeasureOnCompacts μ
s : Set α
hs : IsCompact s
⊢ Tendsto (β := ℝ≥0∞) (fun (r : ℝ) ↦ ((μ : (a : Set α) → ℝ≥0∞) (Metric.cthickening r s) : ℝ≥0∞)) (𝓝 0)
    (𝓝 ((μ : (a : Set α) → ℝ≥0∞) s) : Filter ℝ≥0∞)

Tactic:
tendsto_measure_cthickening_of_isClosed
    ⟨1, zero_lt_one, hs.isBounded.cthickening.measure_lt_top.ne⟩ hs.isClosed

Premises used: IsCompact.isBounded, zero_lt_one, Bornology.IsBounded.measure_lt_top, And.intro, tendsto_measure_cthickening_of_isClosed, Exists.intro, Bornology.IsBounded.cthickening, OfNat.ofNat, LT.lt.ne, IsCompact.isClosed
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablyGenerated α
inst_1 : MeasurableSpace.SeparatesPoints α
rcases :
  ∀ (s : Set (ℕ → Bool)) (f : α ≃ᵐ (↑s : Type)),
    ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
rcases measurableEquiv_nat_bool_of_countablyGenerated α with ⟨s, ⟨f⟩⟩

Premises used: MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablyGenerated α
inst_1 : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ (↑s : Type)
this : TopologicalSpace α := induced (Y := (↑s : Type)) (⇑f : (a : α) → (↑s : Type)) inferInstance
F : α ≃ₜ (↑s : Type) := f.toHomeomorphOfIsInducing ⋯
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
⟨inferInstance, F.secondCountableTopology, F.symm.t4Space,
    f.measurableEmbedding.borelSpace F.isInducing⟩

Premises used: Homeomorph.isInducing, MeasurableEquiv.measurableEmbedding, Homeomorph.secondCountableTopology, inferInstance, Homeomorph.symm, And.intro, Exists.intro, Homeomorph.t4Space, MeasurableEmbedding.borelSpace
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablyGenerated α
inst_1 : MeasurableSpace.SeparatesPoints α
s : Set (ℕ → Bool)
f : α ≃ᵐ (↑s : Type)
this : TopologicalSpace α := induced (Y := (↑s : Type)) (⇑f : (a : α) → (↑s : Type)) inferInstance
F : α ≃ₜ (↑s : Type) := f.toHomeomorphOfIsInducing ⋯
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ BorelSpace α

Tactic:
exact ⟨inferInstance, F.secondCountableTopology, F.symm.t4Space,
    f.measurableEmbedding.borelSpace F.isInducing⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
rcases :
  ∀ (m' : MeasurableSpace α),
    CountablyGenerated α →
      MeasurableSpace.SeparatesPoints α →
        ∀ (m'le : m' ≤ m), ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
rcases exists_countablyGenerated_le_of_countablySeparated α with ⟨m', _, _, m'le⟩

Premises used: MeasurableSpace.exists_countablyGenerated_le_of_countablySeparated
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
rcases :
  ∀ (τ : TopologicalSpace α),
    SecondCountableTopology α →
      T4Space α →
        ∀ (τm' : BorelSpace α),
          ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
rcases exists_borelSpace_of_countablyGenerated_of_separatesPoints (m := m') with ⟨τ, _, _, τm'⟩

Premises used: exists_borelSpace_of_countablyGenerated_of_separatesPoints
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
τ : TopologicalSpace α
left_2 : SecondCountableTopology α
left_3 : T4Space α
τm' : BorelSpace α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩

Premises used: BorelSpace.measurable_eq, OpensMeasurableSpace.mk, Eq.le, And.intro, Exists.intro, LE.le.trans, Eq.symm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_5
m : MeasurableSpace α
inst : CountablySeparated α
m' : MeasurableSpace α
left : CountablyGenerated α
left_1 : MeasurableSpace.SeparatesPoints α
m'le : m' ≤ m
τ : TopologicalSpace α
left_2 : SecondCountableTopology α
left_3 : T4Space α
τm' : BorelSpace α
⊢ ∃ (x : TopologicalSpace α), SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α

Tactic:
exact ⟨τ, ‹_›, ‹_›, @OpensMeasurableSpace.mk _ _ m (τm'.measurable_eq.symm.le.trans m'le)⟩
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
ε : Type u_5
inst : MeasurableSpace ε
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
inst_3 : OpensMeasurableSpace ε
⊢ Measurable.{u_5, 0} (α := ε) enorm

Tactic:
continuous_enorm.measurable

Premises used: continuous_enorm, Continuous.measurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
β : Type u_2
ε : Type u_5
inst : MeasurableSpace ε
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
inst_3 : OpensMeasurableSpace ε
inst_4 : MeasurableSpace β
f : β → ε
hf : Measurable f
⊢ Measurable (β := ℝ≥0∞) fun (x : β) ↦ ‖f x‖ₑ

Tactic:
measurable_enorm.comp hf

Premises used: Measurable.comp, measurable_enorm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
β : Type u_2
ε : Type u_5
inst : MeasurableSpace ε
inst_1 : TopologicalSpace ε
inst_2 : ContinuousENorm ε
inst_3 : OpensMeasurableSpace ε
inst_4 : MeasurableSpace β
f : β → ε
μ : Measure β
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : β) ↦ ‖f x‖ₑ) μ

Tactic:
measurable_enorm.comp_aemeasurable hf

Premises used: measurable_enorm, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
⊢ Measurable.{u_1, 0} (α := α) norm

Tactic:
continuous_norm.measurable

Premises used: Continuous.measurable, continuous_norm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
⊢ Measurable (β := ℝ) fun (a : β) ↦ ‖f a‖

Tactic:
measurable_norm.comp hf

Premises used: measurable_norm, Measurable.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
μ : Measure β
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ) (fun (a : β) ↦ ‖f a‖) μ

Tactic:
measurable_norm.comp_aemeasurable hf

Premises used: measurable_norm, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
⊢ Measurable.{u_1, 0} (α := α) nnnorm

Tactic:
continuous_nnnorm.measurable

Premises used: Continuous.measurable, continuous_nnnorm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
hf : Measurable f
⊢ Measurable (β := ℝ≥0) fun (a : β) ↦ ‖f a‖₊

Tactic:
measurable_nnnorm.comp hf

Premises used: Measurable.comp, measurable_nnnorm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : NormedAddCommGroup α
inst_2 : OpensMeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
μ : Measure β
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0) (fun (a : β) ↦ ‖f a‖₊) μ

Tactic:
measurable_nnnorm.comp_aemeasurable hf

Premises used: Measurable.comp_aemeasurable, measurable_nnnorm
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
hf₁ : ∀ (s : Set β), IsClosed[inst_1] s → s.Nonempty → s ≠ Set.univ → MeasurableSet (g ⁻¹' s)
⊢ Measurable g

Tactic:
apply measurable_of_isClosed'

Premises used: measurable_of_isClosed'
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
suffices :
  Tendsto.{u_3, u_1} (β := (x : α) → ℝ≥0) (fun (i : ι) (x : α) ↦ infNndist (f i x) s) u
    (𝓝 fun (x : α) ↦ infNndist (g x) s)
⊢ Measurable (β := ℝ≥0) 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
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
rw :
  ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))),
    let this := 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))
⊢ Tendsto.{u_3, u_1} (β := (x : α) → ℝ≥0) (fun (i : ι) (x : α) ↦ infNndist (f i x) s) u
    (𝓝 fun (x : α) ↦ infNndist (g x) s)

Tactic:
rw [tendsto_pi_nhds] at lim ⊢

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : 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[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
x : α
⊢ Tendsto (fun (i : ι) ↦ infNndist (f i x) s) u (𝓝 (infNndist (g x) s))

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

Premises used: ENNReal.toNNReal, Continuous.tendsto, Metric.continuous_infNndist_pt, Metric.infNndist, WithTop.untopD, Filter.Tendsto.comp, WithTop.recTopCoe
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : 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[inst_1] 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)

Premises used: Continuous.tendsto, Metric.continuous_infNndist_pt, Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
⊢ Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s

Tactic:
have : Measurable fun x => infNndist (g x) s := by
    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
    rw [tendsto_pi_nhds] at lim ⊢
    intro x
    exact ((continuous_infNndist_pt s).tendsto (g x)).comp (lim x)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
h :
  ∀ (x : α), x ∈ g ⁻¹' s ↔ Membership.mem (γ := Set α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}) x
⊢ g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
x : α
⊢ x ∈ g ⁻¹' s ↔ Membership.mem (γ := Set α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}) x

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

Premises used: IsClosed.mem_iff_infDist_zero, NNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
⊢ g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}

Tactic:
have h4s : g ⁻¹' s = (fun x => infNndist (g x) s) ⁻¹' {0} := by
    ext x
    simp [← h1s.mem_iff_infDist_zero h2s, ← NNReal.coe_eq_zero]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
h4s : g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
hf₁ : MeasurableSet.{u_1} (α := α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0})
⊢ MeasurableSet (g ⁻¹' s)

Tactic:
rw [h4s]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
h4s : g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
⊢ MeasurableSet.{u_1} (α := α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0})

Tactic:
this (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
f : ι → α → β
g : α → β
u : Filter ι
inst_5 : u.NeBot
inst_6 : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
s : Set β
h1s : IsClosed[inst_1] s
h2s : s.Nonempty
h3s : s ≠ Set.univ
this : Measurable (β := ℝ≥0) fun (x : α) ↦ infNndist (g x) s
h4s : g ⁻¹' s = Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0}
⊢ MeasurableSet.{u_1} (α := α) (Set.preimage (β := ℝ≥0) (fun (x : α) ↦ infNndist (g x) s) {0})

Tactic:
exact this (measurableSet_singleton 0)

Premises used: MeasurableSingletonClass.measurableSet_singleton, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
f : ℕ → α → β
g : α → β
hf : ∀ (i : ℕ), Measurable (f i)
lim : Tendsto f atTop (𝓝 g)
⊢ Measurable g

Tactic:
measurable_of_tendsto_metrizable' atTop hf lim

Premises used: measurable_of_tendsto_metrizable', Filter.atTop
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
rcases : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
rcases u.exists_seq_tendsto with ⟨v, hv⟩

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
⊢ ∀ (n : ℕ), AEMeasurable (f (v n)) μ

Tactic:
have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
x : α
hx : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ p x fun (n : ℕ) ↦ f (v n) x

Tactic:
hx.comp hv

Premises used: Filter.Tendsto.comp
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ p x fun (n : ℕ) ↦ f (v n) x) x} x}
      a
h₁ h₂ : ∀ (x : α) (hx : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))), p x fun (n : ℕ) ↦ f (v n) x
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x

Tactic:
filter_upwards [h_tendsto] with x hx using hx.comp hv
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : TopologicalSpace β
inst_2 : PseudoMetrizableSpace β
inst_3 : MeasurableSpace β
inst_4 : BorelSpace β
ι : Type u_3
μ : Measure α
f : ι → α → β
g : α → β
u : Filter ι
hu : u.NeBot
inst_5 : u.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
v : ℕ → ι
hv : Tendsto v atTop u
h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ
p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x))
⊢ ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x

Tactic:
have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv