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

Goal state before:
pp: 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✝)

pp: 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✝)

pp: 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✝)

Tactic:
<;>

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✝)