Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left.left.left.left.id.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

pp: case left.left.left.right.id.id.fst
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.fst a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.fst a✝))

pp: case left.left.left.right.id.id.snd
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.snd a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.snd a✝))

pp: case left.left.right.right.id.fst.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.fst a✝)).comp (Hom.id (right (J.fst a✝))) =
    (Hom.id (left a✝)).comp ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝))))

pp: case left.left.right.right.id.snd.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.snd a✝)).comp (Hom.id (right (J.snd a✝))) =
    (Hom.id (left a✝)).comp ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝))))

pp: case left.right.right.right.fst.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝)))).comp (Hom.id (right (J.fst a✝))) =
    (Hom.fst a✝).comp ((Hom.id (right (J.fst a✝))).comp (Hom.id (right (J.fst a✝))))

pp: case left.right.right.right.snd.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝)))).comp (Hom.id (right (J.snd a✝))) =
    (Hom.snd a✝).comp ((Hom.id (right (J.snd a✝))).comp (Hom.id (right (J.snd a✝))))

pp: case right.right.right.right.id.id.id
J : MultispanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))

Tactic:
<;>

Goal state after:
case left.left.left.left.id.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.id (left a✝)) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.id (left a✝)))

case left.left.left.right.id.id.fst
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.fst a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.fst a✝))

case left.left.left.right.id.id.snd
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.id (left a✝))).comp (Hom.snd a✝) =
    (Hom.id (left a✝)).comp ((Hom.id (left a✝)).comp (Hom.snd a✝))

case left.left.right.right.id.fst.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.fst a✝)).comp (Hom.id (right (J.fst a✝))) =
    (Hom.id (left a✝)).comp ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝))))

case left.left.right.right.id.snd.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.id (left a✝)).comp (Hom.snd a✝)).comp (Hom.id (right (J.snd a✝))) =
    (Hom.id (left a✝)).comp ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝))))

case left.right.right.right.fst.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.fst a✝).comp (Hom.id (right (J.fst a✝)))).comp (Hom.id (right (J.fst a✝))) =
    (Hom.fst a✝).comp ((Hom.id (right (J.fst a✝))).comp (Hom.id (right (J.fst a✝))))

case left.right.right.right.snd.id.id
J : MultispanShape
a✝ : J.L
⊢ ((Hom.snd a✝).comp (Hom.id (right (J.snd a✝)))).comp (Hom.id (right (J.snd a✝))) =
    (Hom.snd a✝).comp ((Hom.id (right (J.snd a✝))).comp (Hom.id (right (J.snd a✝))))

case right.right.right.right.id.id.id
J : MultispanShape
a✝ : J.R
⊢ ((Hom.id (right a✝)).comp (Hom.id (right a✝))).comp (Hom.id (right a✝)) =
    (Hom.id (right a✝)).comp ((Hom.id (right a✝)).comp (Hom.id (right a✝)))