Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

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

Tactic:
rintro _ _ ⟨_⟩

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

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

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