[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
⊢ ∀ (a b : f ⟶ g), a = b
[PROOFSTEP]
intro h₁ h₂
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ h₁ = h₂
[PROOFSTEP]
apply Over.OverMorphism.ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ h₁.left = h₂.left
[PROOFSTEP]
erw [← cancel_mono g.arrow, Over.w h₁, Over.w h₂]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
f g : MonoOver X
h : f.obj.left ≅ g.obj.left
w : autoParam (h.hom ≫ arrow g = arrow f) _auto✝
⊢ h.inv ≫ arrow f = arrow g
[PROOFSTEP]
rw [h.inv_comp_eq, w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : MonoOver Y
⊢ Mono ((Over.pullback f).obj ((forget Y).obj g)).hom
[PROOFSTEP]
haveI : Mono ((forget Y).obj g).hom := (inferInstance : Mono g.arrow)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : MonoOver Y
this : Mono ((forget Y).obj g).hom
⊢ Mono ((Over.pullback f).obj ((forget Y).obj g)).hom
[PROOFSTEP]
apply pullback.snd_of_mono
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g : MonoOver X
⊢ Mono ((Over.map f).obj ((forget X).obj g)).hom
[PROOFSTEP]
apply mono_comp g.arrow f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ g ⟶ h
[PROOFSTEP]
refine' homMk e.left _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ e.left ≫ arrow h = arrow g
[PROOFSTEP]
rw [← cancel_mono f, assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ e.left ≫ arrow h ≫ f = arrow g ≫ f
[PROOFSTEP]
apply w e
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.hom ≫ e.inv) = map (𝟙 A)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.inv ≫ e.hom) = map (𝟙 B)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver X
⊢ Mono ((Over.post e.functor).obj ((forget X).obj f)).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver X
⊢ Mono (e.functor.map (arrow f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver (e.functor.obj X)
⊢ Mono ((Over.post e.inverse).obj ((forget (e.functor.obj X)).obj f)).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver (e.functor.obj X)
⊢ Mono (e.inverse.map (arrow f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ (fun f => imageMonoOver f.hom) f ⟶ (fun f => imageMonoOver f.hom) g
[PROOFSTEP]
apply (forget X).preimage _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ (forget X).obj ((fun f => imageMonoOver f.hom) f) ⟶ (forget X).obj ((fun f => imageMonoOver f.hom) g)
[PROOFSTEP]
apply Over.homMk _ _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ((forget X).obj ((fun f => imageMonoOver f.hom) f)).left ⟶ ((forget X).obj ((fun f => imageMonoOver f.hom) g)).left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ?m.186308 ≫ ((forget X).obj ((fun f => imageMonoOver f.hom) g)).hom =
    ((forget X).obj ((fun f => imageMonoOver f.hom) f)).hom
[PROOFSTEP]
refine'
  image.lift
    { I := Limits.image _
      m := image.ι g.hom
      e := k.left ≫ factorThruImage g.hom }
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ image.lift (MonoFactorisation.mk (Limits.image g.hom) (image.ι g.hom) (k.left ≫ factorThruImage g.hom)) ≫
      ((forget X).obj ((fun f => imageMonoOver f.hom) g)).hom =
    ((forget X).obj ((fun f => imageMonoOver f.hom) f)).hom
[PROOFSTEP]
apply image.lift_fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ f ⟶ (forget X).obj g
[PROOFSTEP]
apply Over.homMk (factorThruImage f.hom ≫ k.left) _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ (factorThruImage f.hom ≫ k.left) ≫ g.obj.hom = f.hom
[PROOFSTEP]
change (factorThruImage f.hom ≫ k.left) ≫ _ = f.hom
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ (factorThruImage f.hom ≫ k.left) ≫ g.obj.hom = f.hom
[PROOFSTEP]
rw [assoc, Over.w k]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ factorThruImage f.hom ≫ (image.obj f).obj.hom = f.hom
[PROOFSTEP]
apply image.fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ image.obj f ⟶ g
[PROOFSTEP]
refine' Over.homMk _ _
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ (image.obj f).obj.left ⟶ g.obj.left
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ ?refine'_1 ≫ g.obj.hom = (image.obj f).obj.hom
[PROOFSTEP]
refine'
  image.lift
    { I := g.obj.left
      m := g.arrow
      e := k.left
      fac := Over.w k }
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left) ≫ g.obj.hom = (image.obj f).obj.hom
[PROOFSTEP]
apply image.lift_fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ (fun k => Over.homMk (factorThruImage f.hom ≫ k.left))
      ((fun k => Over.homMk (image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left))) k) =
    k
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ ((fun k => Over.homMk (factorThruImage f.hom ≫ k.left))
        ((fun k => Over.homMk (image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left))) k)).left =
    k.left
[PROOFSTEP]
change factorThruImage _ ≫ image.lift _ = _
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ factorThruImage f.hom ≫ image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left) = k.left
[PROOFSTEP]
rw [← cancel_mono g.arrow, assoc, image.lift_fac, image.fac f.hom]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ f.hom = k.left ≫ arrow g
[PROOFSTEP]
exact (Over.w k).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
⊢ (X_1 : MonoOver X) → (exists f).obj X_1 ≅ (map f).obj X_1
[PROOFSTEP]
intro Z
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (exists f).obj Z ≅ (map f).obj Z
[PROOFSTEP]
suffices : (forget _).obj ((exists f).obj Z) ≅ (forget _).obj ((map f).obj Z)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
this : (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
⊢ (exists f).obj Z ≅ (map f).obj Z
case this
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
[PROOFSTEP]
apply (forget _).preimageIso this
[GOAL]
case this
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
[PROOFSTEP]
apply Over.isoMk _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ ((forget Y).obj ((exists f).obj Z)).left ≅ ((forget Y).obj ((map f).obj Z)).left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ ?m.226355.hom ≫ ((forget Y).obj ((map f).obj Z)).hom = ((forget Y).obj ((exists f).obj Z)).hom
[PROOFSTEP]
apply imageMonoIsoSource (Z.arrow ≫ f)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (imageMonoIsoSource (arrow Z ≫ f)).hom ≫ ((forget Y).obj ((map f).obj Z)).hom =
    ((forget Y).obj ((exists f).obj Z)).hom
[PROOFSTEP]
apply imageMonoIsoSource_hom_self


[GOAL]
α : Type u_1
β : Type u_2
X Y Z : Bipointed
f : Bipointed.Hom X Y
g : Bipointed.Hom Y Z
⊢ (g.toFun ∘ f.toFun) X.toProd.fst = Z.toProd.fst
[PROOFSTEP]
rw [Function.comp_apply, f.map_fst, g.map_fst]
[GOAL]
α : Type u_1
β : Type u_2
X Y Z : Bipointed
f : Bipointed.Hom X Y
g : Bipointed.Hom Y Z
⊢ (g.toFun ∘ f.toFun) X.toProd.snd = Z.toProd.snd
[PROOFSTEP]
rw [Function.comp_apply, f.map_snd, g.map_snd]
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ (fun f =>
        { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
          map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
          map_snd :=
            (_ :
              (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) })
      ((fun f =>
          { toFun := f.toFun ∘ some,
            map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
        f) =
    f
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
            map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                  (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
          f)).toFun =
    f.toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
x : (pointedToBipointedFst.obj X).X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
            map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                  (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
          f))
      x =
    Bipointed.Hom.toFun f x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
            map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                  (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
          f))
      none =
    Bipointed.Hom.toFun f none
[PROOFSTEP]
exact f.map_snd.symm
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedFst.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
            map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
            map_snd :=
              (_ :
                (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                  (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ ↑((fun X Y =>
              {
                toFun := fun f =>
                  { toFun := f.toFun ∘ some,
                    map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                invFun := fun f =>
                  { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                    map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                    map_snd :=
                      (_ :
                        (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                left_inv :=
                  (_ :
                    ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                      (fun f =>
                            { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                              map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                              map_snd :=
                                (_ :
                                  (fun o => Option.elim o Y.toProd.snd f.toFun)
                                      (pointedToBipointedFst.obj X).toProd.snd =
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                      (pointedToBipointedFst.obj X).toProd.snd) })
                          ((fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                      (fun f =>
                            { toFun := f.toFun ∘ some,
                              map_point :=
                                (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                          ((fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            f) =
                        f) })
            X'✝ Y✝).symm
      (f ≫ g) =
    pointedToBipointedFst.map f ≫
      ↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                      map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              f) =
                          f) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                      map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g)).toFun =
    (pointedToBipointedFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                        map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                              (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst =
                                          Y.toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                    map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd =
                                          (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g).toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
x : (pointedToBipointedFst.obj X'✝).X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                      map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      x =
    Bipointed.Hom.toFun
      (pointedToBipointedFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                        map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                              (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst =
                                          Y.toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                    map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd =
                                          (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                      map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      none =
    Bipointed.Hom.toFun
      (pointedToBipointedFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                        map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                              (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst =
                                          Y.toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                    map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd =
                                          (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      none
[PROOFSTEP]
rfl
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedFst.obj Y✝
val✝ : X'✝.X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                      map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                      map_snd :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                map_snd :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd =
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                        (pointedToBipointedFst.obj X).toProd.snd) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      (some val✝) =
    Bipointed.Hom.toFun
      (pointedToBipointedFst.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                        map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                        map_snd :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd =
                              (fun o => Option.elim o Y.toProd.snd f.toFun) (pointedToBipointedFst.obj X).toProd.snd) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedFst.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                  map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                  map_snd :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd =
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                          (pointedToBipointedFst.obj X).toProd.snd) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst =
                                          Y.toProd.fst) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedFst.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedFst.obj X).toProd.fst = Y.toProd.fst) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.snd f.toFun,
                                    map_fst := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedFst.obj Y).point),
                                    map_snd :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd =
                                          (fun o => Option.elim o Y.toProd.snd f.toFun)
                                            (pointedToBipointedFst.obj X).toProd.snd) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ (fun f =>
        { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
          map_fst :=
            (_ :
              (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
          map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
      ((fun f =>
          { toFun := f.toFun ∘ some,
            map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
        f) =
    f
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                  (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
            map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
          f)).toFun =
    f.toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
x : (pointedToBipointedSnd.obj X).X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                  (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
            map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
          f))
      x =
    Bipointed.Hom.toFun f x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                  (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
            map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
          f))
      none =
    Bipointed.Hom.toFun f none
[PROOFSTEP]
exact f.map_fst.symm
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X : Pointed
Y : Bipointed
f : pointedToBipointedSnd.obj X ⟶ Y
val✝ : X.X
⊢ Bipointed.Hom.toFun
      ((fun f =>
          { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
            map_fst :=
              (_ :
                (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                  (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
            map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
        ((fun f =>
            { toFun := f.toFun ∘ some,
              map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
          f))
      (some val✝) =
    Bipointed.Hom.toFun f (some val✝)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ ↑((fun X Y =>
              {
                toFun := fun f =>
                  { toFun := f.toFun ∘ some,
                    map_point := (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                invFun := fun f =>
                  { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                    map_fst :=
                      (_ :
                        (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                    map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                left_inv :=
                  (_ :
                    ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                      (fun f =>
                            { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                              map_fst :=
                                (_ :
                                  (fun o => Option.elim o Y.toProd.fst f.toFun)
                                      (pointedToBipointedSnd.obj X).toProd.fst =
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                      (pointedToBipointedSnd.obj X).toProd.fst),
                              map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                          ((fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            f) =
                        f),
                right_inv :=
                  (_ :
                    ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                      (fun f =>
                            { toFun := f.toFun ∘ some,
                              map_point :=
                                (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                          ((fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            f) =
                        f) })
            X'✝ Y✝).symm
      (f ≫ g) =
    pointedToBipointedSnd.map f ≫
      ↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                      map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              f) =
                          f) })
              X✝ Y✝).symm
        g
[PROOFSTEP]
apply Bipointed.Hom.ext
[GOAL]
case toFun
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                      map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g)).toFun =
    (pointedToBipointedSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                              (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                        map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd =
                                          Y.toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst =
                                          (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst),
                                    map_snd :=
                                      (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g).toFun
[PROOFSTEP]
funext x
[GOAL]
case toFun.h
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
x : (pointedToBipointedSnd.obj X'✝).X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                      map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      x =
    Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                              (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                        map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd =
                                          Y.toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst =
                                          (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst),
                                    map_snd :=
                                      (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      x
[PROOFSTEP]
cases x
[GOAL]
case toFun.h.none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                      map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      none =
    Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                              (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                        map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd =
                                          Y.toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst =
                                          (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst),
                                    map_snd :=
                                      (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      none
[PROOFSTEP]
rfl
[GOAL]
case toFun.h.some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : Bipointed
f : X'✝ ⟶ X✝
g : X✝ ⟶ bipointedToPointedSnd.obj Y✝
val✝ : X'✝.X
⊢ Bipointed.Hom.toFun
      (↑((fun X Y =>
                {
                  toFun := fun f =>
                    { toFun := f.toFun ∘ some,
                      map_point :=
                        (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                  invFun := fun f =>
                    { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                      map_fst :=
                        (_ :
                          (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                      map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                  left_inv :=
                    (_ :
                      ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                        (fun f =>
                              { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                map_fst :=
                                  (_ :
                                    (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst =
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                        (pointedToBipointedSnd.obj X).toProd.fst),
                                map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                            ((fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              f) =
                          f),
                  right_inv :=
                    (_ :
                      ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                        (fun f =>
                              { toFun := f.toFun ∘ some,
                                map_point :=
                                  (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                            ((fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              f) =
                          f) })
              X'✝ Y✝).symm
        (f ≫ g))
      (some val✝) =
    Bipointed.Hom.toFun
      (pointedToBipointedSnd.map f ≫
        ↑((fun X Y =>
                  {
                    toFun := fun f =>
                      { toFun := f.toFun ∘ some,
                        map_point :=
                          (_ : Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) },
                    invFun := fun f =>
                      { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                        map_fst :=
                          (_ :
                            (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst =
                              (fun o => Option.elim o Y.toProd.fst f.toFun) (pointedToBipointedSnd.obj X).toProd.fst),
                        map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) },
                    left_inv :=
                      (_ :
                        ∀ (f : pointedToBipointedSnd.obj X ⟶ Y),
                          (fun f =>
                                { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                  map_fst :=
                                    (_ :
                                      (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst =
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                          (pointedToBipointedSnd.obj X).toProd.fst),
                                  map_snd := (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                              ((fun f =>
                                  { toFun := f.toFun ∘ some,
                                    map_point :=
                                      (_ :
                                        Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd =
                                          Y.toProd.snd) })
                                f) =
                            f),
                    right_inv :=
                      (_ :
                        ∀ (f : X ⟶ bipointedToPointedSnd.obj Y),
                          (fun f =>
                                { toFun := f.toFun ∘ some,
                                  map_point :=
                                    (_ :
                                      Bipointed.Hom.toFun f (pointedToBipointedSnd.obj X).toProd.snd = Y.toProd.snd) })
                              ((fun f =>
                                  { toFun := fun o => Option.elim o Y.toProd.fst f.toFun,
                                    map_fst :=
                                      (_ :
                                        (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst =
                                          (fun o => Option.elim o Y.toProd.fst f.toFun)
                                            (pointedToBipointedSnd.obj X).toProd.fst),
                                    map_snd :=
                                      (_ : Pointed.Hom.toFun f X.point = (bipointedToPointedSnd.obj Y).point) })
                                f) =
                            f) })
                X✝ Y✝).symm
          g)
      (some val✝)
[PROOFSTEP]
rfl


[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ (downFunctor ⋙ upFunctor).map f ≫ (fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) Y =
    (fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) X ≫ (𝟭 (ULift C)).map f
[PROOFSTEP]
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ (𝟭 (ULift C)).map f ≫ (fun X => 𝟙 ((𝟭 (ULift C)).obj X)) Y =
    (fun X => 𝟙 ((𝟭 (ULift C)).obj X)) X ≫ (downFunctor ⋙ upFunctor).map f
[PROOFSTEP]
change f ≫ 𝟙 _ = 𝟙 _ ≫ f
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : ULift C
f : X ⟶ Y
⊢ f ≫ 𝟙 Y = 𝟙 X ≫ f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) =
    𝟙 (downFunctor ⋙ upFunctor)
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ NatTrans.app
      ((NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) x✝ =
    NatTrans.app (𝟙 (downFunctor ⋙ upFunctor)) x✝
[PROOFSTEP]
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ 𝟙 ((downFunctor ⋙ upFunctor).obj x✝) ≫ 𝟙 ((downFunctor ⋙ upFunctor).obj x✝) = 𝟙 ((downFunctor ⋙ upFunctor).obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
⊢ ((NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) =
    𝟙 (𝟭 (ULift C))
[PROOFSTEP]
ext
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ NatTrans.app
      ((NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X)) ≫ NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X)) x✝ =
    NatTrans.app (𝟙 (𝟭 (ULift C))) x✝
[PROOFSTEP]
change 𝟙 _ ≫ 𝟙 _ = 𝟙 _
[GOAL]
case w.h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
x✝ : ULift C
⊢ 𝟙 ((𝟭 (ULift C)).obj x✝) ≫ 𝟙 ((𝟭 (ULift C)).obj x✝) = 𝟙 ((𝟭 (ULift C)).obj x✝)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ upFunctor.map (NatTrans.app (Iso.mk (𝟙 (𝟭 C)) (𝟙 (upFunctor ⋙ downFunctor))).hom X) ≫
      NatTrans.app
        (Iso.mk (NatTrans.mk fun X => 𝟙 ((downFunctor ⋙ upFunctor).obj X))
            (NatTrans.mk fun X => 𝟙 ((𝟭 (ULift C)).obj X))).hom
        (upFunctor.obj X) =
    𝟙 (upFunctor.obj X)
[PROOFSTEP]
change 𝟙 X ≫ 𝟙 X = 𝟙 X
[GOAL]
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X
[PROOFSTEP]
simp