-- Module: Mathlib.CategoryTheory.Category.Pointed
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)
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 := ⋯ : (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))
        (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 := ⋯ : (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)
        (some val))
⊢ 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)

Tactic:
cases x