α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ f atTop g
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ TendstoInMeasure μ f atTop g
have hg : AEStronglyMeasurable g μ := aestronglyMeasurable_of_tendsto_ae _ hf hfg
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) (_ : AEStronglyMeasurable (f i) μ)) atTop
    (AEStronglyMeasurable.mk g hg)
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ f atTop g
refine' TendstoInMeasure.congr (fun i => (hf i).ae_eq_mk.symm) hg.ae_eq_mk.symm _
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ TendstoInMeasure μ (fun i => AEStronglyMeasurable.mk (f i) (_ : AEStronglyMeasurable (f i) μ)) atTop
    (AEStronglyMeasurable.mk g hg)
refine' tendstoInMeasure_of_tendsto_ae_of_stronglyMeasurable
  (fun i => (hf i).stronglyMeasurable_mk) hg.stronglyMeasurable_mk _
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
have hf_eq_ae : ∀ᵐ x ∂μ, ∀ n, (hf n).mk (f n) x = f n x :=
  ae_all_iff.mpr fun n => (hf n).ae_eq_mk.symm
case h
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
    (𝓝 (AEStronglyMeasurable.mk g hg x))
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
⊢ ∀ᵐ (x : α) ∂μ,
    Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
      (𝓝 (AEStronglyMeasurable.mk g hg x))
filter_upwards [hf_eq_ae, hg.ae_eq_mk, hfg] with x hxf hxg hxfg
case h
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
case h
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x) atTop
    (𝓝 (AEStronglyMeasurable.mk g hg x))
rw [← hxg, funext fun n => hxf n]
no goals
case h
α : Type u_1
ι : Type ?u.7016
E : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝¹ : MetricSpace E
f : ℕ → α → E
g : α → E
inst✝ : IsFiniteMeasure μ
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
hfg : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (g x))
hg : AEStronglyMeasurable g μ
hf_eq_ae : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
x : α
hxf : ∀ (n : ℕ), AEStronglyMeasurable.mk (f n) (_ : AEStronglyMeasurable (f n) μ) x = f n x
hxg : g x = AEStronglyMeasurable.mk g hg x
hxfg : Tendsto (fun n => f n x) atTop (𝓝 (g x))
⊢ Tendsto (fun n => f n x) atTop (𝓝 (g x))
exact hxfg