awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
hb : Ne.{u + 1} (α := (partialFunToPointed.obj Y).X) none (partialFunToPointed.obj Y).point
⊢ (∃ a_1 ∈ f a,
      Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
        (Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯))
        (Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) none hb)) ↔
    (↑(Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) none hb) :
        Option Y) =
      Option.elim' none (fun (a : X) ↦ (f a).toOption)
        (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯) : Option X)

Tactic:
exact (hb rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
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) ⋯)) ↔
    Option.some b = (f a).toOption
⊢ (∃ a_1 ∈ f a,
      Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
        (Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (Option.some a_1) ⋯))
        (Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point)
          (Option.some b) hb)) ↔
    (↑(Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) (Option.some b)
            hb) :
        Option Y) =
      Option.elim' none (fun (a : X) ↦ (f a).toOption)
        (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (Option.some a) ⋯) : Option X)

Tactic:
simp only [partialFunToPointed_obj, ne_eq, Part.mem_some_iff, elim'_some]

Premises used: Part.mem_some_iff, ne_eq, partialFunToPointed_obj, Option.elim'_some
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
⊢ (∃ a_1 ∈ f a,
      Eq (α := PartialFun.of { x : Option Y // ¬x = none })
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
        (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯)) ↔
    some b = (f a).toOption

Tactic:
⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩

Premises used: Option.some, Part.mem_toOption, And.intro, Iff.intro, Exists.intro, Iff.mp, Eq.symm, Eq, _private.0.partialFunEquivPointed.match_1, Part.toOption, rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
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
⊢ (∃ 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

Tactic:
refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none }) (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (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) (some b) hb)
    (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some w) ⋯)
⊢ (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb) : Option Y) =
    (↑(Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some w) ⋯) : Option Y)

Tactic:
rw [Subtype.ext_iff] at h

Premises used: Subtype.ext_iff
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : Option.some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ 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
some : Option.some w = (f a).toOption
⊢ Option.some b = (f a).toOption

Tactic:
rw [h]
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none }) (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯)
w : Y
hw : w ∈ f a
h : some b = some w
⊢ (f a).toOption = some w

Tactic:
rw [← Part.mem_toOption, mem_def] at hw

Premises used: Part.mem_toOption, Option.mem_def
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none }) (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯)
w : Y
hw : w ∈ f a
h : some b = some w
hw₁ : (f a).toOption = some w
⊢ some b = some w

Tactic:
rw [← Part.mem_toOption, mem_def] at hw

Premises used: Part.mem_toOption, Option.mem_def
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none }) (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯)
w : Y
hw : (f a).toOption = some w
h : some b = some w
⊢ some w = (f a).toOption

Tactic:
hw.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : Y
hb : some b ≠ (partialFunToPointed.obj Y).point
h_1 :
  ∃ a_1 ∈ f a,
    Eq (α := PartialFun.of { x : Option Y // ¬x = none }) (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some b) hb)
      (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some a_1) ⋯)
w : Y
hw : (f a).toOption = some w
h : some b = some w
⊢ some w = (f a).toOption

Tactic:
exact hw.symm

Premises used: Eq.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
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
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 : (f a).toOption = Option.some w) (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

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

Premises used: Part.mem_toOption, Subtype.ext_iff, Option.mem_def
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : Pointed
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X ≃ (Functor.obj (𝟭 Pointed) X).X

Tactic:
exact Equiv.optionSubtypeNe X.point

Premises used: Pointed.point, Equiv.optionSubtypeNe
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : Pointed
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X ≃ (Functor.obj (𝟭 Pointed) X).X

Tactic:
classical exact Equiv.optionSubtypeNe X.point
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : Pointed
⊢ Eq (α := (Functor.obj (𝟭 Pointed) X).X)
    ((Equiv.optionSubtypeNe X.point :
          (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X) → ((𝟭 Pointed).obj X).X)
        ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point :
      (Functor.obj (𝟭 Pointed) X).X)
    ((Functor.obj (𝟭 Pointed) X).point : (Functor.obj (𝟭 Pointed) X).X)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
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)
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) ⋯ :
                  (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
              Y))
        (Option.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) ⋯ :
                  (pointedToPartialFun ⋙ partialFunToPointed).obj X ≅ Functor.obj (𝟭 Pointed) X))
              X) ≫
          CategoryTheory.Functor.map (𝟭 Pointed) f)
        (Option.some (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha)))
⊢ 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)

Tactic:
obtain _ | ⟨a, ha⟩ := a
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Pointed
f : X ⟶ Y
⊢ 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))
      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)
      none)

Tactic:
f.map_point.symm

Premises used: Option.casesOn', Pointed.Hom.map_point, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Pointed
f : X ⟶ Y
⊢ 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))
      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)
      none)

Tactic:
exact f.map_point.symm

Premises used: Pointed.Hom.map_point, Eq.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Pointed
f : X ⟶ Y
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) ⋯ :
                (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) ⋯ :
                (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:
simp_all [Equiv.optionSubtypeNe, Equiv.optionSubtype,
          Option.casesOn'_eq_elim, Part.elim_toOption]

Premises used: Part.elim_toOption, Equiv.optionSubtypeNe, Equiv.optionSubtype, Option.casesOn'_eq_elim
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
⊢ (↑(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)
      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:
rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
x : X
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) ⋯),
                map_point := ⋯ }
              (Iso.hom (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯)))) :
        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)
⊢ (↑(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)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.PartialFun
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 := { 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) ⋯),
                map_point := ⋯ }
              (Iso.hom (Pointed.Iso.mk (Equiv.optionSubtypeNe none) ⋯)))) :
        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:
rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
f : X ⟶ Y
a_1 : ((typeToPartialFun ⋙ partialFunToPointed).obj X).X
a : typeToPartialFun.obj X
⊢ Eq (α := Option Y)
    (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)) :
      Option Y)
    (some
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u_1) ↦ X) X) → (fun (X : Type u_1) ↦ X) Y)
          a) :
      Option Y)

Tactic:
Part.some_toOption _

Premises used: Part.some_toOption