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

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

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

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