Module: Mathlib.CategoryTheory.Monoidal.Cartesian.FunctorCategory

Goal state before:
pp: case left
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.left } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.left }

pp: case right
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.right } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.right }

Tactic:
;

Goal state after:
case left
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.left } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.left }

case right
J : Type u_1
C : Type u_2
D : Type u_3
E : Type u_4
inst✝⁵ : Category.{v_1, u_1} J
inst✝⁴ : Category.{v_2, u_2} C
inst✝³ : Category.{v_3, u_3} D
inst✝² : Category.{v_4, u_4} E
inst✝¹ : CartesianMonoidalCategory C
inst✝ : CartesianMonoidalCategory E
X Y : J ⥤ C
j : J
⊢ (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).π.app { as := WalkingPair.right } =
    (Iso.refl (BinaryFan.mk (fst (X.obj j) (Y.obj j)) (snd (X.obj j) (Y.obj j))).pt).hom ≫
      ((Cone.postcompose
                  (mapPairIso (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.left }))
                      (Iso.refl ((pair X Y ⋙ (evaluation J C).obj j).obj { as := WalkingPair.right }))).hom).obj
              (((evaluation J C).obj j).mapCone
                (BinaryFan.mk { app := fun x ↦ fst (X.obj x) (Y.obj x), naturality := ⋯ }
                  { app := fun x ↦ snd (X.obj x) (Y.obj x), naturality := ⋯ }))).π.app
        { as := WalkingPair.right }