-- Lean 4 proof step from Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable (goal)
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))
inl :
  ∀ (inhabited_h : Inhabited ι) [IsCountablyGenerated.{u_3} (α := ι) ⊥]
    (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))
inr inr₁ inr₂ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    ∃ (f_lim : α → β), Measurable f_lim ∧ ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))
inr₃ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    let f_lim : α → β := fun (x : α) ↦
      if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
        h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
      else ⋯.some;
    ∀ (h_ae_tendsto_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))
inr₄ :
  ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
    let f_lim : α → β := fun (x : α) ↦
      if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
        h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
      else ⋯.some;
    ∀ (h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x)))
      (hf_lim : AEMeasurable f_lim μ),
      ∃ (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))
have inr₅ : ∀ (inhabited_h : Inhabited ι) (hL : L.NeBot),
  let f_lim : α → β := fun (x : α) ↦
    if h : ∃ (l : β), Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l) then
      h.choose (p := fun (l : β) ↦ Tendsto (fun (n : ι) ↦ f n x) L (𝓝 l))
    else sorry.some;
  ∀ (h_ae_tendsto_f_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (f_lim x))) (hf_lim : AEMeasurable f_lim μ),
    ∀ᵐ (x : α) ∂μ, Tendsto (fun (n : ι) ↦ f n x) L (𝓝 (AEMeasurable.mk f_lim hf_lim x))
Tactic: classical
  inhabit ι
  rcases eq_or_neBot L with (rfl | hL)
  · exact ⟨(hf default).mk _, (hf default).measurable_mk, Eventually.of_forall fun x => tendsto_bot⟩
  set f_lim : α → β := fun x ↦
    if h : ∃ l : β, Tendsto (fun n ↦ f n x) L (𝓝 l) then h.choose
      else (⟨f default x⟩ : Nonempty β).some
  have h_ae_tendsto_f_lim : ∀ᵐ x ∂μ, Tendsto (fun n ↦ f n x) L (𝓝 (f_lim x)) := by
    filter_upwards [h_ae_tendsto] with x hx
    simpa [f_lim, hx] using hx.choose_spec
  have hf_lim : AEMeasurable f_lim μ :=
    aemeasurable_of_tendsto_metrizable_ae L hf h_ae_tendsto_f_lim
  refine ⟨hf_lim.mk f_lim, hf_lim.measurable_mk, ?_⟩
  filter_upwards [h_ae_tendsto_f_lim, hf_lim.ae_eq_mk] with x hx h_eq
  simpa [h_eq] using hx