-- Mathlib/MeasureTheory/Constructions/BorelSpace/Metrizable.lean
theorem measurable_limit_of_tendsto_metrizable_ae {ι} [Countable ι] [Nonempty ι] {μ : Measure α}
    {f : ι → α → β} {L : Filter ι} [L.IsCountablyGenerated] (hf : ∀ n, AEMeasurable (f n) μ)
    (h_ae_tendsto : ∀ᵐ x ∂μ, ∃ l : β, Tendsto (fun n => f n x) L (𝓝 l)) :
    ∃ f_lim : α → β, Measurable f_lim ∧ ∀ᵐ x ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Proof state:
case inl
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
hf : ∀ (n : ι), AEMeasurable (f n) μ
inhabited_h : Inhabited ι
inst✝ : ⊥.IsCountablyGenerated
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) ⊥ (𝓝 l)
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) ⊥ (𝓝 (f_lim x))

Tactic:
exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Tactic:
have h_ae_eq : ∀ᵐ x ∂μ, ∀ n, aeSeq hf p n x = f n x := aeSeq.aeSeq_eq_fun_ae hf h_ae_tendsto

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
x : α
h : x ∈ aeSeqSet hf p
⊢ Tendsto (fun n => AEMeasurable.mk (f n) ⋯ x) L (𝓝 (Exists.choose ⋯))

Tactic:
refine (hp_mem x h).choose_spec.congr fun n => ?_

Result:
case pos
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
x : α
h : x ∈ aeSeqSet hf p
n : ι
⊢ (fun n => f n x) n = AEMeasurable.mk (f n) ⋯ x

Proof state:
case pos
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
x : α
h : x ∈ aeSeqSet hf p
n : ι
⊢ (fun n => f n x) n = AEMeasurable.mk (f n) ⋯ x

Tactic:
exact (aeSeq.mk_eq_fun_of_mem_aeSeqSet hf h n).symm

Result:
no goals

Proof state:
case neg
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
x : α
h : x ∉ aeSeqSet hf p
⊢ Tendsto (fun n => ⋯.some) L (𝓝 ⋯.some)

Tactic:
exact tendsto_const_nhds

Result:
no goals

Proof state:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))

Tactic:
set f_lim : α → β := fun x => dite (x ∈ aeSeqSet hf p) (fun h => (hp_mem x h).choose)
  fun _ => (⟨f default x⟩ : Nonempty β).some

Result:
case inr
α : Type u_1
β : Type u_2
inst✝⁷ : MeasurableSpace α
inst✝⁶ : TopologicalSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : MeasurableSpace β
inst✝³ : BorelSpace β
ι : Type u_3
inst✝² : Countable ι
inst✝¹ : Nonempty ι
μ : Measure α
f : ι → α → β
L : Filter ι
inst✝ : L.IsCountablyGenerated
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_ae_tendsto : ∀ᵐ (x : α) ∂μ, ∃ l, Tendsto (fun n => f n x) L (𝓝 l)
inhabited_h : Inhabited ι
hL : L.NeBot
p : α → (ι → β) → Prop := fun x f' => ∃ l, Tendsto (fun n => f' n) L (𝓝 l)
hp_mem : ∀ x ∈ aeSeqSet hf p, p x fun n => f n x
h_ae_eq : ∀ᵐ (x : α) ∂μ, ∀ (n : ι), aeSeq hf p n x = f n x
f_lim : α → β := fun x => if h : x ∈ aeSeqSet hf p then Exists.choose ⋯ else ⋯.some
⊢ ∃ f_lim, Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) L (𝓝 (f_lim x))