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

Goal state before:
pp: case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

pp: case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

Tactic:
<;>

Goal state after:
case none.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case none.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case none.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : none ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.left.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.left ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.none
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ none
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.some.left
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.left
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f

case some.right.some.right
C : Type u
inst✝ : Category.{v, u} C
F : WalkingSpan ⥤ C
f : some WalkingPair.right ⟶ some WalkingPair.right
⊢ F.map f ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (span (F.map fst) (F.map snd)).map f