awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Set.Countable (α := ℝ) univ

Tactic:
Cardinal.not_countable_real

Premises used: Cardinal.not_countable_real
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
hα : ¬Countable α
⊢ ¬Set.Countable (α := ℝ) univ

Tactic:
exact Cardinal.not_countable_real

Premises used: Cardinal.not_countable_real
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
obtain : ∀ (s : Set ℝ) (hs : MeasurableSet s) (e : α ≃ᵐ (↑s : Type)), ∃ (f : α → ℝ), MeasurableEmbedding f
⊢ ∃ (f : α → ℝ), MeasurableEmbedding f

Tactic:
obtain ⟨s, hs, ⟨e⟩⟩ := exists_subset_real_measurableEquiv α

Premises used: MeasureTheory.exists_subset_real_measurableEquiv
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ (↑s : Type)
⊢ ∃ (f : α → ℝ), MeasurableEmbedding f

Tactic:
⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩

Premises used: Function.comp, Exists.intro, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : StandardBorelSpace α
s : Set ℝ
hs : MeasurableSet s
e : α ≃ᵐ (↑s : Type)
⊢ ∃ (f : α → ℝ), MeasurableEmbedding f

Tactic:
exact ⟨(↑) ∘ e, (MeasurableEmbedding.subtype_coe hs).comp e.measurableEmbedding⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
Ω : Type u_2
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
⊢ MeasurableEmbedding (embeddingReal Ω)

Tactic:
(exists_measurableEmbedding_real Ω).choose_spec

Premises used: Exists.choose_spec, MeasureTheory.embeddingReal, MeasureTheory.exists_measurableEmbedding_real
-- Module: Mathlib.MeasureTheory.Constructions.Polish.EmbeddingReal
Goal:
Ω : Type u_2
inst : MeasurableSpace Ω
inst_1 : StandardBorelSpace Ω
⊢ Measurable (embeddingReal Ω)

Tactic:
(measurableEmbedding_embeddingReal Ω).measurable

Premises used: MeasureTheory.measurableEmbedding_embeddingReal, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
    MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) ⊥ (𝓝 c)}
inr : ∀ (hl : l.NeBot), MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}

Tactic:
obtain rfl | hl := eq_or_neBot l

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
f : ι → X → E
inst_3 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inst_4 : IsCountablyGenerated.{u_1} (α := ι) ⊥
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) ⊥ (𝓝 c)}

Tactic:
simp_all
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
⊢ let this := borel E;
  BorelSpace E

Tactic:
borelize E
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
⊢ SecondCountableTopology.{u_3} (↑s : Type u_3)

Tactic:
have : SecondCountableTopology s := @UniformSpace.secondCountable_of_separable s _ _
    (IsSeparable.iUnion (fun i ↦ (hf i).isSeparable_range)).closure.separableSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this : SecondCountableTopology.{u_3} (↑s : Type u_3)
⊢ IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)

Tactic:
have : IsCompletelyPseudoMetrizableSpace s := isClosed_closure.isCompletelyPseudoMetrizableSpace
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
⊢ ∀ (i : ι), Measurable (g i)

Tactic:
have mg i : Measurable (g i) := (hf i).measurable.subtype_mk
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)}

Tactic:
MeasureTheory.measurableSet_exists_tendsto (l := l) mg

Premises used: MeasureTheory.measurableSet_exists_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
h :
  ∀ (x : X),
    (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) ↔
      ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)
⊢ MeasurableSet.{u_2} (α := X) {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}

Tactic:
convert! MeasureTheory.measurableSet_exists_tendsto (l := l) mg with x

Premises used: MeasureTheory.measurableSet_exists_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
⊢ (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) ↔
    ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)

Tactic:
⟨fun ⟨c, hc⟩ ↦ ⟨⟨c, ?_⟩, tendsto_subtype_rng.2 hc⟩,
    fun ⟨c, hc⟩ ↦ ⟨c, tendsto_subtype_rng.1 hc⟩⟩

Premises used: Iff.mpr, Exists, nhds, _private.0.MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto.match_1, Subtype.mk, Filter.Tendsto, Iff.intro, Exists.intro, Iff.mp, tendsto_subtype_rng, Subtype.val, _private.0.MeasureTheory.StronglyMeasurable.measurableSet_exists_tendsto.match_2
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
h :
  (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) →
    ∀ (c : E) (hc : Tendsto (fun (x_2 : ι) ↦ f x_2 x) l (𝓝 c)), c ∈ s
⊢ (∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)) ↔
    ∃ (c : (↑s : Type u_3)), Tendsto (fun (n : ι) ↦ g n x) l (𝓝 c)

Tactic:
refine ⟨fun ⟨c, hc⟩ ↦ ⟨⟨c, ?_⟩, tendsto_subtype_rng.2 hc⟩,
    fun ⟨c, hc⟩ ↦ ⟨c, tendsto_subtype_rng.1 hc⟩⟩
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
h : ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)
c : E
hc : Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)
⊢ c ∈ s

Tactic:
mem_closure_of_tendsto hc (Eventually.of_forall fun i ↦ mem_iUnion.2 ⟨i, ⟨x, rfl⟩⟩)

Premises used: Iff.mpr, Set.Mem, Set.mem_iUnion, Filter.Eventually.of_forall, Exists.intro, rfl, mem_closure_of_tendsto
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
inst_4 : IsCompletelyPseudoMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
this_1 : MeasurableSpace E := borel E
this_2 : BorelSpace E
this_3 : UpgradedIsCompletelyPseudoMetrizableSpace E := upgradeIsCompletelyPseudoMetrizable E
s : Set E := closure[inst_1] (⋃ (i : ι), range (f i))
this_4 : SecondCountableTopology.{u_3} (↑s : Type u_3)
this : IsCompletelyPseudoMetrizableSpace.{u_3} (↑s : Type u_3)
g : (i : ι) → (x : X) → (↑s : Type u_3) := fun (i : ι) (x : X) ↦ Subtype.mk (p := fun (x : E) ↦ x ∈ s) (f i x) ⋯
mg : ∀ (i : ι), Measurable (g i)
x : X
h : ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)
c : E
hc : Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)
⊢ c ∈ s

