-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measurable_of_tendsto' {ι : Type*} {f : ι → α → ℝ≥0∞} {g : α → ℝ≥0∞} (u : Filter ι)
    [NeBot u] [IsCountablyGenerated u] (hf : ∀ i, Measurable (f i)) (lim : Tendsto f u (𝓝 g)) :
    Measurable g

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
y : α
⊢ liminf (fun n => f (x n) y) atTop = g y

Tactic:
exact ((lim y).comp hx).liminf_eq

Result:
no goals

Proof state:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y => liminf (fun n => f (x n) y) atTop) = g
⊢ Measurable fun y => liminf (fun n => f (x n) y) atTop

Tactic:
exact .liminf fun n => hf (x n)

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ (fun y => liminf (fun n => f (x n) y) atTop) = g

Tactic:
ext1 y

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
y : α
⊢ liminf (fun n => f (x n) y) atTop = g y

Proof state:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g

Tactic:
rw [tendsto_pi_nhds] at lim

Result:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g

Proof state:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y => liminf (fun n => f (x n) y) atTop) = g
⊢ Measurable g

Tactic:
rw [← this]

Result:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y => liminf (fun n => f (x n) y) atTop) = g
⊢ Measurable fun y => liminf (fun n => f (x n) y) atTop

Proof state:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g

Tactic:
have : (fun y => liminf (fun n => (f (x n) y : ℝ≥0∞)) atTop) = g := by
  ext1 y
  exact ((lim y).comp hx).liminf_eq

Result:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : ∀ (x : α), Tendsto (fun i => f i x) u (𝓝 (g x))
x : ℕ → ι
hx : Tendsto x atTop u
this : (fun y => liminf (fun n => f (x n) y) atTop) = g
⊢ Measurable g

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
⊢ Measurable g

Tactic:
rcases u.exists_seq_tendsto with ⟨x, hx⟩

Result:
case intro
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
f : ι → α → ℝ≥0∞
g : α → ℝ≥0∞
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
hf : ∀ (i : ι), Measurable (f i)
lim : Tendsto f u (𝓝 g)
x : ℕ → ι
hx : Tendsto x atTop u
⊢ Measurable g