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

Goal state before:
pp: case none.none.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id none)

pp: case some.left.none.term
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.left) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.left)

pp: case some.left.some.left.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

pp: case some.right.none.term
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.right) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.right)

pp: case some.right.some.right.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.right))

Tactic:
<;>

Goal state after:
case none.none.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id none) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id none)

case some.left.none.term
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.left) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.left)

case some.left.some.left.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.left) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.left))

case some.right.none.term
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (term WalkingPair.right) ≫
      (Option.casesOn none (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (term WalkingPair.right)

case some.right.some.right.id
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 ⟶ Z
g : Y ⟶ Z
⊢ (cospan f g ⋙ F).map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom =
    (Option.casesOn (some WalkingPair.right) (Iso.refl ((cospan f g ⋙ F).obj none)) fun val ↦
          WalkingPair.casesOn val (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.left)))
            (Iso.refl ((cospan f g ⋙ F).obj (some WalkingPair.right)))).hom ≫
      (cospan (F.map f) (F.map g)).map (WidePullbackShape.Hom.id (some WalkingPair.right))