awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
X : Type u_5
Y : Type u_6
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this_1 : MeasurableSpace α := borel α
this_2 : BorelSpace α
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ IsSeparable (range f)

Tactic:
IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)

Premises used: IsCompact.isSeparable, HasCompactSupport.isCompact_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
X : Type u_5
Y : Type u_6
inst : Zero α
inst_1 : TopologicalSpace X
inst_2 : TopologicalSpace Y
inst_3 : MeasurableSpace X
inst_4 : MeasurableSpace Y
inst_5 : OpensMeasurableSpace X
inst_6 : OpensMeasurableSpace Y
inst_7 : TopologicalSpace α
inst_8 : PseudoMetrizableSpace α
f : X × Y → α
hf : Continuous[instTopologicalSpaceProd, inst_7] f
h'f : HasCompactSupport f
this_1 : MeasurableSpace α := borel α
this_2 : BorelSpace α
this : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
⊢ IsSeparable (range f)

Tactic:
exact IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)

Premises used: IsCompact.isSeparable, HasCompactSupport.isCompact_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β γ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this₁ :
  let this := borel β;
  BorelSpace β
⊢ let this := borel γ;
  BorelSpace γ

Tactic:
borelize β γ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, Continuous.comp_stronglyMeasurable, And.intro, Iff.intro, Topology.IsEmbedding.continuous
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
refine_1 : ∀ (H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)), Measurable f
refine_2 : ∀ (H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)), IsSeparable (range f)
⊢ (StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)) ↔ StronglyMeasurable f

Tactic:
refine
    ⟨fun H => stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩, fun H =>
      hg.continuous.comp_stronglyMeasurable H⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
rw : IsClosed[instTopologicalSpaceSubtype] univ
⊢ IsClosed[instTopologicalSpaceSubtype] (range G)

Tactic:
rw [rangeFactorization_surjective.range_eq]

Premises used: Function.Surjective.range_eq, Set.rangeFactorization_surjective
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ IsClosed[instTopologicalSpaceSubtype] univ

Tactic:
isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ IsClosed[instTopologicalSpaceSubtype] univ

Tactic:
exact isClosed_univ

Premises used: isClosed_univ
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
⊢ IsClosedEmbedding G

Tactic:
have hG : IsClosedEmbedding G :=
      { hg.codRestrict _ _ with
        isClosed_range := by
          rw [rangeFactorization_surjective.range_eq]
          exact isClosed_univ }
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ Measurable (G ∘ f)

Tactic:
have : Measurable (G ∘ f) := Measurable.subtype_mk H.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this_1 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
this_4 : MeasurableSpace γ := borel γ
this_5 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
this : Measurable (G ∘ f)
⊢ Measurable f

Tactic:
hG.measurableEmbedding.measurable_comp_iff.1 this

Premises used: Iff.mp, Topology.IsClosedEmbedding.measurableEmbedding, MeasurableEmbedding.measurable_comp_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this_1 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
this_4 : MeasurableSpace γ := borel γ
this_5 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
this : Measurable (G ∘ f)
⊢ Measurable f

Tactic:
exact hG.measurableEmbedding.measurable_comp_iff.1 this

Premises used: Iff.mp, Topology.IsClosedEmbedding.measurableEmbedding, MeasurableEmbedding.measurable_comp_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
this_3 : MeasurableSpace γ := borel γ
this_4 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
⊢ IsSeparable (g ⁻¹' range (g ∘ f))

Tactic:
have : IsSeparable (g ⁻¹' range (g ∘ f)) := hg.isSeparable_preimage H.isSeparable_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
inst_2 : TopologicalSpace γ
inst_3 : PseudoMetrizableSpace γ
g : β → γ
f : α → β
hg : IsEmbedding g
this_1 : PseudoMetricSpace γ := pseudoMetrizableSpacePseudoMetric γ
this_2 : MeasurableSpace β := borel β
this_3 : BorelSpace β
this_4 : MeasurableSpace γ := borel γ
this_5 : BorelSpace γ
H : StronglyMeasurable.{u_1, u_3} (β := γ) fun (x : α) ↦ g (f x)
this : IsSeparable (g ⁻¹' range (g ∘ f))
refine_2 : ∀ (this : IsSeparable (g ⁻¹' g '' range f)), IsSeparable (range f)
refine_2₁ refine_2₂ refine_2₃ refine_2₄ : ∀ (this : IsSeparable (range f)), IsSeparable (range f)
⊢ IsSeparable (range f)

Tactic:
rwa [range_comp, hg.injective.preimage_image] at this

Premises used: Set.range_comp, Function.Injective.preimage_image, Topology.IsEmbedding.injective
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ StronglyMeasurable g

Tactic:
stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : Measurable g
refine_2 : IsSeparable (range g)
⊢ StronglyMeasurable g

Tactic:
refine stronglyMeasurable_iff_measurable_separable.2 ⟨?_, ?_⟩

Premises used: Iff.mpr, stronglyMeasurable_iff_measurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ Measurable g

Tactic:
measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim

Premises used: measurable_of_tendsto_metrizable', MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ Measurable g

Tactic:
exact measurable_of_tendsto_metrizable' u (fun i => (hf i).measurable) lim

Premises used: measurable_of_tendsto_metrizable', MeasureTheory.StronglyMeasurable.measurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_2 : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), IsSeparable (range g)
⊢ IsSeparable (range g)

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

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))

Tactic:
have : IsSeparable (closure (⋃ i, range (f (v i)))) :=
      .closure <| .iUnion fun i => (hf (v i)).isSeparable_range
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
refine_2 : range g ⊆ closure[inst] (⋃ (i : ℕ), range (f (v i)))
⊢ IsSeparable (range g)

Tactic:
apply this.mono

Premises used: TopologicalSpace.IsSeparable.mono
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : Tendsto f u (𝓝 g)
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
refine_2 :
  ∀ (lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))),
    let this := borel β;
    BorelSpace β →
      ∀ (v : ℕ → ι) (hv : Tendsto v atTop u)
        (this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))) (x : α),
        Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)

