Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    F.map f ≫
        (match Y with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom =
      (match X with
          | WalkingMulticospan.left i => left i
          | WalkingMulticospan.right i => right i).hom ≫
        G.map f

Tactic:
rintro _ _ ⟨_⟩

Goal state after:
case id
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
X✝ : WalkingMulticospan J
⊢ F.map (Hom.id X✝) ≫
      (match X✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match X✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.id X✝)

case fst
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
b✝ : J.R
⊢ F.map (Hom.fst b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match WalkingMulticospan.left (J.fst b✝) with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.fst b✝)

case snd
J : MulticospanShape
C : Type u_1
inst✝ : Category.{v_1, u_1} C
F G : WalkingMulticospan J ⥤ C
left : (i : J.L) → F.obj (WalkingMulticospan.left i) ≅ G.obj (WalkingMulticospan.left i)
right : (i : J.R) → F.obj (WalkingMulticospan.right i) ≅ G.obj (WalkingMulticospan.right i)
wl : ∀ (i : J.R), F.map (Hom.fst i) ≫ (right i).hom = (left (J.fst i)).hom ≫ G.map (Hom.fst i)
wr : ∀ (i : J.R), F.map (Hom.snd i) ≫ (right i).hom = (left (J.snd i)).hom ≫ G.map (Hom.snd i)
b✝ : J.R
⊢ F.map (Hom.snd b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom =
    (match WalkingMulticospan.left (J.snd b✝) with
        | WalkingMulticospan.left i => left i
        | WalkingMulticospan.right i => right i).hom ≫
      G.map (Hom.snd b✝)