awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ AEMeasurable g μ

Tactic:
⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩

Premises used: Iff.mpr, measurable_of_tendsto_metrizable', AEMeasurable, aeSeq.measurable, tendsto_pi_nhds, Filter.atTop, And.intro, Exists.intro
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
refine_1 : ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
refine_2 : g =ᶠ[ae μ] aeSeqLim
⊢ AEMeasurable g μ

Tactic:
refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun 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
μ : 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
refine_1 :
  Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))
⊢ Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))

Tactic:
simp_rw [aeSeqLim, aeSeq]

Premises used: aeSeq
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
pos : ∀ (hx : x ∈ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))
neg : ∀ (hx : x ∉ aeSeqSet h'f p), Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)
⊢ Tendsto (fun (i : ℕ) ↦ if x ∈ aeSeqSet h'f p then AEMeasurable.mk (f (v i)) ⋯ x else Nonempty.some ⋯) atTop
    (𝓝 (if x ∈ aeSeqSet h'f p then g x else ⋯.some))

Tactic:
split_ifs with hx
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
pos : Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))
⊢ Tendsto (fun (i : ℕ) ↦ AEMeasurable.mk (f (v i)) ⋯ x) atTop (𝓝 (g x))

Tactic:
simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]

Premises used: aeSeq.mk_eq_fun_of_mem_aeSeqSet
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))

Tactic:
@aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx

Premises used: aeSeq.fun_prop_of_mem_aeSeqSet
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∈ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ f (v i) x) atTop (𝓝 (g x))

Tactic:
exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx

Premises used: aeSeq.fun_prop_of_mem_aeSeqSet
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)

Tactic:
tendsto_const_nhds

Premises used: tendsto_const_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
μ : 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
x : α
hx : x ∉ aeSeqSet h'f p
⊢ Tendsto (fun (i : ℕ) ↦ Nonempty.some ⋯) atTop (𝓝 ⋯.some)

Tactic:
exact tendsto_const_nhds

Premises used: tendsto_const_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
μ : 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᶠ[ae μ] aeSeqLim

Tactic:
(ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: Nonempty.some, Nonempty.intro, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, OfNat.ofNat, Filter.EventuallyEq.symm
-- 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))
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x
aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some
⊢ g =ᶠ[ae μ] aeSeqLim

Tactic:
exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: Nonempty.some, Nonempty.intro, aeSeq.measure_compl_aeSeqSet_eq_zero, MeasureTheory.ite_ae_eq_of_measure_compl_zero, aeSeqSet, OfNat.ofNat, Filter.EventuallyEq.symm
-- 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 μ
rcases₁ rcases₂ : ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ), AEMeasurable g μ
rcases₃ rcases₄ :
  ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
    let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
    ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x), AEMeasurable g μ
