Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMultispan J} (f : X ⟶ Y),
    (d.map F).multispan.map f ≫
        (match Y with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
      (match X with
          | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
          | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
        (d.multispan ⋙ F).map f

Tactic:
rintro _ _ (_ | _)

Goal state after:
case id
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
X✝ : WalkingMultispan J
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.id X✝) ≫
      (match X✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match X✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.id X✝)

case fst
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
a✝ : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.fst a✝) ≫
      (match WalkingMultispan.right (J.fst a✝) with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.fst a✝)

case snd
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
a✝ : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.snd a✝) ≫
      (match WalkingMultispan.right (J.snd a✝) with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.snd a✝)