-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X' X : Type u_1
Y : Pointed
f : X' ⟶ X
g :
  X ⟶
    Functor.obj
      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)) Y
x : (typeToPointed.obj X').X
toFun :
  Eq (α := Y.X)
    (Pointed.Hom.toFun (X := typeToPointed.obj X')
      (({ toFun := fun (f : typeToPointed.obj X' ⟶ Y) ↦ ↾(f.toFun ∘ some),
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                          (CC := Pointed.X))
                        Y) ↦
                {
                  toFun := fun (o : (typeToPointed.obj X').X) ↦
                    Option.elim o Y.point
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u_1) ↦ X) X') → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                  map_point := ⋯ : (typeToPointed.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (typeToPointed.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) }.symm :
          (a : X' ⟶ (forget Pointed).obj Y) → typeToPointed.obj X' ⟶ Y)
        (f ≫ g))
      none)
    (Pointed.Hom.toFun
      (typeToPointed.map f ≫
        ({ toFun := fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some),
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                            (CC := Pointed.X))
                          Y) ↦
                  {
                    toFun := fun (o : (typeToPointed.obj X).X) ↦
                      Option.elim o Y.point
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                    map_point := ⋯ : (typeToPointed.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (typeToPointed.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                        (CC := Pointed.X))
                      Y) }.symm :
            (a : X ⟶ (forget Pointed).obj Y) → typeToPointed.obj X ⟶ Y)
          g)
      none)
⊢ Eq (α := Y.X)
    (Pointed.Hom.toFun
      (({ toFun := fun (f : typeToPointed.obj X' ⟶ Y) ↦ ↾(f.toFun ∘ some),
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                          (CC := Pointed.X))
                        Y) ↦
                {
                  toFun := fun (o : (typeToPointed.obj X').X) ↦
                    Option.elim o Y.point
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u_1) ↦ X) X') → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                  map_point := ⋯ : (typeToPointed.obj X').Hom Y },
              left_inv := ⋯, right_inv := ⋯ :
              (typeToPointed.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) }.symm :
          (a : X' ⟶ (forget Pointed).obj Y) → typeToPointed.obj X' ⟶ Y)
        (f ≫ g))
      x)
    (Pointed.Hom.toFun
      (typeToPointed.map f ≫
        ({ toFun := fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some),
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                            (CC := Pointed.X))
                          Y) ↦
                  {
                    toFun := fun (o : (typeToPointed.obj X).X) ↦
                      Option.elim o Y.point
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                    map_point := ⋯ : (typeToPointed.obj X).Hom Y },
                left_inv := ⋯, right_inv := ⋯ :
                (typeToPointed.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                        (CC := Pointed.X))
                      Y) }.symm :
            (a : X ⟶ (forget Pointed).obj Y) → typeToPointed.obj X ⟶ Y)
          g)
      x)
have toFun₁ : ∀ (val : X'),
  Eq (α := Y.X)
    (Pointed.Hom.toFun (X := typeToPointed.obj X')
      (({ toFun := fun (f : typeToPointed.obj X' ⟶ Y) ↦ ↾(f.toFun ∘ some),
              invFun :=
                fun
                  (f :
                    X' ⟶
                      Functor.obj
                        (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                          (CC := Pointed.X))
                        Y) ↦
                {
                  toFun := fun (o : (typeToPointed.obj X').X) ↦
                    Option.elim o Y.point
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                        (a : (fun (X : Type u_1) ↦ X) X') → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                  map_point := sorry : (typeToPointed.obj X').Hom Y },
              left_inv := sorry, right_inv := sorry :
              (typeToPointed.obj X' ⟶ Y) ≃
                (X' ⟶
                  Functor.obj
                    (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC :=
                      Pointed.X))
                    Y) }.symm :
          (a : X' ⟶ (forget Pointed).obj Y) → typeToPointed.obj X' ⟶ Y)
        (f ≫ g))
      (some val))
    (Pointed.Hom.toFun
      (typeToPointed.map f ≫
        ({ toFun := fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some),
                invFun :=
                  fun
                    (f :
                      X ⟶
                        Functor.obj
                          (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                            (CC := Pointed.X))
                          Y) ↦
                  {
                    toFun := fun (o : (typeToPointed.obj X).X) ↦
                      Option.elim o Y.point
                        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f) :
                          (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) ((forget Pointed).obj Y)),
                    map_point := sorry : (typeToPointed.obj X).Hom Y },
                left_inv := sorry, right_inv := sorry :
                (typeToPointed.obj X ⟶ Y) ≃
                  (X ⟶
                    Functor.obj
                      (forget Pointed (FC := fun (X Y : Pointed.{u_1}) ↦ { f : X.X → Y.X // f X.point = Y.point })
                        (CC := Pointed.X))
                      Y) }.symm :
            (a : X ⟶ (forget Pointed).obj Y) → typeToPointed.obj X ⟶ Y)
          g)
      (some val))
Tactic: cases x
Cleared hypotheses: x