-- Mathlib/Probability/Martingale/Convergence.lean
theorem tendsto_ae_condExp (g : Ω → ℝ) :
    ∀ᵐ x ∂μ, Tendsto (fun n => (μ[g|ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ℱ n]) x))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Tactic:
filter_upwards [heq, ht] with x hxeq hxt

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
x : Ω
hxeq : ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) x = (μ[g|↑ℱ i]) x
hxt : Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
⊢ Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Tactic:
have heq : ∀ n, ∀ᵐ x ∂μ, (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x = (μ[g|ℱ n]) x := fun n =>
  condExp_condExp_of_le (le_iSup _ n) (iSup_le fun n => ℱ.le n)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
x : Ω
hxeq : ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) x = (μ[g|↑ℱ i]) x
hxt : Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
⊢ Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Tactic:
exact hxt.congr hxeq

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ (n : ℕ), ∀ᵐ (x : Ω) ∂μ, (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x = (μ[g|↑ℱ n]) x
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Tactic:
rw [← ae_all_iff] at heq

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
heq : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ i]) a = (μ[g|↑ℱ i]) a
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))

Tactic:
have ht : ∀ᵐ x ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ℱ n]|ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ℱ n]) x)) :=
  integrable_condExp.tendsto_ae_condExp stronglyMeasurable_condExp

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
ht : ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[μ[g|⨆ n, ↑ℱ n]|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))
⊢ ∀ᵐ (x : Ω) ∂μ, Tendsto (fun n => (μ[g|↑ℱ n]) x) atTop (𝓝 ((μ[g|⨆ n, ↑ℱ n]) x))