Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: case left.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)

pp: case left.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)

pp: case right.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)

pp: case right.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)

pp: case reflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)

pp: case reflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)

pp: case reflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)

pp: case reflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)

pp: case reflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)

pp: case leftCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)

pp: case leftCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)

pp: case leftCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)

pp: case leftCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)

pp: case leftCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)

pp: case rightCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)

pp: case rightCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)

pp: case rightCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)

pp: case rightCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)

pp: case rightCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)

pp: case id.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)

pp: case id.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)

pp: case id.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)

pp: case id.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)

pp: case id.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)

pp: case id.id
W✝ Z✝ : WalkingReflexivePair
h : W✝.Hom Z✝
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp h = (Hom.id W✝).comp ((Hom.id W✝).comp h)

Tactic:
<;>

Goal state after:
case left.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)

case left.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)

case right.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)

case right.id
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)

case reflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)

case reflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)

case reflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)

case reflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)

case reflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)

case leftCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)

case leftCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)

case leftCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)

case leftCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)

case leftCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)

case rightCompReflexion.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)

case rightCompReflexion.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)

case rightCompReflexion.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)

case rightCompReflexion.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)

case rightCompReflexion.id
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)

case id.left
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)

case id.right
Z✝ : WalkingReflexivePair
h : zero.Hom Z✝
⊢ ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)

case id.reflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)

case id.leftCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)

case id.rightCompReflexion
Z✝ : WalkingReflexivePair
h : one.Hom Z✝
⊢ ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)

case id.id
W✝ Z✝ : WalkingReflexivePair
h : W✝.Hom Z✝
⊢ ((Hom.id W✝).comp (Hom.id W✝)).comp h = (Hom.id W✝).comp ((Hom.id W✝).comp h)