awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
⊢ AEMeasurable (G ∘ f) μ

Tactic:
have : AEMeasurable (G ∘ f) μ := AEMeasurable.subtype_mk H.aemeasurable
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
this : AEMeasurable (G ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
hG.measurableEmbedding.aemeasurable_comp_iff.1 this

Premises used: MeasurableEmbedding.aemeasurable_comp_iff, Iff.mp, Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
G : β → (↑(range g) : Type u_3) := rangeFactorization g
hG : IsClosedEmbedding G
this : AEMeasurable (G ∘ f) μ
⊢ AEMeasurable f μ

Tactic:
exact hG.measurableEmbedding.aemeasurable_comp_iff.1 this

Premises used: MeasurableEmbedding.aemeasurable_comp_iff, Iff.mp, Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
refine_2 :
  ∀ (t : Set γ) (ht : IsSeparable t) (h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t),
    ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
rcases (aestronglyMeasurable_iff_aemeasurable_separable.1 H).2 with ⟨t, ht, h't⟩

Premises used: aestronglyMeasurable_iff_aemeasurable_separable, And.right, Iff.mp
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
t : Set γ
ht : IsSeparable t
h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩

Premises used: Topology.IsEmbedding.isSeparable_preimage, Set.preimage, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : TopologicalSpace β
inst_1 : TopologicalSpace γ
m₀ : MeasurableSpace α
μ : Measure α
inst_2 : PseudoMetrizableSpace β
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 : AEStronglyMeasurable.{u_1, u_3} (β := γ) (fun (x : α) ↦ g (f x)) μ
t : Set γ
ht : IsSeparable t
h't : ∀ᵐ (x : α) ∂μ, g (f x) ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t

Tactic:
exact ⟨g ⁻¹' t, hg.isSeparable_preimage ht, h't⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
⊢ let this := borel β;
  BorelSpace β

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

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

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_1 : AEMeasurable g μ
refine_2 : ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ AEStronglyMeasurable g μ

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

Premises used: Iff.mpr, aestronglyMeasurable_iff_aemeasurable_separable, And.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEMeasurable g μ

Tactic:
aemeasurable_of_tendsto_metrizable_ae _ (fun n => (hf n).aemeasurable) lim

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae _ (fun n => (hf n).aemeasurable) lim

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
refine_2 : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u), ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

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

Premises used: Filter.exists_seq_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
⊢ ∀ (n : ℕ), ∃ (t : Set β), IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ

Tactic:
have : ∀ n : ℕ, ∃ t : Set β, IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ := fun n =>
      (aestronglyMeasurable_iff_aemeasurable_separable.1 (hf (v n))).2
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this_1 : MeasurableSpace β := borel β
this_2 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
this : ∀ (n : ℕ), ∃ (t : Set β), IsSeparable t ∧ f (v n) ⁻¹' t ∈ ae μ
refine_2 :
  ∀ (t : (n : ℕ) → Set β) (t_sep : ∀ (n : ℕ), IsSeparable (t n)) (ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ),
    ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
choose t t_sep ht using this
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩

Premises used: TopologicalSpace.IsSeparable.closure, TopologicalSpace.IsSeparable.iUnion, closure, And.intro, Exists.intro, Set.iUnion
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
refine_2 : ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
⊢ ∃ (t : Set β), IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, g x ∈ t

Tactic:
refine ⟨closure (⋃ i, t i), .closure <| .iUnion t_sep, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
h :
  ∀ (x : α) (hx : ∀ (i : ℕ), f (v i) x ∈ t i) (h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))),
    Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)
⊢ ∀ᵐ (x : α) ∂μ, Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)

Tactic:
filter_upwards [ae_all_iff.2 ht, lim] with x hx h'x

Premises used: Iff.mpr, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
h : ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_1)
⊢ Membership.mem (γ := Set β) (closure[inst] (⋃ (i : ℕ), t i)) (g x)

Tactic:
apply mem_closure_of_tendsto (h'x.comp hv)

Premises used: Filter.Tendsto.comp, mem_closure_of_tendsto
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
n : ℕ
⊢ Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) n)

Tactic:
mem_iUnion_of_mem n (hx n)

