awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
α β : PartialFun
e : α ≃ β
simp : PFun.id α = 𝟙 α
⊢ (↑(Function.comp (β := β) (⇑e.symm : (a : β) → α) (⇑e : (a : α) → β)) : α →. α) = 𝟙 α

Tactic:
simp only [Equiv.symm_comp_self, PFun.coe_id]

Premises used: Equiv.symm_comp_self, PFun.coe_id
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
α β : PartialFun
e : α ≃ β
⊢ PFun.id α = 𝟙 α

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
α β : PartialFun
e : α ≃ β
simp : PFun.id β = 𝟙 β
⊢ (↑(Function.comp (β := α) (⇑e : (a : α) → β) (⇑e.symm : (a : β) → α)) : β →. β) = 𝟙 β

Tactic:
simp only [Equiv.self_comp_symm, PFun.coe_id]

Premises used: Equiv.self_comp_symm, PFun.coe_id
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
α β : PartialFun
e : α ≃ β
⊢ PFun.id β = 𝟙 β

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
a₁ a₂ : X ⟶ Y
h : typeToPartialFun.map a₁ = typeToPartialFun.map a₂
h₁ :
  ∀ (x : X),
    (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x
⊢ a₁ = a₂

Tactic:
ext x
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
a₁ a₂ : X ⟶ Y
h : typeToPartialFun.map a₁ = typeToPartialFun.map a₂
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x

Tactic:
congrFun (PFun.lift_injective h) x

Premises used: PFun.lift_injective, congrFun
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : Type u_1
a₁ a₂ : X ⟶ Y
h : typeToPartialFun.map a₁ = typeToPartialFun.map a₂
x : X
⊢ (ConcreteCategory.hom (FC := TypeCat.Fun) a₁).toFun x = (ConcreteCategory.hom (FC := TypeCat.Fun) a₂).toFun x

Tactic:
exact congrFun (PFun.lift_injective h) x

Premises used: PFun.lift_injective, congrFun
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
⊢ Eq (α := PartialFun.of { x : X.X // x ≠ X.point } ⟶ PartialFun.of { x : Z.X // x ≠ Z.point })
    (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
    (CategoryStruct.comp (Y := PartialFun.of { x : Y.X // x ≠ Y.point })
      (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
      (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)))

Tactic:
PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ =>
      (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm

Premises used: Part.mem_bind_iff, Function.comp, Membership.mem, _private.0.pointedToPartialFun.match_1, Ne, Subtype.mk, Pointed.point, Iff, PFun.mem_toSubtype_iff, CategoryTheory.CategoryStruct.comp, Iff.trans, PFun.toSubtype, PFun.ext, Subtype.val, Iff.symm, Pointed.Hom.toFun
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
refine :
  ∀ (x : PartialFun.of { x : X.X // x ≠ X.point }) (x : PartialFun.of { x : Z.X // x ≠ Z.point }) (a : X.X)
    (ha : a ≠ X.point) (c : Z.X) (hc : c ≠ Z.point),
    (↑(Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc) : Z.X) =
        (f ≫ g).toFun (↑(Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha) : X.X) ↔
      ∃ (a_1 : PartialFun.of { x : Y.X // x ≠ Y.point }),
        Membership.mem (γ := Part (PartialFun.of { x : Y.X // x ≠ Y.point }))
            (Function.comp (α := PartialFun.of { x : X.X // x ≠ X.point })
              (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun) (Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
              (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha))
            a_1 ∧
          Membership.mem (γ := Part (PartialFun.of { x : Z.X // x ≠ Z.point }))
            ((PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point))
              a_1)
            (Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc)
⊢ Eq (α := PartialFun.of { x : X.X // x ≠ X.point } ⟶ PartialFun.of { x : Z.X // x ≠ Z.point })
    (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) (f ≫ g).toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
    (CategoryStruct.comp (Y := PartialFun.of { x : Y.X // x ≠ Y.point })
      (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun ∘ Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
      (PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)))

Tactic:
refine PFun.ext fun ⟨a, ha⟩ ⟨c, hc⟩ =>
      (PFun.mem_toSubtype_iff.trans ?_).trans Part.mem_bind_iff.symm

Premises used: PFun.ext
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ (↑(Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc) : Z.X) =
      (f ≫ g).toFun (↑(Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha) : X.X) →
    ∃ (a_2 : PartialFun.of { x : Y.X // x ≠ Y.point }),
      Membership.mem (γ := Part (PartialFun.of { x : Y.X // x ≠ Y.point }))
          (Function.comp (α := PartialFun.of { x : X.X // x ≠ X.point })
            (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun) (Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
            (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha))
          a_2 ∧
        Membership.mem (γ := Part (PartialFun.of { x : Z.X // x ≠ Z.point }))
          ((PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)) a_2)
          (Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc)

Tactic:
aesop
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
simp :
  ∀ (x : ¬f.toFun a = Y.point) (x_2 : ¬g.toFun (f.toFun a) = Z.point)
    (h :
      Eq (α := PartialFun.of { x : Z.X // ¬x = Z.point })
        (Subtype.mk (p := fun (x : Z.X) ↦ ¬x = Z.point) (g.toFun (f.toFun a)) ⋯)
        (Subtype.mk (p := fun (x : Z.X) ↦ ¬x = Z.point) c hc)),
    c = g.toFun (f.toFun a)
⊢ (∃ (a_1 : PartialFun.of { x : Y.X // x ≠ Y.point }),
      Membership.mem (γ := Part (PartialFun.of { x : Y.X // x ≠ Y.point }))
          (Function.comp (α := PartialFun.of { x : X.X // x ≠ X.point })
            (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun) (Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
            (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha))
          a_1 ∧
        Membership.mem (γ := Part (PartialFun.of { x : Z.X // x ≠ Z.point }))
          ((PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)) a_1)
          (Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc)) →
    (↑(Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc) : Z.X) =
      (f ≫ g).toFun (↑(Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha) : X.X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
this : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ ∀ (x : ¬f.toFun a = Y.point) (x_2 : ¬g.toFun (f.toFun a) = Z.point)
    (h :
      Eq (α := PartialFun.of { x : Z.X // ¬x = Z.point })
        (Subtype.mk (p := fun (x : Z.X) ↦ ¬x = Z.point) (g.toFun (f.toFun a)) ⋯)
        (Subtype.mk (p := fun (x : Z.X) ↦ ¬x = Z.point) c hc)),
    c = g.toFun (f.toFun a)

Tactic:
grind
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
c : Z.X
hc : c ≠ Z.point
suffices : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
⊢ (↑(Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc) : Z.X) =
      (f ≫ g).toFun (↑(Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha) : X.X) ↔
    ∃ (a_1 : PartialFun.of { x : Y.X // x ≠ Y.point }),
      Membership.mem (γ := Part (PartialFun.of { x : Y.X // x ≠ Y.point }))
          (Function.comp (α := PartialFun.of { x : X.X // x ≠ X.point })
            (PFun.toSubtype (fun (x : Y.X) ↦ x ≠ Y.point) f.toFun) (Subtype.val (p := fun (x : X.X) ↦ x ≠ X.point))
            (Subtype.mk (p := fun (x : X.X) ↦ x ≠ X.point) a ha))
          a_1 ∧
        Membership.mem (γ := Part (PartialFun.of { x : Z.X // x ≠ Z.point }))
          ((PFun.toSubtype (fun (x : Z.X) ↦ x ≠ Z.point) g.toFun ∘ Subtype.val (p := fun (x : Y.X) ↦ x ≠ Y.point)) a_1)
          (Subtype.mk (p := fun (x : Z.X) ↦ x ≠ Z.point) c hc)

Tactic:
suffices c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a) from
      ⟨by aesop, by simp; grind⟩
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
hc : g.toFun (f.toFun a) ≠ Z.point
⊢ ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)

Tactic:
⟨fun h => hc.symm <| g.map_point ▸ congr_arg g.toFun h, hc.symm⟩

Premises used: Eq.rec, Pointed.Hom.map_point, Ne.symm, congr_arg, And.intro, Pointed.Hom.toFun
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : Pointed
f : X ⟶ Y
g : Y ⟶ Z
x : PartialFun.of { x : X.X // x ≠ X.point }
x_1 : PartialFun.of { x : Z.X // x ≠ Z.point }
a : X.X
ha : a ≠ X.point
hc : g.toFun (f.toFun a) ≠ Z.point
⊢ ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)

Tactic:
refine ⟨fun h => hc.symm <| g.map_point ▸ congr_arg g.toFun h, hc.symm⟩
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
o : { X := Option X, point := none }.X
a : X
dsimp : (Part.some a).toOption = some a
⊢ Pointed.Hom.toFun (X := { X := Option X, point := none })
      { toFun := Option.elim' none fun (a : X) ↦ Part.toOption (𝟙 X a), map_point := ⋯ } (some a) =
    Pointed.Hom.toFun (𝟙 { X := Option X, point := none : Pointed.{?u.17570} }) (some a)

Tactic:
dsimp [CategoryStruct.id]

Premises used: CategoryTheory.CategoryStruct.id
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ (Part.some a).toOption = some a

Tactic:
Part.some_toOption a

Premises used: Part.some_toOption
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ (Part.some a).toOption = some a

Tactic:
convert! Part.some_toOption a

Premises used: Part.some_toOption
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : PartialFun
f : X ⟶ Y
g : Y ⟶ Z
o : { X := Option X, point := none }.X
a : X
dsimp : ((f a).bind g).toOption = Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption
⊢ Eq (α := { X := Option Z, point := none }.X)
    (Pointed.Hom.toFun (X := { X := Option X, point := none })
      { toFun := Option.elim' none fun (a : X) ↦ ((f ≫ g) a).toOption, map_point := ⋯ } (some a))
    (Pointed.Hom.toFun (X := { X := Option X, point := none })
      (CategoryStruct.comp (Y := { X := Option Y, point := none })
        { toFun := Option.elim' none fun (a : X) ↦ (f a).toOption, map_point := ⋯ }
        { toFun := Option.elim' none fun (a : Y) ↦ (g a).toOption, map_point := ⋯ })
      (some a))

Tactic:
dsimp [CategoryStruct.comp]

Premises used: CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y Z : PartialFun
f : X ⟶ Y
g : Y ⟶ Z
o : { X := Option X, point := none }.X
a : X
rw :
  Eq (α := Option Z) ((f a).toOption.elim none fun (a : Y) ↦ (g a).toOption)
    (Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption)
rw₁ rw₂ :
  Eq (α := Option Z) ((f a).toOption.elim none fun (a : Y) ↦ (g a).toOption)
    ((f a).toOption.elim none fun (a : Y) ↦ (g a).toOption)
⊢ ((f a).bind g).toOption = Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption

Tactic:
rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]

Premises used: Option.elim'_eq_elim, Part.bind_toOption
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
⊢ PartialFun ⥤ Pointed

Tactic:
exact
    { obj := fun X => ⟨(Option X), none⟩
      map := fun f => ⟨Option.elim' none fun a => (f a).toOption, rfl⟩
      map_id := fun X => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => (by
        dsimp [CategoryStruct.id]
        convert! Part.some_toOption a)
      map_comp := fun f g => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => by
        dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim] }
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
⊢ PartialFun ⥤ Pointed

Tactic:
classical
  exact
    { obj := fun X => ⟨(Option X), none⟩
      map := fun f => ⟨Option.elim' none fun a => (f a).toOption, rfl⟩
      map_id := fun X => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => (by
        dsimp [CategoryStruct.id]
        convert! Part.some_toOption a)
      map_comp := fun f g => Pointed.Hom.ext <| funext fun o => Option.recOn o rfl fun a => by
        dsimp [CategoryStruct.comp]
        rw [Part.bind_toOption g (f a), Option.elim'_eq_elim] }
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X : PartialFun
a : (partialFunToPointed ⋙ pointedToPartialFun).obj X
⊢ (fun (a : Functor.obj (𝟭 PartialFun) X) ↦
        (Subtype.mk (p := fun (x : (partialFunToPointed.obj X).X) ↦ x ≠ (partialFunToPointed.obj X).point) (some a) ⋯ :
          { x : (partialFunToPointed.obj X).X // x ≠ (partialFunToPointed.obj X).point }))
      ((fun (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X) ↦ Option.get (↑a : (partialFunToPointed.obj X).X) ⋯)
        a) =
    a

Tactic:
simp only [some_get, Subtype.coe_eta]

Premises used: Option.some_get, Subtype.coe_eta
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
dsimp :
  Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      ((f a).bind fun (x : Y) ↦ Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some x) ⋯)) b ↔
    Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      (Part.bind (α := PartialFun.of { x : Option X // ¬x = none })
        (Part.some (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯))
        (PFun.toSubtype (fun (x : Option Y) ↦ ¬x = none) (Option.elim' none fun (a : X) ↦ (f a).toOption) ∘
          Subtype.val (p := fun (x : Option X) ↦ ¬x = none)))
      b
⊢ Membership.mem (γ := Part ((partialFunToPointed ⋙ pointedToPartialFun).obj Y))
      ((CategoryTheory.Functor.map (𝟭 PartialFun) f ≫
            Iso.hom
              ((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 := ⋯ } :
                    Functor.obj (𝟭 PartialFun) X ≅ (partialFunToPointed ⋙ pointedToPartialFun).obj X))
                Y))
          a :
        Part ((partialFunToPointed ⋙ pointedToPartialFun).obj Y))
      b ↔
    Membership.mem (γ := Part ((partialFunToPointed ⋙ pointedToPartialFun).obj Y))
      ((Iso.hom
              ((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 := ⋯ } :
                    Functor.obj (𝟭 PartialFun) X ≅ (partialFunToPointed ⋙ pointedToPartialFun).obj X))
                X) ≫
            (partialFunToPointed ⋙ pointedToPartialFun).map f)
          a :
        Part ((partialFunToPointed ⋙ pointedToPartialFun).obj Y))
      b

Tactic:
dsimp [PartialFun.Iso.mk, CategoryStruct.comp, pointedToPartialFun]

Premises used: pointedToPartialFun, CategoryTheory.CategoryStruct.comp, PartialFun.Iso.mk
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
rw :
  Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      ((f a).bind fun (x : Y) ↦ Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some x) ⋯)) b ↔
    Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      (Function.comp (α := PartialFun.of { x : Option X // ¬x = none })
        (PFun.toSubtype (fun (x : Option Y) ↦ ¬x = none) (Option.elim' none fun (a : X) ↦ (f a).toOption))
        (Subtype.val (p := fun (x : Option X) ↦ ¬x = none))
        (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯))
      b
⊢ Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      ((f a).bind fun (x : Y) ↦ Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some x) ⋯)) b ↔
    Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      (Part.bind (α := PartialFun.of { x : Option X // ¬x = none })
        (Part.some (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯))
        (PFun.toSubtype (fun (x : Option Y) ↦ ¬x = none) (Option.elim' none fun (a : X) ↦ (f a).toOption) ∘
          Subtype.val (p := fun (x : Option X) ↦ ¬x = none)))
      b

Tactic:
rw [Part.bind_some]

Premises used: Part.bind_some
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
⊢ Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      ((f a).bind fun (x : Y) ↦ Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some x) ⋯)) b ↔
    Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      (Function.comp (α := PartialFun.of { x : Option X // ¬x = none })
        (PFun.toSubtype (fun (x : Option Y) ↦ ¬x = none) (Option.elim' none fun (a : X) ↦ (f a).toOption))
        (Subtype.val (p := fun (x : Option X) ↦ ¬x = none))
        (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯))
      b

Tactic:
(Part.mem_bind_iff.trans ?_).trans PFun.mem_toSubtype_iff.symm

Premises used: Part.mem_bind_iff, PartialFun.of, PFun.mem_toSubtype_iff, Iff.trans, Iff.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
refine :
  (∃ 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) ⋯)) b) ↔
    (↑b : Option Y) =
      Option.elim' none (fun (a : X) ↦ (f a).toOption)
        (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯) : Option X)
⊢ Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      ((f a).bind fun (x : Y) ↦ Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = none) (some x) ⋯)) b ↔
    Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = none }))
      (Function.comp (α := PartialFun.of { x : Option X // ¬x = none })
        (PFun.toSubtype (fun (x : Option Y) ↦ ¬x = none) (Option.elim' none fun (a : X) ↦ (f a).toOption))
        (Subtype.val (p := fun (x : Option X) ↦ ¬x = none))
        (Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) ⋯))
      b

Tactic:
refine (Part.mem_bind_iff.trans ?_).trans PFun.mem_toSubtype_iff.symm

Premises used: Part.mem_bind_iff, PFun.mem_toSubtype_iff, Iff.trans, Iff.symm
-- Module: Mathlib.CategoryTheory.Category.PartialFun
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
none :
  ∀ (hb : Ne.{u + 1} (α := (partialFunToPointed.obj Y).X) Option.none (partialFunToPointed.obj Y).point),
    (∃ a_1 ∈ f a,
        Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = Option.none }))
          (Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = Option.none) (Option.some a_1) ⋯))
          (Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) Option.none
            hb)) ↔
      (↑(Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) Option.none
              hb) :
          Option Y) =
        Option.elim' Option.none (fun (a : X) ↦ (f a).toOption)
          (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = Option.none) (Option.some a) ⋯) : Option X)
some :
  ∀ (b : Y) (hb : Option.some b ≠ (partialFunToPointed.obj Y).point),
    (∃ a_1 ∈ f a,
        Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = Option.none }))
          (Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = Option.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' Option.none (fun (a : X) ↦ (f a).toOption)
          (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = Option.none) (Option.some a) ⋯) : Option X)
⊢ (∃ a_1 ∈ f a,
      Membership.mem (γ := Part (PartialFun.of { x : Option Y // ¬x = Option.none }))
        (Part.some (Subtype.mk (p := fun (x : Option Y) ↦ ¬x = Option.none) (Option.some a_1) ⋯)) b) ↔
    (↑b : Option Y) =
      Option.elim' Option.none (fun (a : X) ↦ (f a).toOption)
        (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = Option.none) (Option.some a) ⋯) : Option X)

Tactic:
obtain ⟨b | b, hb⟩ := b
-- 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:
(hb rfl).elim

Premises used: False.elim, rfl