Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case none.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case none.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.left.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.left.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.left.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.right.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.right.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

pp: case some.right.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

Tactic:
<;>

Goal state after:
case none.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case none.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case none.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : none ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.left.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.left.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.left.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.right.none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ none
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn none (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.right.some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f

case some.right.some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
X Y Z : C
f✝ : X ⟶ Y
g : X ⟶ Z
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ (span f✝ g ⋙ F).map f ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((span f✝ g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((span f✝ g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (span (F.map f✝) (F.map g)).map f