-- Lean 4 proof step from Mathlib.Topology.Compactification.OnePoint.Basic (goal)
Goal:
X : Type u_1
Y_1 : Type u_2
inst : TopologicalSpace X
s : Set (OnePoint X)
Y : Type u_3
inst_1 : DiscreteTopology X
inst_2 : TopologicalSpace Y
inst_3 : T2Space Y
inst_4 : Infinite X
f : ContinuousMap.{u_1, u_3} (OnePoint X) Y
x : OnePoint X
h :
  Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) ⋯
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := ⋯ } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) ⋯ :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        ∞ :
      Y)
    ((f : (a : OnePoint X) → Y) ∞ : Y)
⊢ Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) ⋯
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := ⋯ } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) ⋯ :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        x :
      Y)
    ((f : (a : OnePoint X) → Y) x : Y)
have h₁ : ∀ (x : X),
  Eq.{u_3 + 1} (α := Y)
    (((fun (f : { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }) ↦
              ({
                  toFun := fun (x : OnePoint X) ↦
                    match (motive := OnePoint X → Y) x with
                    | none =>
                      Classical.choose (p := fun (x : Y) ↦ Tendsto (fun (x : X) ↦ (↑f : X → Y) x) cofinite (𝓝 x)) sorry
                    | Option.some x => (↑f : X → Y) x,
                  continuous_toFun := sorry } :
                ContinuousMap.{u_1, u_3} (OnePoint X) Y))
            ((fun (f : ContinuousMap.{u_1, u_3} (OnePoint X) Y) ↦
                (Subtype.mk (p := fun (f : X → Y) ↦ ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L))
                    (fun (x : X) ↦ (f : (a : OnePoint X) → Y) (↑x : OnePoint X)) sorry :
                  { f : X → Y // ∃ (L : Y), Tendsto (fun (x : X) ↦ f x) cofinite (𝓝 L) }))
              f) :
          (a : OnePoint X) → Y)
        (↑x : OnePoint X) :
      Y)
    ((f : (a : OnePoint X) → Y) (↑x : OnePoint X) : Y)
Tactic: refine OnePoint.rec ?_ ?_ x