awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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)
⊢ (∃ (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)
have 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)) sorry)
      (Subtype.mk (p := fun (x : Z.X) ↦ ¬x = Z.point) c hc)),
  c = g.toFun (f.toFun a)
Tactic: simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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
⊢ (↑(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)
have suffices : c = g.toFun (f.toFun a) → ¬Y.point = f.toFun a ∧ ¬Z.point = g.toFun (f.toFun a)
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⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X : PartialFun
o : { X := Option X, point := none }.X
a : X
⊢ 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)
have dsimp : (Part.some a).toOption = some a
Tactic: dsimp [CategoryStruct.id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y Z : PartialFun
f : X ⟶ Y
g : Y ⟶ Z
o : { X := Option X, point := none }.X
a : X
⊢ 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))
have dsimp : ((f a).bind g).toOption = Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption
Tactic: dsimp [CategoryStruct.comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y Z : PartialFun
f : X ⟶ Y
g : Y ⟶ Z
o : { X := Option X, point := none }.X
a : X
⊢ ((f a).bind g).toOption = Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption
have 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)
Tactic: rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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)
⊢ ((f a).bind g).toOption = Option.elim' none (fun (a : Y) ↦ (g a).toOption) (f a).toOption
have 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)
Tactic: rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
⊢ 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
have 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) sorry)) 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) sorry))
      (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: dsimp [PartialFun.Iso.mk, CategoryStruct.comp, pointedToPartialFun]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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 }))
      (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
have 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) sorry)) 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) sorry))
    b
Tactic: rw [Part.bind_some]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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
have 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) sorry)) b) ↔
  (↑b : Option Y) =
    Option.elim' none (fun (a : X) ↦ (f a).toOption)
      (↑(Subtype.mk (p := fun (x : Option X) ↦ ¬x = none) (some a) sorry) : Option X)
Tactic: refine (Part.mem_bind_iff.trans ?_).trans PFun.mem_toSubtype_iff.symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
Goal:
X Y : PartialFun
f : X ⟶ Y
a : Functor.obj (𝟭 PartialFun) X
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y
⊢ (∃ 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)
have none : ∀ (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) sorry))
        (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) sorry) : Option X)
Tactic: obtain ⟨b | b, hb⟩ := b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (goal)
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) (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) (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) (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) (some a) ⋯) : Option X)
have some : ∀ (b : Y) (hb : 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) (some a_1) sorry))
        (Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) (some b)
          hb)) ↔
    (↑(Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) (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) (some a) sorry) : Option X)
Tactic: obtain ⟨b | b, hb⟩ := b
Cleared hypotheses: b
-- 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 : some b ≠ (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) (some b)
          hb)) ↔
    (↑(Subtype.mk (p := fun (x : (partialFunToPointed.obj Y).X) ↦ x ≠ (partialFunToPointed.obj Y).point) (some b) 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)
have some : (∃ 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) sorry)) ↔
  some b = (f a).toOption
Tactic: simp only [partialFunToPointed_obj, ne_eq, Part.mem_some_iff, elim'_some]
-- 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 : 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
have some : (∃ 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) sorry)) →
  ∀ (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) sorry)),
    some b = (f a).toOption
Tactic: refine ⟨fun ⟨w, hw, h⟩ ↦ ?_, fun h ↦ ⟨b, Part.mem_toOption.mp h.symm, rfl⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (hypothesis)
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) ⋯)
⊢ some b = (f a).toOption
have h₁ : (↑(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) sorry) : Option Y)
Tactic: rw [Subtype.ext_iff] at h
Cleared hypotheses: h
-- 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 : 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
⊢ some b = (f a).toOption
have some : some w = (f a).toOption
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.CategoryTheory.Category.PartialFun (hypothesis)
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
⊢ some w = (f a).toOption
have hw₁ : (f a).toOption = some w
Tactic: rw [← Part.mem_toOption, mem_def] at hw
Cleared hypotheses: hw, h
-- 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 : 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
have some : (∃ 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) sorry)) →
  ∀ (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) sorry)),
    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
-- 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
⊢ (∃ 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 :
      (↑(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) sorry) : Option Y)),
    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
-- 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
⊢ (∃ 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 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