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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ 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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (term WalkingPair.left) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫ 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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (term WalkingPair.right) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id none) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom ≫ 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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (term WalkingPair.left) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫ 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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.left)) ≫
      (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.left) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (term WalkingPair.right) ≫ (Option.casesOn none z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      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
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingCospan ⥤ C
z : F.obj WalkingCospan.one ≅ G.obj WalkingCospan.one
l : F.obj WalkingCospan.left ≅ G.obj WalkingCospan.left
r : F.obj WalkingCospan.right ≅ G.obj WalkingCospan.right
hl : F.map inl ≫ z.hom = l.hom ≫ G.map inl
hr : F.map inr ≫ z.hom = r.hom ≫ G.map inr
⊢ F.map (WidePullbackShape.Hom.id (some WalkingPair.right)) ≫
      (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom =
    (Option.casesOn (some WalkingPair.right) z fun val ↦ WalkingPair.casesOn val l r).hom ≫
      G.map (WidePullbackShape.Hom.id (some WalkingPair.right))