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 : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    (d.map F).multicospan.map f ≫
        (match Y with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
      (match X with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
        (d.multicospan ⋙ F).map f

Tactic:
rintro a b (_ | _)

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 : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
a : WalkingMulticospan J
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.id a) ≫
      (match a with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match a with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.id a)

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 : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
b✝ : J.R
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.fst b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (J.fst b✝) with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.fst b✝)

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 : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
b✝ : J.R
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.snd b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (J.snd b✝) with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.snd b✝)