awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X : WalkingReflexivePair
_ : ∀ {Y : WalkingReflexivePair} (f : X.Hom Y), (Hom.id X).comp f = f
⊢ ∀ {Y : WalkingReflexivePair} (f : X.Hom Y), (Hom.id X).comp f = f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
left : (Hom.id one).comp Hom.left = Hom.left
right : (Hom.id one).comp Hom.right = Hom.right
reflexion : (Hom.id zero).comp Hom.reflexion = Hom.reflexion
leftCompReflexion : (Hom.id one).comp Hom.leftCompReflexion = Hom.leftCompReflexion
rightCompReflexion : (Hom.id one).comp Hom.rightCompReflexion = Hom.rightCompReflexion
id : (Hom.id X).comp (Hom.id X) = Hom.id X
⊢ (Hom.id X).comp f = f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ (Hom.id one).comp Hom.left = Hom.left

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ (Hom.id one).comp Hom.right = Hom.right

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ (Hom.id zero).comp Hom.reflexion = Hom.reflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ (Hom.id one).comp Hom.leftCompReflexion = Hom.leftCompReflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ (Hom.id one).comp Hom.rightCompReflexion = Hom.rightCompReflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X : WalkingReflexivePair
⊢ (Hom.id X).comp (Hom.id X) = Hom.id X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X : WalkingReflexivePair
_ : ∀ {Y : WalkingReflexivePair} (f : X.Hom Y), f.comp (Hom.id Y) = f
⊢ ∀ {Y : WalkingReflexivePair} (f : X.Hom Y), f.comp (Hom.id Y) = f

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
left : Hom.left.comp (Hom.id zero) = Hom.left
right : Hom.right.comp (Hom.id zero) = Hom.right
reflexion : Hom.reflexion.comp (Hom.id one) = Hom.reflexion
leftCompReflexion : Hom.leftCompReflexion.comp (Hom.id one) = Hom.leftCompReflexion
rightCompReflexion : Hom.rightCompReflexion.comp (Hom.id one) = Hom.rightCompReflexion
id : (Hom.id X).comp (Hom.id X) = Hom.id X
⊢ f.comp (Hom.id Y) = f

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ Hom.left.comp (Hom.id zero) = Hom.left

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ Hom.right.comp (Hom.id zero) = Hom.right

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ Hom.reflexion.comp (Hom.id one) = Hom.reflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ Hom.leftCompReflexion.comp (Hom.id one) = Hom.leftCompReflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
⊢ Hom.rightCompReflexion.comp (Hom.id one) = Hom.rightCompReflexion

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
W : WalkingReflexivePair
_ : ∀ {X Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)
⊢ ∀ {X Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
W X : WalkingReflexivePair
_ : ∀ {Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)
⊢ ∀ {Y Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
W X Y : WalkingReflexivePair
_ : ∀ {Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)
⊢ ∀ {Z : WalkingReflexivePair} (f : W.Hom X) (g : X.Hom Y) (h : Y.Hom Z), (f.comp g).comp h = f.comp (g.comp h)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
W X Y Z : WalkingReflexivePair
f : W.Hom X
g : X.Hom Y
h : Y.Hom Z
left : ∀ (g : zero.Hom Y), (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)
right : ∀ (g : zero.Hom Y), (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)
reflexion : ∀ (g : one.Hom Y), (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
leftCompReflexion : ∀ (g : one.Hom Y), (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
rightCompReflexion : ∀ (g : one.Hom Y), (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
id : ∀ (g : W.Hom Y), ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : zero.Hom Y
left : ∀ (h : one.Hom Z), (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)
left₁ : ∀ (h : zero.Hom Z), (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : zero.Hom Y
right : ∀ (h : one.Hom Z), (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)
right₁ : ∀ (h : zero.Hom Z), (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
reflexion : ∀ (h : zero.Hom Z), (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)
reflexion₁ : ∀ (h : zero.Hom Z), (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)
reflexion₂ :
  ∀ (h : one.Hom Z),
    (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)
reflexion₃ :
  ∀ (h : one.Hom Z),
    (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)
reflexion₄ : ∀ (h : one.Hom Z), (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
leftCompReflexion :
  ∀ (h : zero.Hom Z), (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)
leftCompReflexion₁ :
  ∀ (h : zero.Hom Z), (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)
leftCompReflexion₂ :
  ∀ (h : one.Hom Z),
    (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h =
      Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)
leftCompReflexion₃ :
  ∀ (h : one.Hom Z),
    (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
      Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)
leftCompReflexion₄ :
  ∀ (h : one.Hom Z), (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
rightCompReflexion :
  ∀ (h : zero.Hom Z), (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)
rightCompReflexion₁ :
  ∀ (h : zero.Hom Z), (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)
rightCompReflexion₂ :
  ∀ (h : one.Hom Z),
    (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
      Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)
rightCompReflexion₃ :
  ∀ (h : one.Hom Z),
    (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
      Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)
rightCompReflexion₄ :
  ∀ (h : one.Hom Z),
    (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
W Y Z : WalkingReflexivePair
h : Y.Hom Z
g : W.Hom Y
id : ∀ (h : zero.Hom Z), ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)
id₁ : ∀ (h : zero.Hom Z), ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)
id₂ : ∀ (h : one.Hom Z), ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)
id₃ :
  ∀ (h : one.Hom Z), ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
id₄ :
  ∀ (h : one.Hom Z),
    ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
id₅ : ∀ (h : W.Hom Z), ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
left : (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)
left₁ : (Hom.left.comp Hom.reflexion).comp Hom.right = Hom.left.comp (Hom.reflexion.comp Hom.right)
left₂ :
  (Hom.left.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.leftCompReflexion)
left₃ :
  (Hom.left.comp Hom.reflexion).comp Hom.rightCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.rightCompReflexion)
left₄ : (Hom.left.comp Hom.reflexion).comp (Hom.id one) = Hom.left.comp (Hom.reflexion.comp (Hom.id one))
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
left : (Hom.left.comp (Hom.id zero)).comp Hom.reflexion = Hom.left.comp ((Hom.id zero).comp Hom.reflexion)
left₁ : (Hom.left.comp (Hom.id zero)).comp (Hom.id zero) = Hom.left.comp ((Hom.id zero).comp (Hom.id zero))
⊢ (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
right : (Hom.right.comp Hom.reflexion).comp Hom.left = Hom.right.comp (Hom.reflexion.comp Hom.left)
right₁ : (Hom.right.comp Hom.reflexion).comp Hom.right = Hom.right.comp (Hom.reflexion.comp Hom.right)
right₂ :
  (Hom.right.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.right.comp (Hom.reflexion.comp Hom.leftCompReflexion)
right₃ :
  (Hom.right.comp Hom.reflexion).comp Hom.rightCompReflexion =
    Hom.right.comp (Hom.reflexion.comp Hom.rightCompReflexion)
right₄ : (Hom.right.comp Hom.reflexion).comp (Hom.id one) = Hom.right.comp (Hom.reflexion.comp (Hom.id one))
⊢ (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
right : (Hom.right.comp (Hom.id zero)).comp Hom.reflexion = Hom.right.comp ((Hom.id zero).comp Hom.reflexion)
right₁ : (Hom.right.comp (Hom.id zero)).comp (Hom.id zero) = Hom.right.comp ((Hom.id zero).comp (Hom.id zero))
⊢ (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
reflexion : (Hom.reflexion.comp Hom.left).comp Hom.reflexion = Hom.reflexion.comp (Hom.left.comp Hom.reflexion)
reflexion₁ : (Hom.reflexion.comp Hom.left).comp (Hom.id zero) = Hom.reflexion.comp (Hom.left.comp (Hom.id zero))
⊢ (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
reflexion : (Hom.reflexion.comp Hom.right).comp Hom.reflexion = Hom.reflexion.comp (Hom.right.comp Hom.reflexion)
reflexion₁ : (Hom.reflexion.comp Hom.right).comp (Hom.id zero) = Hom.reflexion.comp (Hom.right.comp (Hom.id zero))
⊢ (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
reflexion :
  (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.left)
reflexion₁ :
  (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.right = Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.right)
reflexion₂ :
  (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
reflexion₃ :
  (Hom.reflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)
reflexion₄ :
  (Hom.reflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
⊢ (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
reflexion :
  (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.left = Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.left)
reflexion₁ :
  (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.right)
reflexion₂ :
  (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
reflexion₃ :
  (Hom.reflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)
reflexion₄ :
  (Hom.reflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.reflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
⊢ (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
reflexion : (Hom.reflexion.comp (Hom.id one)).comp Hom.left = Hom.reflexion.comp ((Hom.id one).comp Hom.left)
reflexion₁ : (Hom.reflexion.comp (Hom.id one)).comp Hom.right = Hom.reflexion.comp ((Hom.id one).comp Hom.right)
reflexion₂ :
  (Hom.reflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)
reflexion₃ :
  (Hom.reflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.reflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)
reflexion₄ : (Hom.reflexion.comp (Hom.id one)).comp (Hom.id one) = Hom.reflexion.comp ((Hom.id one).comp (Hom.id one))
⊢ (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
leftCompReflexion :
  (Hom.leftCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.left.comp Hom.reflexion)
leftCompReflexion₁ :
  (Hom.leftCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.left.comp (Hom.id zero))
⊢ (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
leftCompReflexion :
  (Hom.leftCompReflexion.comp Hom.right).comp Hom.reflexion = Hom.leftCompReflexion.comp (Hom.right.comp Hom.reflexion)
leftCompReflexion₁ :
  (Hom.leftCompReflexion.comp Hom.right).comp (Hom.id zero) = Hom.leftCompReflexion.comp (Hom.right.comp (Hom.id zero))
⊢ (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
leftCompReflexion :
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)
leftCompReflexion₁ :
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)
leftCompReflexion₂ :
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
leftCompReflexion₃ :
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)
leftCompReflexion₄ :
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
⊢ (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
leftCompReflexion :
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)
leftCompReflexion₁ :
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)
leftCompReflexion₂ :
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
leftCompReflexion₃ :
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)
leftCompReflexion₄ :
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
⊢ (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
leftCompReflexion :
  (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.left)
leftCompReflexion₁ :
  (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.right)
leftCompReflexion₂ :
  (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)
leftCompReflexion₃ :
  (Hom.leftCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.leftCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)
leftCompReflexion₄ :
  (Hom.leftCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.leftCompReflexion.comp ((Hom.id one).comp (Hom.id one))
⊢ (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
rightCompReflexion :
  (Hom.rightCompReflexion.comp Hom.left).comp Hom.reflexion = Hom.rightCompReflexion.comp (Hom.left.comp Hom.reflexion)
rightCompReflexion₁ :
  (Hom.rightCompReflexion.comp Hom.left).comp (Hom.id zero) = Hom.rightCompReflexion.comp (Hom.left.comp (Hom.id zero))
⊢ (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
rightCompReflexion :
  (Hom.rightCompReflexion.comp Hom.right).comp Hom.reflexion =
    Hom.rightCompReflexion.comp (Hom.right.comp Hom.reflexion)
rightCompReflexion₁ :
  (Hom.rightCompReflexion.comp Hom.right).comp (Hom.id zero) =
    Hom.rightCompReflexion.comp (Hom.right.comp (Hom.id zero))
⊢ (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
rightCompReflexion :
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.left)
rightCompReflexion₁ :
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.right)
rightCompReflexion₂ :
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.leftCompReflexion)
rightCompReflexion₃ :
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp Hom.rightCompReflexion)
rightCompReflexion₄ :
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp (Hom.id one))
⊢ (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
rightCompReflexion :
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.left =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.left)
rightCompReflexion₁ :
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.right =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.right)
rightCompReflexion₂ :
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.leftCompReflexion)
rightCompReflexion₃ :
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp Hom.rightCompReflexion)
rightCompReflexion₄ :
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp (Hom.id one) =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp (Hom.id one))
⊢ (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
rightCompReflexion :
  (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.left = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.left)
rightCompReflexion₁ :
  (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.right = Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.right)
rightCompReflexion₂ :
  (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.leftCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.leftCompReflexion)
rightCompReflexion₃ :
  (Hom.rightCompReflexion.comp (Hom.id one)).comp Hom.rightCompReflexion =
    Hom.rightCompReflexion.comp ((Hom.id one).comp Hom.rightCompReflexion)
rightCompReflexion₄ :
  (Hom.rightCompReflexion.comp (Hom.id one)).comp (Hom.id one) =
    Hom.rightCompReflexion.comp ((Hom.id one).comp (Hom.id one))
⊢ (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
id : ((Hom.id one).comp Hom.left).comp Hom.reflexion = (Hom.id one).comp (Hom.left.comp Hom.reflexion)
id₁ : ((Hom.id one).comp Hom.left).comp (Hom.id zero) = (Hom.id one).comp (Hom.left.comp (Hom.id zero))
⊢ ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive
Goal:
Z : WalkingReflexivePair
h : zero.Hom Z
id : ((Hom.id one).comp Hom.right).comp Hom.reflexion = (Hom.id one).comp (Hom.right.comp Hom.reflexion)
id₁ : ((Hom.id one).comp Hom.right).comp (Hom.id zero) = (Hom.id one).comp (Hom.right.comp (Hom.id zero))
⊢ ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)

Tactic:
cases h