Tactic:
rw [tendsto_pi_nhds] at lim

Premises used: tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
refine_2 :
  ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) x_1)
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), range (f (v i)))) (g x)

Tactic:
apply mem_closure_of_tendsto ((lim x).comp hv)

Premises used: Filter.Tendsto.comp, mem_closure_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
refine_2 : ∀ (n : ℕ), Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) n)
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) x_1)

Tactic:
filter_upwards with n
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
refine_2 : ((fun (i : ι) ↦ f i x) ∘ v) n ∈ range (f (v n))
⊢ Membership.mem (γ := Set β) (⋃ (i : ℕ), range (f (v i))) (((fun (i : ι) ↦ f i x) ∘ v) n)

Tactic:
apply mem_iUnion_of_mem n

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun (i : ι) ↦ f i x) ∘ v) n ∈ range (f (v n))

Tactic:
mem_range_self _

Premises used: Set.mem_range_self, Set.Mem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
ι : Type u_5
m : MeasurableSpace α
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), StronglyMeasurable (f i)
lim : ∀ (x : α), Tendsto (fun (i : ι) ↦ f i x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : IsSeparable.{u_2} (α := β) (closure[inst] (⋃ (i : ℕ), range (f (v i))))
x : α
n : ℕ
⊢ ((fun (i : ι) ↦ f i x) ∘ v) n ∈ range (f (v n))

Tactic:
exact mem_range_self _

Premises used: Set.mem_range_self
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
⊢ StronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => ?_⟩

Premises used: MeasureTheory.StronglyMeasurable.approx, Exists.intro, MeasureTheory.StronglyMeasurable, MeasureTheory.SimpleFunc.piecewise
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
refine :
  ∀ (x_1 : α),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x_1)
      atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x_1))
⊢ StronglyMeasurable (s.piecewise (β := fun (a : α) ↦ β) f g)

Tactic:
refine ⟨fun n => SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n), fun x => ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
pos :
  ∀ (hx : x ∈ s),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
      atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
neg :
  ∀ (hx : x ∉ s),
    Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
      atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))

Tactic:
by_cases hx : x ∈ s
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∈ s
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))

Tactic:
simpa [@Set.piecewise_eq_of_mem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
      hx] using hf.tendsto_approx x

Premises used: Set.piecewise_eq_of_mem, MeasureTheory.StronglyMeasurable.tendsto_approx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Goal:
α : Type u_1
β : Type u_2
f g : α → β
m : MeasurableSpace α
inst : TopologicalSpace β
s : Set α
x_1 : DecidablePred fun (x : α) ↦ x ∈ s
hs : MeasurableSet s
hf : StronglyMeasurable f
hg : StronglyMeasurable g
x : α
hx : x ∉ s
⊢ Tendsto (fun (n : ℕ) ↦ ((fun (n : ℕ) ↦ SimpleFunc.piecewise s hs (hf.approx n) (hg.approx n)) n : (a : α) → β) x)
    atTop (𝓝 (s.piecewise (β := fun (a : α) ↦ β) f g x))

Tactic:
simpa [@Set.piecewise_eq_of_notMem _ _ _ _ _ (fun _ => Classical.propDecidable _) _ hx,
      hx] using hg.tendsto_approx x

Premises used: Set.piecewise_eq_of_notMem, MeasureTheory.StronglyMeasurable.tendsto_approx