awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : Option.some b ≠ (partialFunToPointed.obj Y).point
some :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a)
      (h :
        Eq (α := PartialFun.of { x : Option Y // ¬x = none })
          (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
          (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some w) ⋯)),
      Option.some b = (f a).toOption
some₁ :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a)
      (h :
        (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb) : Option Y) =
          (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some w) ⋯) : Option Y)),
      Option.some b = (f a).toOption
some₂ :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a) (h : Option.some b = Option.some w), Option.some b = (f a).toOption
⊢ (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) ↔
    Option.some b = (f a).toOption
have some₃ : (∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none })
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) sorry)) →
  ∀ (w : Y) (hw : w ∈ f a) (h : Option.some b = Option.some w), Option.some w = (f a).toOption
Tactic: classical
            refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
            rw [Subtype.ext_iff] at h
            dsimp at h
            rw [h]
            rw [← Part.mem_toOption, mem_def] at hw
            exact hw.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : Option.some b ≠ (partialFunToPointed.obj Y).point
some :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a)
      (h :
        Eq (α := PartialFun.of { x : Option Y // ¬x = none })
          (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
          (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some w) ⋯)),
      Option.some b = (f a).toOption
some₁ :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a)
      (h :
        (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb) : Option Y) =
          (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some w) ⋯) : Option Y)),
      Option.some b = (f a).toOption
some₂ :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a) (h : Option.some b = Option.some w), Option.some b = (f a).toOption
some₃ :
  (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) →
    ∀ (w : Y) (hw : w ∈ f a) (h : Option.some b = Option.some w), Option.some w = (f a).toOption
⊢ (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯)) ↔
    Option.some b = (f a).toOption
have some₄ : (∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none })
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) sorry)) →
  ∀ (w : Y) (hw : (f a).toOption = Option.some w) (h : Option.some b = Option.some w), Option.some w = (f a).toOption
Tactic: classical
            refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
            rw [Subtype.ext_iff] at h
            dsimp at h
            rw [h]
            rw [← Part.mem_toOption, mem_def] at hw
            exact hw.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : Pointed
f : X ⟶ Y
a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
⊢ Eq (α := (Functor.obj (𝟭 Pointed) Y).X)
    (Pointed.Hom.toFun
      ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            Y))
      a)
    (Pointed.Hom.toFun
      (Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            X) ≫
        CategoryTheory.Functor.map (𝟭 Pointed) f)
      a)
have none : Eq (α := (Functor.obj (𝟭 Pointed) Y).X)
  (Pointed.Hom.toFun
    ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
      Iso.hom
        ((fun (X : Pointed.{u}) ↦
            (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry :
              (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
          Y))
    none)
  (Pointed.Hom.toFun (X := (pointedToPartialFun ⋙ partialFunToPointed).obj X)
    (Iso.hom
        ((fun (X : Pointed.{u}) ↦
            (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry :
              (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
          X) ≫
      CategoryTheory.Functor.map (𝟭 Pointed) f)
    none)
Tactic: obtain _ | ⟨a, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : Pointed
f : X ⟶ Y
a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
none :
  Eq (α := (Functor.obj (𝟭 Pointed) Y).X)
    (Pointed.Hom.toFun
      ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            Y))
      Option.none)
    (Pointed.Hom.toFun (X := (pointedToPartialFun ⋙ partialFunToPointed).obj X)
      (Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            X) ≫
        CategoryTheory.Functor.map (𝟭 Pointed) f)
      Option.none)
⊢ Eq (α := (Functor.obj (𝟭 Pointed) Y).X)
    (Pointed.Hom.toFun
      ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            Y))
      a)
    (Pointed.Hom.toFun
      (Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯ :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            X) ≫
        CategoryTheory.Functor.map (𝟭 Pointed) f)
      a)