Premises used: Set.mem_iUnion_of_mem
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
ι : Type u_5
inst_1 : PseudoMetrizableSpace β
u : Filter ι
inst_2 : u.NeBot
inst_3 : u.IsCountablyGenerated
f : ι → α → β
g : α → β
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
v : ℕ → ι
hv : Tendsto v atTop u
t : (n : ℕ) → Set β
t_sep : ∀ (n : ℕ), IsSeparable (t n)
ht : ∀ (n : ℕ), f (v n) ⁻¹' t n ∈ ae μ
x : α
hx : ∀ (i : ℕ), f (v i) x ∈ t i
h'x : Tendsto (fun (n : ι) ↦ f n x) u (𝓝 (g x))
h :
  ∀ (a : ℕ),
    Membership.mem (γ := Set ℕ)
      {x_1 : ℕ | (fun (x_2 : ℕ) ↦ Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_2)) x_1} a
h₁ h₂ : ∀ (n : ℕ), Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) n)
⊢ ∀ᶠ (x_1 : ℕ) in atTop, Membership.mem (γ := Set β) (⋃ (i : ℕ), t i) (((fun (n : ι) ↦ f n x) ∘ v) x_1)

Tactic:
filter_upwards with n using mem_iUnion_of_mem n (hx n)
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
⊢ let this := borel β;
  BorelSpace β

Tactic:
borelize β
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
⊢ ∃ (g : α → β), Measurable g ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
measurable_limit_of_tendsto_metrizable_ae (fun n => (hf n).aemeasurable) h_ae_tendsto

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, measurable_limit_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
obtain :
  ∀ (g : α → β),
    Measurable g →
      ∀ (hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))),
        ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))

Tactic:
obtain ⟨g, _, hg⟩ :
    ∃ g : α → β, Measurable g ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) :=
    measurable_limit_of_tendsto_metrizable_ae (fun n => (hf n).aemeasurable) h_ae_tendsto

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, measurable_limit_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ AEStronglyMeasurable g μ

Tactic:
have Hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hg
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))

Tactic:
⟨Hg.mk g, Hg.stronglyMeasurable_mk, ?_⟩

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
refine : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
⊢ ∃ (f_lim : α → β), StronglyMeasurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (f_lim x))

Tactic:
refine ⟨Hg.mk g, Hg.stronglyMeasurable_mk, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
h :
  ∀ (x : α) (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))) (h'x : g x = AEStronglyMeasurable.mk g Hg x),
    Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))

Tactic:
filter_upwards [hg, Hg.ae_eq_mk] with x hx h'x

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_1
β : Type u_2
inst : TopologicalSpace β
m₀ : MeasurableSpace α
μ : Measure α
inst_1 : PseudoMetrizableSpace β
f : ℕ → α → β
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 l)
this : MeasurableSpace β := borel β
this_1 : BorelSpace β
g : α → β
left : Measurable g
hg : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
Hg : AEStronglyMeasurable g μ
x : α
hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
h'x : g x = AEStronglyMeasurable.mk g Hg x
h h₁ h₂ h₃ :
  ∀ (hx : Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x)))
    (h'x : g x = AEStronglyMeasurable.mk g Hg x),
    Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (AEStronglyMeasurable.mk g Hg x))

Tactic:
rwa [h'x] at hx
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
hf : AEStronglyMeasurable f μ
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
obtain :
  ∀ (f' : α → β) (hf' : StronglyMeasurable f') (hff' : f =ᶠ[ae μ] f'),
    ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g

Tactic:
obtain ⟨f', hf', hff'⟩ := hf
-- Module: Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Goal:
α : Type u_5
β : Type u_6
inst : TopologicalSpace β
inst_1 : PseudoMetrizableSpace β
mb : MeasurableSpace β
inst_2 : BorelSpace β
m : MeasurableSpace α
μ : Measure α
f : α → β
s : Set β
hs : MeasurableSet s
h_nonempty : s.Nonempty
h_mem : ∀ᵐ (x : α) ∂μ, f x ∈ s
f' : α → β
hf' : StronglyMeasurable f'
hff' : f =ᶠ[ae μ] f'
⊢ ∃ (g : α → β), StronglyMeasurable g ∧ (∀ (x : α), g x ∈ s) ∧ f =ᶠ[ae μ] g

Tactic:
⟨(f' ⁻¹' s).piecewise f' (fun _ ↦ h_nonempty.some), ?meas, ?subset, ?ae_eq⟩

Premises used: Set.preimage, And.intro, Exists.intro, Set.piecewise, Set.Nonempty.some