refine_1 :
  ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
    let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
    ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x),
      let aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some;
      ∀ (x : α), Tendsto (fun (i : ℕ) ↦ aeSeq h'f p i x) atTop (𝓝 (aeSeqLim x))
refine_2 refine_2₁ :
  ∀ (v : ℕ → ι) (hv : Tendsto v atTop u) (h'f : ∀ (n : ℕ), AEMeasurable (f (v n)) μ),
    let p : α → (ℕ → β) → Prop := fun (x : α) (f' : ℕ → β) ↦ Tendsto (fun (n : ℕ) ↦ f' n) atTop (𝓝 (g x));
    ∀ (hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ℕ) ↦ f (v n) x),
      let aeSeqLim : (x : α) → β := fun (x : α) ↦ if x ∈ aeSeqSet h'f p then g x else ⋯.some;
      g =ᶠ[ae μ] aeSeqLim
⊢ AEMeasurable g μ

Tactic:
classical
  rcases u.exists_seq_tendsto with ⟨v, hv⟩
  have h'f : ∀ n, AEMeasurable (f (v n)) μ := fun n => hf (v n)
  set p : α → (ℕ → β) → Prop := fun x f' => Tendsto (fun n => f' n) atTop (𝓝 (g x))
  have hp : ∀ᵐ x ∂μ, p x fun n => f (v n) x := by
    filter_upwards [h_tendsto] with x hx using hx.comp hv
  set aeSeqLim := fun x => ite (x ∈ aeSeqSet h'f p) (g x) (⟨f (v 0) x⟩ : Nonempty β).some
  refine
    ⟨aeSeqLim,
      measurable_of_tendsto_metrizable' atTop (aeSeq.measurable h'f p)
        (tendsto_pi_nhds.mpr fun x => ?_),
      ?_⟩
  · simp_rw [aeSeqLim, aeSeq]
    split_ifs with hx
    · simp_rw [aeSeq.mk_eq_fun_of_mem_aeSeqSet h'f hx]
      exact @aeSeq.fun_prop_of_mem_aeSeqSet _ α β _ _ _ _ _ h'f x hx
    · exact tendsto_const_nhds
  · exact
      (ite_ae_eq_of_measure_compl_zero g (fun x => (⟨f (v 0) x⟩ : Nonempty β).some) (aeSeqSet h'f p)
          (aeSeq.measure_compl_aeSeqSet_eq_zero h'f hp)).symm

Premises used: tendsto_const_nhds, aeSeq, nhds, Filter.atTop, Filter.Tendsto, 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 β
μ : Measure α
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
aemeasurable_of_tendsto_metrizable_ae atTop hf h_ae_tendsto

Premises used: Filter.atTop, aemeasurable_of_tendsto_metrizable_ae
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
⊢ ∃ (u : ℕ → ℝ), StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0)

Tactic:
exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
obtain : ∀ (u : ℕ → ℝ) (u_pos : ∀ (n : ℕ), 0 < u n) (u_lim : Tendsto u atTop (𝓝 0)), AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
obtain ⟨u, -, u_pos, u_lim⟩ :
    ∃ u : ℕ → ℝ, StrictAnti u ∧ (∀ n : ℕ, 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
    exists_seq_strictAnti_tendsto (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
choose :
  ∀ (f : (n : ℕ) → α → β) (Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n),
    AEMeasurable g μ
⊢ AEMeasurable g μ

Tactic:
choose f Hf using fun n : ℕ => hf (u n) (u_pos n)
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
⊢ ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n

Tactic:
have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
h : ∀ (a : α), (∀ (n : ℕ), dist (f n a) (g a) ≤ u n) → Tendsto (fun (n : ℕ) ↦ f n a) atTop (𝓝 (g a))
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
filter_upwards [this]
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
h : Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (f b x) (g x)) atTop (𝓝 0)
⊢ Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
rw [tendsto_iff_dist_tendsto_zero]

Premises used: tendsto_iff_dist_tendsto_zero
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (f b x) (g x)) atTop (𝓝 0)

Tactic:
squeeze_zero (fun n => dist_nonneg) hx u_lim

Premises used: squeeze_zero, dist_nonneg
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
x : α
hx : ∀ (n : ℕ), dist (f n x) (g x) ≤ u n
⊢ Tendsto (β := ℝ) (fun (b : ℕ) ↦ dist (f b x) (g x)) atTop (𝓝 0)

Tactic:
exact squeeze_zero (fun n => dist_nonneg) hx u_lim

Premises used: squeeze_zero, dist_nonneg
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
⊢ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))

Tactic:
have : ∀ᵐ x ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x)) := by
    have : ∀ᵐ x ∂μ, ∀ n, dist (f n x) (g x) ≤ u n := ae_all_iff.2 fun n => (Hf n).2
    filter_upwards [this]
    intro x hx
    rw [tendsto_iff_dist_tendsto_zero]
    exact squeeze_zero (fun n => dist_nonneg) hx u_lim
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this

Premises used: aemeasurable_of_tendsto_metrizable_ae', And.left
-- Module: Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
Goal:
α : Type u_1
inst : MeasurableSpace α
β : Type u_3
inst_1 : MeasurableSpace β
inst_2 : PseudoMetricSpace β
inst_3 : BorelSpace β
μ : Measure α
g : α → β
hf : ∀ ε > 0, ∃ (f : α → β), AEMeasurable f μ ∧ ∀ᵐ (x : α) ∂μ, dist (f x) (g x) ≤ ε
u : ℕ → ℝ
u_pos : ∀ (n : ℕ), 0 < u n
u_lim : Tendsto u atTop (𝓝 0)
f : (n : ℕ) → α → β
Hf : ∀ (n : ℕ), AEMeasurable (f n) μ ∧ ∀ᵐ (x : α) ∂μ, dist (f n x) (g x) ≤ u n
this : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae' (fun n => (Hf n).1) this

Premises used: aemeasurable_of_tendsto_metrizable_ae', And.left
-- 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 β
μ : Measure α
inst_5 : μ.IsComplete
f : ℕ → α → β
g : α → β
hf : ∀ (n : ℕ), Measurable (f n)
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ℕ) ↦ f n x) atTop (𝓝 (g x))
⊢ Measurable g

Tactic:
aemeasurable_iff_measurable.mp
    (aemeasurable_of_tendsto_metrizable_ae' (fun i => (hf i).aemeasurable) h_ae_tendsto)

Premises used: Measurable.aemeasurable, aemeasurable_iff_measurable, aemeasurable_of_tendsto_metrizable_ae', Iff.mp
-- 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
inst_5 : Countable ι
inst_6 : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst_7 : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l)
inhabit :
  ∀ (inhabited_h : Inhabited ι),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
⊢ ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))

Tactic:
inhabit ι