-- Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v, v₂, u, u₂} C D
X Y Z : C
f_1 : X ⟶ Z
g : Y ⟶ Z
f : Option.some WalkingPair.right ⟶ Option.some WalkingPair.right
some :
  Eq (α :=
    (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶
      (cospan (F.map f_1) (F.map g)).obj (Option.some WalkingPair.right))
    ((cospan f_1 g ⋙ F).map (WidePullbackShape.Hom.id (Option.some WalkingPair.right)) ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map (WidePullbackShape.Hom.id (Option.some WalkingPair.right)))
⊢ Eq (α :=
    (cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right) ⟶
      (cospan (F.map f_1) (F.map g)).obj (Option.some WalkingPair.right))
    ((cospan f_1 g ⋙ F).map f ≫
      Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))))
    (Iso.hom
        (Option.casesOn (motive := fun (x : WalkingCospan) ↦
          (cospan f_1 g ⋙ F).obj x ≅ (cospan (F.map f_1) (F.map g)).obj x) (Option.some WalkingPair.right)
          (Iso.refl ((cospan f_1 g ⋙ F).obj none)) fun (val : WalkingPair) ↦
          WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦
            (cospan f_1 g ⋙ F).obj (Option.some x) ≅ (cospan (F.map f_1) (F.map g)).obj (Option.some x)) val
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.left)))
            (Iso.refl ((cospan f_1 g ⋙ F).obj (Option.some WalkingPair.right)))) ≫
      (cospan (F.map f_1) (F.map g)).map f)

Tactic:
cases f