-- Module: Mathlib.Topology.Compactification.OnePoint.Basic
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)
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)) ⋯
                      | 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 : OnePoint X) :
        Y)
      ((f : (a : OnePoint X) → Y) (↑x : OnePoint X) : 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)

Tactic:
refine OnePoint.rec ?_ ?_ x