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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ ∀ ⦃X Y : WalkingSpan⦄ (f : X ⟶ Y),
    (F.map f ≫ Option.casesOn Y z fun val ↦ WalkingPair.casesOn val l r) =
      (Option.casesOn X z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map f

Tactic:
rintro (_ | _ | _) (_ | _ | _) (_ | _)

Goal state after:
case none.none.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (F.map (WidePushoutShape.Hom.id none) ≫ Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (WidePushoutShape.Hom.id none)

case none.some.left.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (F.map (init WalkingPair.left) ≫ Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (init WalkingPair.left)

case none.some.right.init
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (F.map (init WalkingPair.right) ≫ Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r) ≫ G.map (init WalkingPair.right)

case some.left.some.left.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (F.map (WidePushoutShape.Hom.id (some WalkingPair.left)) ≫
      Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.left))

case some.right.some.right.id
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ⟶ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ⟶ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ⟶ G.obj WalkingSpan.right
hl : F.map fst ≫ l = z ≫ G.map fst
hr : F.map snd ≫ r = z ≫ G.map snd
⊢ (F.map (WidePushoutShape.Hom.id (some WalkingPair.right)) ≫
      Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r) ≫
      G.map (WidePushoutShape.Hom.id (some WalkingPair.right))