have some : ∀ (a : X.X) (ha : a ≠ X.point),
  Eq (α := (Functor.obj (𝟭 Pointed) Y).X)
    (Pointed.Hom.toFun
      ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            Y))
      (some (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha)))
    (Pointed.Hom.toFun (X := (pointedToPartialFun ⋙ partialFunToPointed).obj X)
      (Iso.hom
          ((fun (X : Pointed.{u}) ↦
              (Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry :
                (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
            X) ≫
        CategoryTheory.Functor.map (𝟭 Pointed) f)
      (some (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha)))
Tactic: obtain _ | ⟨a, ha⟩ := a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X : PartialFun
⊢ Eq (α := partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)
    (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
        (partialFunToPointed.map
          (NatTrans.app
            (Iso.hom
              (NatIso.ofComponents
                (fun (X : PartialFun.{u}) ↦
                  PartialFun.Iso.mk
                    {
                      toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                        Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                          x ≠ (partialFunToPointed.obj X).point) (some a) ⋯,
                      invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                        Option.get (↑a : (partialFunToPointed.obj X).X) ⋯,
                      left_inv := ⋯, right_inv := ⋯ })
                ⋯))
            X))
        (NatTrans.app
          (Iso.hom (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯))
          (partialFunToPointed.obj X)) :
      partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)
    (𝟙 (partialFunToPointed.obj X) : partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)
have h : (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
          (X := partialFunToPointed.obj X) (Y := partialFunToPointed.obj X)
          (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
              (partialFunToPointed.map
                (NatTrans.app
                  (Iso.hom
                    (NatIso.ofComponents
                      (fun (X : PartialFun.{u}) ↦
                        PartialFun.Iso.mk
                          {
                            toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                              Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                                x ≠ (partialFunToPointed.obj X).point) (some a) sorry,
                            invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                              Option.get (↑a : (partialFunToPointed.obj X).X) sorry,
                            left_inv := sorry, right_inv := sorry })
                      sorry))
                  X))
              (NatTrans.app
                (Iso.hom
                  (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) sorry) sorry))
                (partialFunToPointed.obj X)) :
            partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)) :
      (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
    none =
  (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
          (𝟙 (partialFunToPointed.obj X))) :
      (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
    none
Tactic: ext (_ | x)
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X : PartialFun
x : X
⊢ (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
            (X := partialFunToPointed.obj X) (Y := partialFunToPointed.obj X)
            (CategoryStruct.comp (Y := partialFunToPointed.obj (pointedToPartialFun.obj (partialFunToPointed.obj X)))
                (partialFunToPointed.map
                  (NatTrans.app
                    (Iso.hom
                      (NatIso.ofComponents
                        (fun (X : PartialFun.{u}) ↦
                          PartialFun.Iso.mk
                            {
                              toFun := fun (a : Functor.obj (𝟭 PartialFun) X) ↦
                                Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦
                                  x ≠ (partialFunToPointed.obj X).point) (some a) ⋯,
                              invFun := fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦
                                Option.get (↑a : (partialFunToPointed.obj X).X) ⋯,
                              left_inv := ⋯, right_inv := ⋯ })
                        ⋯))
                    X))
                (NatTrans.app
                  (Iso.hom
                    (NatIso.ofComponents (fun (X : Pointed.{u}) ↦ Pointed.Iso.mk (Equiv.optionSubtypeNe X.point) ⋯) ⋯))
                  (partialFunToPointed.obj X)) :
              partialFunToPointed.obj X ⟶ partialFunToPointed.obj X)) :
        (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
      (some x) =
    (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
            (𝟙 (partialFunToPointed.obj X))) :
        (partialFunToPointed.obj X).X → (partialFunToPointed.obj X).X)
      (some x)
have h : (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
          (X := { X := Option X, point := none }) (Y := { X := Option X, point := none })
          (CategoryStruct.comp (Y := { X := Option (PartialFun.of { x : Option X // ¬x = none }), point := none })
            {
              toFun :=
                Option.elim' none fun (a : X) ↦ some (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) sorry),
              map_point := sorry }
            (Iso.hom (Pointed.Iso.mk (Equiv.optionSubtypeNe none) sorry)))) :
      Option X → Option X)
    (some x) =
  (↑(ConcreteCategory.hom (FC := fun (X Y : Pointed.{u}) ↦ { f : X.X → Y.X // f X.point = Y.point }) (CC := Pointed.X)
          (𝟙 { X := Option X, point := none : Pointed.{u} })) :
      Option X → Option X)
    (some x)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : Type u_1
f : X ⟶ Y
a_1 : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X
a : typeToPartialFun.obj X
⊢ Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            Y))
      (some a) =
    Pointed.Hom.toFun (X := (typeToPartialFun ⋙ partialFunToPointed).obj X)
      (Iso.hom
          ((fun (x : Type u_1) ↦
              ({
                  hom :=
                    { toFun := id, map_point := ⋯ :
                      ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                  inv :=
                    { toFun := id, map_point := ⋯ :
                      (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                  hom_inv_id := ⋯, inv_hom_id := ⋯ } :
                (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
            X) ≫
        typeToPointed.map f)
      (some a)
have h : Eq (α := (typeToPointed.obj Y).X)
  (Pointed.Hom.toFun
    ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
      Iso.hom
        ((fun (x : Type u_1) ↦
            ({
                hom :=
                  { toFun := id, map_point := sorry :
                    ((typeToPartialFun ⋙ partialFunToPointed).obj x).Hom (typeToPointed.obj x) },
                inv :=
                  { toFun := id, map_point := sorry :
                    (typeToPointed.obj x).Hom ((typeToPartialFun ⋙ partialFunToPointed).obj x) },
                hom_inv_id := sorry, inv_hom_id := sorry } :
              (typeToPartialFun ⋙ partialFunToPointed).obj x ≅ typeToPointed.obj x))
          Y))
    (some a))
  (Part.toOption
    (Part.some
      ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) Y) a)))
Tactic: convert! Part.some_toOption _
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
⊢ (g.toFun ∘ f.toFun) X.point = Z.point
have rw : g.toFun (f.toFun X.point) = Z.point
Tactic: rw [Function.comp_apply, f.map_point, g.map_point]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.point) = Z.point
⊢ (g.toFun ∘ f.toFun) X.point = Z.point
have rw₁ : g.toFun Y.point = Z.point
Tactic: rw [Function.comp_apply, f.map_point, g.map_point]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X Y Z : Pointed
f : X.Hom Y
g : Y.Hom Z
rw : g.toFun (f.toFun X.point) = Z.point
rw₁ : g.toFun Y.point = Z.point
⊢ (g.toFun ∘ f.toFun) X.point = Z.point
have rw₂ : Z.point = Z.point
Tactic: rw [Function.comp_apply, f.map_point, g.map_point]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X Y Z : Type u
x : X ⟶ Y
x_1 : Y ⟶ Z
⊢ Eq.{u + 1} (α := { X := Option X, point := none }.X → { X := Option Z, point := none }.X)
    (Pointed.Hom.toFun
      {
        toFun :=
          Option.map
            (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1)) :
              (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Z),
        map_point := ⋯ })
    (Pointed.Hom.toFun
      (CategoryStruct.comp (Y := { X := Option Y, point := none })
        {
          toFun :=
            Option.map
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x) :
                (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) Y),
          map_point := ⋯ }
        {
          toFun :=
            Option.map
              (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1) :
                (a : (fun (X : Type u) ↦ X) Y) → (fun (X : Type u) ↦ X) Z),
          map_point := ⋯ }))
have simp : Eq (α := X → Z) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (x ≫ x_1)) : (a : X) → Z)
  (Function.comp (β := Y) (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x_1) : (a : Y) → Z)
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) x) : (a : X) → Y))
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ (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))
      ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f) =
    f
have toFun : Pointed.Hom.toFun
    ((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))
      ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f)) =
  f.toFun
Tactic: apply Pointed.Hom.ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.Pointed (goal)
Goal:
X : Type u_1
Y : Pointed
f : typeToPointed.obj X ⟶ Y
⊢ Pointed.Hom.toFun
      ((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))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f)) =
    f.toFun
have toFun : ∀ (x : (typeToPointed.obj X).X),
  Pointed.Hom.toFun
      ((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))
        ((fun (f : typeToPointed.obj X ⟶ Y) ↦ ↾(f.toFun ∘ some)) f))
      x =
    f.toFun x
Tactic: funext x