Module: Mathlib.CategoryTheory.Category.TwoP

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      none =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      none

pp: case some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
val✝ : X'✝.X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      (some val✝)

Tactic:
<;>

Goal state after:
case none
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      none =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      none

case some
α : Type u_1
β : Type u_2
X'✝ X✝ : Pointed
Y✝ : TwoP
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ TwoP Bipointed ⋙ bipointedToPointedSnd).obj Y✝
val✝ : X'✝.X
⊢ ↑(ConcreteCategory.hom
          ({ toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                  invFun := fun f ↦
                    {
                      hom :=
                        { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                          map_snd := ⋯ } },
                  left_inv := ⋯, right_inv := ⋯ }.symm
              (f ≫ g)).hom)
      (some val✝) =
    ↑(ConcreteCategory.hom
          (pointedToTwoPSnd.map f ≫
              { toFun := fun f ↦ { toFun := f.hom.toFun ∘ some, map_point := ⋯ },
                    invFun := fun f ↦
                      {
                        hom :=
                          { toFun := fun o ↦ Option.elim o Y✝.toTwoPointing.toProd.1 f.toFun, map_fst := ⋯,
                            map_snd := ⋯ } },
                    left_inv := ⋯, right_inv := ⋯ }.symm
                g).hom)
      (some val✝)