Tactic:
exact mem_closure_of_tendsto hc (Eventually.of_forall fun i ↦ mem_iUnion.2 ⟨i, ⟨x, rfl⟩⟩)
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inl :
  ∀ [IsCountablyGenerated.{u_1} (α := ι) ⊥],
    StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ limUnder ⊥ fun (x_1 : ι) ↦ f x_1 x
inr : ∀ (hl : l.NeBot), StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x

Tactic:
obtain rfl | hl := eq_or_neBot l

Premises used: Filter.eq_or_neBot, rfl
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
f : ι → X → E
hE : Nonempty E
inst_3 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
inst_4 : IsCountablyGenerated.{u_1} (α := ι) ⊥
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : X) ↦ limUnder ⊥ fun (x_1 : ι) ↦ f x_1 x

Tactic:
simpa [limUnder, Filter.map_bot] using stronglyMeasurable_const

Premises used: MeasureTheory.stronglyMeasurable_const, Filter.map_bot, Filter.limUnder
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
⊢ MeasurableSet conv

Tactic:
have mconv : MeasurableSet conv := StronglyMeasurable.measurableSet_exists_tendsto hf
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)

Tactic:
stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_

Premises used: measurable_subtype_coe, stronglyMeasurable_of_tendsto, MeasureTheory.StronglyMeasurable.comp_measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
refine :
  Tendsto (β := (↑conv : Type u_2) → E) (fun (i : ι) ↦ f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) l
    (𝓝 fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X))
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)

Tactic:
refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_

Premises used: measurable_subtype_coe, stronglyMeasurable_of_tendsto, MeasureTheory.StronglyMeasurable.comp_measurable
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ Tendsto (β := (↑conv : Type u_2) → E) (fun (i : ι) ↦ f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) l
    (𝓝 fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X))

Tactic:
tendsto_pi_nhds.2 fun x ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
refine :
  ∀ (x : (↑conv : Type u_2)),
    Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
      (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
⊢ Tendsto (β := (↑conv : Type u_2) → E) (fun (i : ι) ↦ f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) l
    (𝓝 fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X))

Tactic:
refine tendsto_pi_nhds.2 fun x ↦ ?_

Premises used: Iff.mpr, tendsto_pi_nhds
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
x : (↑conv : Type u_2)
obtain :
  ∀ (c : E) (hc : Tendsto (fun (x_1 : ι) ↦ f x_1 (↑x : X)) l (𝓝 c)),
    Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
      (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))
⊢ Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))

Tactic:
obtain ⟨c, hc⟩ := x.2

Premises used: Subtype.property
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
x : (↑conv : Type u_2)
c : E
hc : Tendsto (fun (x_1 : ι) ↦ f x_1 (↑x : X)) l (𝓝 c)
rwa rwa₁ rwa₂ rwa₃ : Tendsto (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l (𝓝 c)
⊢ Tendsto.{u_1, u_3} (β := E) (fun (i : ι) ↦ (f i ∘ Subtype.val (p := fun (x : X) ↦ x ∈ conv)) x) l
    (𝓝 (l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)))

Tactic:
rwa [hc.limUnder_eq]

Premises used: Filter.Tendsto.limUnder_eq
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
⊢ StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)

Tactic:
have hconv : StronglyMeasurable (fun x : conv ↦ limUnder l (f · x)) := by
    refine stronglyMeasurable_of_tendsto l
      (fun i ↦ (hf i).comp_measurable measurable_subtype_coe) ?_
    refine tendsto_pi_nhds.2 fun x ↦ ?_
    obtain ⟨c, hc⟩ := x.2
    rwa [hc.limUnder_eq]
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
h :
  ∀ (x : X),
    Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
      (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
        (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
⊢ Eq (α := (x : X) → E) (fun (x : X) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) fun (x : X) ↦ e)

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Constructions.Polish.StronglyMeasurable
Goal:
ι : Type u_1
X : Type u_2
E : Type u_3
inst : MeasurableSpace X
inst_1 : TopologicalSpace E
inst_2 : Countable ι
l : Filter ι
inst_3 : l.IsCountablyGenerated
f : ι → X → E
hE : Nonempty E
inst_4 : IsCompletelyMetrizableSpace E
hf : ∀ (i : ι), StronglyMeasurable (f i)
hl : l.NeBot
e : E := Classical.choice hE
conv : Set X := {x : X | ∃ (c : E), Tendsto (fun (x_1 : ι) ↦ f x_1 x) l (𝓝 c)}
mconv : MeasurableSet conv
hconv : StronglyMeasurable.{u_2, u_3} (β := E) fun (x : (↑conv : Type u_2)) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)
x : X
pos :
  ∀ (hx : x ∈ conv),
    Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
      (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
        (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
neg :
  ∀ (hx : x ∉ conv),
    Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
      (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
        (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)
⊢ Eq.{u_3 + 1} (α := E) (l.limUnder fun (x_1 : ι) ↦ f x_1 x)
    (Function.extend (Subtype.val (p := fun (x : X) ↦ x ∈ conv))
      (fun (x : { x : X // x ∈ conv }) ↦ l.limUnder fun (x_1 : ι) ↦ f x_1 (↑x : X)) (fun (x : X) ↦ e) x)

Tactic:
by_cases hx : x ∈ conv