[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : PartialFun
e : α ≃ β
⊢ ↑((fun x => ↑e.symm x) ∘ fun x => ↑e x) = 𝟙 α
[PROOFSTEP]
simp only [Equiv.symm_comp_self, PFun.coe_id]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : PartialFun
e : α ≃ β
⊢ PFun.id α = 𝟙 α
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : PartialFun
e : α ≃ β
⊢ ↑((fun x => ↑e x) ∘ fun x => ↑e.symm x) = 𝟙 β
[PROOFSTEP]
simp only [Equiv.self_comp_symm, PFun.coe_id]
[GOAL]
α✝ : Type u_1
β✝ : Type u_2
α β : PartialFun
e : α ≃ β
⊢ PFun.id β = 𝟙 β
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ { obj := fun X => { x // x ≠ X.point },
          map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
      (f ≫ g) =
    { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        f ≫
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        g
[PROOFSTEP]
apply PFun.ext _
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ∀
    (a :
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.obj
        X✝)
    (b :
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.obj
        Z✝),
    b ∈
        { obj := fun X => { x // x ≠ X.point },
              map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
          (f ≫ g) a ↔
      b ∈
        ({ obj := fun X => { x // x ≠ X.point },
                  map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
              f ≫
            { obj := fun X => { x // x ≠ X.point },
                  map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
              g)
          a
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨c, hc⟩
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a : X✝.X
ha : a ≠ X✝.point
c : Z✝.X
hc : c ≠ Z✝.point
⊢ { val := c, property := hc } ∈
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        (f ≫ g) { val := a, property := ha } ↔
    { val := c, property := hc } ∈
      ({ obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            f ≫
          { obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            g)
        { val := a, property := ha }
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.mp
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a : X✝.X
ha : a ≠ X✝.point
c : Z✝.X
hc : c ≠ Z✝.point
⊢ { val := c, property := hc } ∈
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        (f ≫ g) { val := a, property := ha } →
    { val := c, property := hc } ∈
      ({ obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            f ≫
          { obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            g)
        { val := a, property := ha }
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mk.mk.mp.intro
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a : X✝.X
ha : a ≠ X✝.point
c : Z✝.X
hc : c ≠ Z✝.point
h₁ :
  ({ obj := fun X => { x // x ≠ X.point },
          map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
      (f ≫ g) { val := a, property := ha }).Dom
h₂ :
  Part.get
      ({ obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        (f ≫ g) { val := a, property := ha })
      h₁ =
    { val := c, property := hc }
⊢ { val := c, property := hc } ∈
    ({ obj := fun X => { x // x ≠ X.point },
              map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
          f ≫
        { obj := fun X => { x // x ≠ X.point },
              map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
          g)
      { val := a, property := ha }
[PROOFSTEP]
exact ⟨⟨fun h₀ => h₁ ((congr_arg g.toFun h₀).trans g.map_point), h₁⟩, h₂⟩
[GOAL]
case mk.mk.mpr
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a : X✝.X
ha : a ≠ X✝.point
c : Z✝.X
hc : c ≠ Z✝.point
⊢ { val := c, property := hc } ∈
      ({ obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            f ≫
          { obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            g)
        { val := a, property := ha } →
    { val := c, property := hc } ∈
      { obj := fun X => { x // x ≠ X.point },
            map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
        (f ≫ g) { val := a, property := ha }
[PROOFSTEP]
rintro ⟨_, _, _⟩
[GOAL]
case mk.mk.mpr.intro.refl
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : Pointed
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
a : X✝.X
ha : a ≠ X✝.point
w✝ :
  (({ obj := fun X => { x // x ≠ X.point },
              map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
          f ≫
        { obj := fun X => { x // x ≠ X.point },
              map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
          g)
      { val := a, property := ha }).Dom
hc :
  Pointed.Hom.toFun g
      ↑(Part.get
          ({ obj := fun X => { x // x ≠ X.point },
                map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
            f { val := a, property := ha })
          (_ :
            ({ obj := fun X => { x // x ≠ X.point },
                    map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
                f { val := a, property := ha }).Dom)) ≠
    Z✝.point
⊢ {
      val :=
        Pointed.Hom.toFun g
          ↑(Part.get
              ({ obj := fun X => { x // x ≠ X.point },
                    map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
                f { val := a, property := ha })
              (_ :
                ({ obj := fun X => { x // x ≠ X.point },
                        map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
                    f { val := a, property := ha }).Dom)),
      property := hc } ∈
    { obj := fun X => { x // x ≠ X.point },
          map := fun {X Y} f => PFun.toSubtype (fun x => x ≠ Y.point) f.toFun ∘ Subtype.val }.map
      (f ≫ g) { val := a, property := ha }
[PROOFSTEP]
exact ⟨_, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
⊢ PartialFun ⥤ Pointed
[PROOFSTEP]
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] }
[GOAL]
α : Type u_1
β : Type u_2
⊢ PartialFun ⥤ Pointed
[PROOFSTEP]
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] }
[GOAL]
α : Type u_1
β : Type u_2
X : PartialFun
o :
  ({ obj := fun X => { X := Option X, point := none },
          map := fun {X Y} f =>
            { toFun := Option.elim' none fun a => Part.toOption (f a),
              map_point :=
                (_ :
                  Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point =
                    Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point) } }.obj
      X).X
a : X
⊢ Pointed.Hom.toFun
      ({ obj := fun X => { X := Option X, point := none },
            map := fun {X Y} f =>
              { toFun := Option.elim' none fun a => Part.toOption (f a),
                map_point :=
                  (_ :
                    Option.elim' none (fun a => Part.toOption (f a))
                        ((fun X => { X := Option X, point := none }) X).point =
                      Option.elim' none (fun a => Part.toOption (f a))
                        ((fun X => { X := Option X, point := none }) X).point) } }.map
        (𝟙 X))
      (some a) =
    Pointed.Hom.toFun
      (𝟙
        ({ obj := fun X => { X := Option X, point := none },
              map := fun {X Y} f =>
                { toFun := Option.elim' none fun a => Part.toOption (f a),
                  map_point :=
                    (_ :
                      Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point =
                        Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point) } }.obj
          X))
      (some a)
[PROOFSTEP]
dsimp [CategoryStruct.id]
[GOAL]
α : Type u_1
β : Type u_2
X : PartialFun
o :
  ({ obj := fun X => { X := Option X, point := none },
          map := fun {X Y} f =>
            { toFun := Option.elim' none fun a => Part.toOption (f a),
              map_point :=
                (_ :
                  Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point =
                    Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point) } }.obj
      X).X
a : X
⊢ Part.toOption (Part.some a) = some a
[PROOFSTEP]
convert Part.some_toOption a
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : PartialFun
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
o :
  ({ obj := fun X => { X := Option X, point := none },
          map := fun {X Y} f =>
            { toFun := Option.elim' none fun a => Part.toOption (f a),
              map_point :=
                (_ :
                  Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point =
                    Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point) } }.obj
      X✝).X
a : X✝
⊢ Pointed.Hom.toFun
      ({ obj := fun X => { X := Option X, point := none },
            map := fun {X Y} f =>
              { toFun := Option.elim' none fun a => Part.toOption (f a),
                map_point :=
                  (_ :
                    Option.elim' none (fun a => Part.toOption (f a))
                        ((fun X => { X := Option X, point := none }) X).point =
                      Option.elim' none (fun a => Part.toOption (f a))
                        ((fun X => { X := Option X, point := none }) X).point) } }.map
        (f ≫ g))
      (some a) =
    Pointed.Hom.toFun
      ({ obj := fun X => { X := Option X, point := none },
              map := fun {X Y} f =>
                { toFun := Option.elim' none fun a => Part.toOption (f a),
                  map_point :=
                    (_ :
                      Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point =
                        Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point) } }.map
          f ≫
        { obj := fun X => { X := Option X, point := none },
              map := fun {X Y} f =>
                { toFun := Option.elim' none fun a => Part.toOption (f a),
                  map_point :=
                    (_ :
                      Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point =
                        Option.elim' none (fun a => Part.toOption (f a))
                          ((fun X => { X := Option X, point := none }) X).point) } }.map
          g)
      (some a)
[PROOFSTEP]
dsimp [CategoryStruct.comp]
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ Z✝ : PartialFun
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
o :
  ({ obj := fun X => { X := Option X, point := none },
          map := fun {X Y} f =>
            { toFun := Option.elim' none fun a => Part.toOption (f a),
              map_point :=
                (_ :
                  Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point =
                    Option.elim' none (fun a => Part.toOption (f a))
                      ((fun X => { X := Option X, point := none }) X).point) } }.obj
      X✝).X
a : X✝
⊢ Part.toOption (Part.bind (f a) g) = Option.elim' none (fun a => Part.toOption (g a)) (Part.toOption (f a))
[PROOFSTEP]
rw [Part.bind_toOption g (f a), Option.elim'_eq_elim]
[GOAL]
α : Type u_1
β : Type u_2
X : PartialFun
a : (partialFunToPointed ⋙ pointedToPartialFun).obj X
⊢ (fun a => { val := some a, property := (_ : some a ≠ none) }) ((fun a => Option.get ↑a (_ : isSome ↑a = true)) a) = a
[PROOFSTEP]
simp only [some_get, Subtype.coe_eta]
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ b ∈
      ((𝟭 PartialFun).map f ≫
          ((fun X =>
                PartialFun.Iso.mk
                  { toFun := fun a => { val := some a, property := (_ : some a ≠ none) },
                    invFun := fun a => Option.get ↑a (_ : isSome ↑a = true),
                    left_inv :=
                      (_ :
                        ∀ (a : (𝟭 PartialFun).obj X),
                          Option.get (some a)
                              (_ : isSome ↑((fun a => { val := some a, property := (_ : some a ≠ none) }) a) = true) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X),
                          { val := some ((fun a => Option.get ↑a (_ : isSome ↑a = true)) a),
                              property := (_ : some ((fun a => Option.get ↑a (_ : isSome ↑a = true)) a) ≠ none) } =
                            a) })
              Y✝).hom)
        a ↔
    b ∈
      (((fun X =>
                PartialFun.Iso.mk
                  { toFun := fun a => { val := some a, property := (_ : some a ≠ none) },
                    invFun := fun a => Option.get ↑a (_ : isSome ↑a = true),
                    left_inv :=
                      (_ :
                        ∀ (a : (𝟭 PartialFun).obj X),
                          Option.get (some a)
                              (_ : isSome ↑((fun a => { val := some a, property := (_ : some a ≠ none) }) a) = true) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (a : (partialFunToPointed ⋙ pointedToPartialFun).obj X),
                          { val := some ((fun a => Option.get ↑a (_ : isSome ↑a = true)) a),
                              property := (_ : some ((fun a => Option.get ↑a (_ : isSome ↑a = true)) a) ≠ none) } =
                            a) })
              X✝).hom ≫
          (partialFunToPointed ⋙ pointedToPartialFun).map f)
        a
[PROOFSTEP]
dsimp [PartialFun.Iso.mk, CategoryStruct.comp, pointedToPartialFun]
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ (b ∈ Part.bind (f a) fun x => Part.some { val := some x, property := (_ : some x ≠ none) }) ↔
    b ∈
      Part.bind (Part.some { val := some a, property := (_ : some a ≠ none) })
        (PFun.toSubtype (fun x => ¬x = (partialFunToPointed.obj Y✝).point)
            (Option.elim' none fun a => Part.toOption (f a)) ∘
          Subtype.val)
[PROOFSTEP]
rw [Part.bind_some]
  -- porting note: the proof below has changed a lot because
            -- `Part.mem_bind_iff` means that `b ∈ Part.bind f g` is equivalent
            -- to `∃ (a : α), a ∈ f ∧ b ∈ g a`, while in mathlib3 it was equivalent
            -- to `∃ (a : α) (H : a ∈ f), b ∈ g a`
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ (b ∈ Part.bind (f a) fun x => Part.some { val := some x, property := (_ : some x ≠ none) }) ↔
    b ∈
      (PFun.toSubtype (fun x => ¬x = (partialFunToPointed.obj Y✝).point)
            (Option.elim' none fun a => Part.toOption (f a)) ∘
          Subtype.val)
        { val := some a, property := (_ : some a ≠ none) }
[PROOFSTEP]
refine' (Part.mem_bind_iff.trans _).trans PFun.mem_toSubtype_iff.symm
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : (partialFunToPointed ⋙ pointedToPartialFun).obj Y✝
⊢ (∃ a_1, a_1 ∈ f a ∧ b ∈ Part.some { val := some a_1, property := (_ : some a_1 ≠ none) }) ↔
    ↑b = Option.elim' none (fun a => Part.toOption (f a)) ↑{ val := some a, property := (_ : some a ≠ none) }
[PROOFSTEP]
obtain ⟨b | b, hb⟩ := b
[GOAL]
case mk.none
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
hb : none ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1,
      a_1 ∈ f a ∧ { val := none, property := hb } ∈ Part.some { val := some a_1, property := (_ : some a_1 ≠ none) }) ↔
    ↑{ val := none, property := hb } =
      Option.elim' none (fun a => Part.toOption (f a)) ↑{ val := some a, property := (_ : some a ≠ none) }
[PROOFSTEP]
exact (hb rfl).elim
[GOAL]
case mk.some
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1,
      a_1 ∈ f a ∧
        { val := some b, property := hb } ∈ Part.some { val := some a_1, property := (_ : some a_1 ≠ none) }) ↔
    ↑{ val := some b, property := hb } =
      Option.elim' none (fun a => Part.toOption (f a)) ↑{ val := some a, property := (_ : some a ≠ none) }
[PROOFSTEP]
dsimp [Part.toOption]
[GOAL]
case mk.some
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1,
      a_1 ∈ f a ∧
        { val := some b, property := hb } ∈ Part.some { val := some a_1, property := (_ : some a_1 ≠ none) }) ↔
    some b = if h : (f a).Dom then some (Part.get (f a) h) else none
[PROOFSTEP]
simp_rw [Part.mem_some_iff, Subtype.mk_eq_mk]
[GOAL]
case mk.some
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1, a_1 ∈ f a ∧ some b = some a_1) ↔ some b = if h : (f a).Dom then some (Part.get (f a) h) else none
[PROOFSTEP]
constructor
[GOAL]
case mk.some.mp
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (∃ a_1, a_1 ∈ f a ∧ some b = some a_1) → some b = if h : (f a).Dom then some (Part.get (f a) h) else none
[PROOFSTEP]
rintro ⟨_, ⟨h₁, h₂⟩, h₃⟩
[GOAL]
case mk.some.mp.intro.intro.intro
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
w✝ : Y✝
h₃ : some b = some w✝
h₁ : (f a).Dom
h₂ : Part.get (f a) h₁ = w✝
⊢ some b = if h : (f a).Dom then some (Part.get (f a) h) else none
[PROOFSTEP]
rw [h₃, ← h₂, dif_pos h₁]
[GOAL]
case mk.some.mpr
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
⊢ (some b = if h : (f a).Dom then some (Part.get (f a) h) else none) → ∃ a_2, a_2 ∈ f a ∧ some b = some a_2
[PROOFSTEP]
intro h
[GOAL]
case mk.some.mpr
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
h : some b = if h : (f a).Dom then some (Part.get (f a) h) else none
⊢ ∃ a_1, a_1 ∈ f a ∧ some b = some a_1
[PROOFSTEP]
split_ifs at h  with ha
[GOAL]
case pos
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
ha : (f a).Dom
h : some b = some (Part.get (f a) ha)
⊢ ∃ a_1, a_1 ∈ f a ∧ some b = some a_1
[PROOFSTEP]
rw [some_inj] at h
[GOAL]
case pos
α : Type u_1
β : Type u_2
X✝ Y✝ : PartialFun
f : X✝ ⟶ Y✝
a : (𝟭 PartialFun).obj X✝
b : Y✝
hb : some b ≠ (partialFunToPointed.obj Y✝).point
ha : (f a).Dom
h : b = Part.get (f a) ha
⊢ ∃ a_1, a_1 ∈ f a ∧ some b = some a_1
[PROOFSTEP]
refine' ⟨b, ⟨ha, h.symm⟩, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
[PROOFSTEP]
classical exact if h : a = X.point then none else some ⟨_, h⟩
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
⊢ ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
[PROOFSTEP]
exact if h : a = X.point then none else some ⟨_, h⟩
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : pointedToPartialFun.obj X
⊢ (fun a => if h : a = X.point then none else some { val := a, property := h })
      (Option.elim' X.point Subtype.val (some a)) =
    some a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : pointedToPartialFun.obj X
⊢ (if h : ↑a = X.point then none else some { val := ↑a, property := h }) = some a
[PROOFSTEP]
rw [dif_neg a.2]
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : pointedToPartialFun.obj X
⊢ some { val := ↑a, property := (_ : ↑a ≠ X.point) } = some a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
⊢ Option.elim' X.point Subtype.val ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) = a
[PROOFSTEP]
dsimp
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
⊢ Option.elim' X.point Subtype.val (if h : a = X.point then none else some { val := a, property := h }) = a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
h : a = X.point
⊢ Option.elim' X.point Subtype.val none = a
[PROOFSTEP]
rw [h]
[GOAL]
case pos
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
h : a = X.point
⊢ Option.elim' X.point Subtype.val none = X.point
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
X : Pointed
a : ((𝟭 Pointed).obj X).X
h : ¬a = X.point
⊢ Option.elim' X.point Subtype.val (some { val := a, property := h }) = a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
⊢ ∀ (val : pointedToPartialFun.obj X),
    Pointed.Hom.toFun
        ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
          ((fun X =>
                Pointed.Iso.mk
                  { toFun := Option.elim' X.point Subtype.val,
                    invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                    left_inv :=
                      (_ :
                        ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                          (fun a => if h : a = X.point then none else some { val := a, property := h })
                              (Option.elim' X.point Subtype.val a) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (a : ((𝟭 Pointed).obj X).X),
                          Option.elim' X.point Subtype.val
                              ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                            a) }
                  (_ :
                    ↑{ toFun := Option.elim' X.point Subtype.val,
                            invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                            left_inv :=
                              (_ :
                                ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                  (fun a => if h : a = X.point then none else some { val := a, property := h })
                                      (Option.elim' X.point Subtype.val a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (a : ((𝟭 Pointed).obj X).X),
                                  Option.elim' X.point Subtype.val
                                      ((fun a => if h : a = X.point then none else some { val := a, property := h })
                                        a) =
                                    a) }
                        ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point =
                      ↑{ toFun := Option.elim' X.point Subtype.val,
                            invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                            left_inv :=
                              (_ :
                                ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                  (fun a => if h : a = X.point then none else some { val := a, property := h })
                                      (Option.elim' X.point Subtype.val a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (a : ((𝟭 Pointed).obj X).X),
                                  Option.elim' X.point Subtype.val
                                      ((fun a => if h : a = X.point then none else some { val := a, property := h })
                                        a) =
                                    a) }
                        ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point))
              Y).hom)
        (some val) =
      Pointed.Hom.toFun
        (((fun X =>
                Pointed.Iso.mk
                  { toFun := Option.elim' X.point Subtype.val,
                    invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                    left_inv :=
                      (_ :
                        ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                          (fun a => if h : a = X.point then none else some { val := a, property := h })
                              (Option.elim' X.point Subtype.val a) =
                            a),
                    right_inv :=
                      (_ :
                        ∀ (a : ((𝟭 Pointed).obj X).X),
                          Option.elim' X.point Subtype.val
                              ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                            a) }
                  (_ :
                    ↑{ toFun := Option.elim' X.point Subtype.val,
                            invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                            left_inv :=
                              (_ :
                                ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                  (fun a => if h : a = X.point then none else some { val := a, property := h })
                                      (Option.elim' X.point Subtype.val a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (a : ((𝟭 Pointed).obj X).X),
                                  Option.elim' X.point Subtype.val
                                      ((fun a => if h : a = X.point then none else some { val := a, property := h })
                                        a) =
                                    a) }
                        ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point =
                      ↑{ toFun := Option.elim' X.point Subtype.val,
                            invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                            left_inv :=
                              (_ :
                                ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                  (fun a => if h : a = X.point then none else some { val := a, property := h })
                                      (Option.elim' X.point Subtype.val a) =
                                    a),
                            right_inv :=
                              (_ :
                                ∀ (a : ((𝟭 Pointed).obj X).X),
                                  Option.elim' X.point Subtype.val
                                      ((fun a => if h : a = X.point then none else some { val := a, property := h })
                                        a) =
                                    a) }
                        ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point))
              X).hom ≫
          (𝟭 Pointed).map f)
        (some val)
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mk
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
⊢ Pointed.Hom.toFun
      ((pointedToPartialFun ⋙ partialFunToPointed).map f ≫
        ((fun X =>
              Pointed.Iso.mk
                { toFun := Option.elim' X.point Subtype.val,
                  invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                  left_inv :=
                    (_ :
                      ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                        (fun a => if h : a = X.point then none else some { val := a, property := h })
                            (Option.elim' X.point Subtype.val a) =
                          a),
                  right_inv :=
                    (_ :
                      ∀ (a : ((𝟭 Pointed).obj X).X),
                        Option.elim' X.point Subtype.val
                            ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                          a) }
                (_ :
                  ↑{ toFun := Option.elim' X.point Subtype.val,
                          invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                          left_inv :=
                            (_ :
                              ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                (fun a => if h : a = X.point then none else some { val := a, property := h })
                                    (Option.elim' X.point Subtype.val a) =
                                  a),
                          right_inv :=
                            (_ :
                              ∀ (a : ((𝟭 Pointed).obj X).X),
                                Option.elim' X.point Subtype.val
                                    ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                                  a) }
                      ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point =
                    ↑{ toFun := Option.elim' X.point Subtype.val,
                          invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                          left_inv :=
                            (_ :
                              ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                (fun a => if h : a = X.point then none else some { val := a, property := h })
                                    (Option.elim' X.point Subtype.val a) =
                                  a),
                          right_inv :=
                            (_ :
                              ∀ (a : ((𝟭 Pointed).obj X).X),
                                Option.elim' X.point Subtype.val
                                    ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                                  a) }
                      ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point))
            Y).hom)
      (some { val := a, property := ha }) =
    Pointed.Hom.toFun
      (((fun X =>
              Pointed.Iso.mk
                { toFun := Option.elim' X.point Subtype.val,
                  invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                  left_inv :=
                    (_ :
                      ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                        (fun a => if h : a = X.point then none else some { val := a, property := h })
                            (Option.elim' X.point Subtype.val a) =
                          a),
                  right_inv :=
                    (_ :
                      ∀ (a : ((𝟭 Pointed).obj X).X),
                        Option.elim' X.point Subtype.val
                            ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                          a) }
                (_ :
                  ↑{ toFun := Option.elim' X.point Subtype.val,
                          invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                          left_inv :=
                            (_ :
                              ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                (fun a => if h : a = X.point then none else some { val := a, property := h })
                                    (Option.elim' X.point Subtype.val a) =
                                  a),
                          right_inv :=
                            (_ :
                              ∀ (a : ((𝟭 Pointed).obj X).X),
                                Option.elim' X.point Subtype.val
                                    ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                                  a) }
                      ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point =
                    ↑{ toFun := Option.elim' X.point Subtype.val,
                          invFun := fun a => if h : a = X.point then none else some { val := a, property := h },
                          left_inv :=
                            (_ :
                              ∀ (a : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X),
                                (fun a => if h : a = X.point then none else some { val := a, property := h })
                                    (Option.elim' X.point Subtype.val a) =
                                  a),
                          right_inv :=
                            (_ :
                              ∀ (a : ((𝟭 Pointed).obj X).X),
                                Option.elim' X.point Subtype.val
                                    ((fun a => if h : a = X.point then none else some { val := a, property := h }) a) =
                                  a) }
                      ((pointedToPartialFun ⋙ partialFunToPointed).obj X).point))
            X).hom ≫
        (𝟭 Pointed).map f)
      (some { val := a, property := ha })
[PROOFSTEP]
change Option.elim' _ _ _ = f.toFun a
[GOAL]
case mk
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
⊢ Option.elim' Y.point (fun a => ↑a)
      (Pointed.Hom.toFun ((pointedToPartialFun ⋙ partialFunToPointed).map f) (some { val := a, property := ha })) =
    Pointed.Hom.toFun f a
[PROOFSTEP]
dsimp
  -- porting note: `rw [Part.elim_toOption]` does not work because there are
              -- conflicting `Decidable` instances
[GOAL]
case mk
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
⊢ Option.elim' Y.point (fun a => ↑a)
      (Part.toOption { Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) }) =
    Pointed.Hom.toFun f a
[PROOFSTEP]
rw [Option.elim'_eq_elim, @Part.elim_toOption _ _ _ (Classical.propDecidable _)]
[GOAL]
case mk
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
⊢ (if h : { Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) }.Dom then
      ↑(Part.get { Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) } h)
    else Y.point) =
    Pointed.Hom.toFun f a
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
h : { Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) }.Dom
⊢ ↑(Part.get { Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) } h) =
    Pointed.Hom.toFun f a
[PROOFSTEP]
rfl
[GOAL]
case neg
α : Type u_1
β : Type u_2
X Y : Pointed
f : X ⟶ Y
a✝ : ((pointedToPartialFun ⋙ partialFunToPointed).obj X).X
a : X.X
ha : a ≠ X.point
h : ¬{ Dom := ¬Pointed.Hom.toFun f a = Y.point, get := Subtype.mk (Pointed.Hom.toFun f a) }.Dom
⊢ Y.point = Pointed.Hom.toFun f a
[PROOFSTEP]
exact Eq.symm (of_not_not h)
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : Type ?u.22242
f : X✝ ⟶ Y✝
a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X
a : typeToPartialFun.obj X✝
⊢ Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        ((fun X =>
              Iso.mk
                { toFun := id,
                  map_point :=
                    (_ :
                      id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point =
                        id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point) }
                { toFun := id, map_point := (_ : id (typeToPointed.obj X).point = id (typeToPointed.obj X).point) })
            Y✝).hom)
      (some a) =
    Pointed.Hom.toFun
      (((fun X =>
              Iso.mk
                { toFun := id,
                  map_point :=
                    (_ :
                      id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point =
                        id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point) }
                { toFun := id, map_point := (_ : id (typeToPointed.obj X).point = id (typeToPointed.obj X).point) })
            X✝).hom ≫
        typeToPointed.map f)
      (some a)
[PROOFSTEP]
classical convert Part.some_toOption _
[GOAL]
α : Type u_1
β : Type u_2
X✝ Y✝ : Type ?u.22242
f : X✝ ⟶ Y✝
a✝ : ((typeToPartialFun ⋙ partialFunToPointed).obj X✝).X
a : typeToPartialFun.obj X✝
⊢ Pointed.Hom.toFun
      ((typeToPartialFun ⋙ partialFunToPointed).map f ≫
        ((fun X =>
              Iso.mk
                { toFun := id,
                  map_point :=
                    (_ :
                      id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point =
                        id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point) }
                { toFun := id, map_point := (_ : id (typeToPointed.obj X).point = id (typeToPointed.obj X).point) })
            Y✝).hom)
      (some a) =
    Pointed.Hom.toFun
      (((fun X =>
              Iso.mk
                { toFun := id,
                  map_point :=
                    (_ :
                      id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point =
                        id ((typeToPartialFun ⋙ partialFunToPointed).obj X).point) }
                { toFun := id, map_point := (_ : id (typeToPointed.obj X).point = id (typeToPointed.obj X).point) })
            X✝).hom ≫
        typeToPointed.map f)
      (some a)
[PROOFSTEP]
convert Part.some_toOption _