awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ (Hom.id X).comp f = f
have leftCompReflexion : (Hom.id one).comp Hom.leftCompReflexion = Hom.leftCompReflexion
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ (Hom.id X).comp f = f
have rightCompReflexion : (Hom.id one).comp Hom.rightCompReflexion = Hom.rightCompReflexion
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ (Hom.id X).comp f = f
have id : (Hom.id X).comp (Hom.id X) = Hom.id X
Tactic: cases f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
⊢ f.comp (Hom.id Y) = f
have left : Hom.left.comp (Hom.id zero) = Hom.left
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
X Y : WalkingReflexivePair
f : X.Hom Y
left : Hom.left.comp (Hom.id zero) = Hom.left
⊢ f.comp (Hom.id Y) = f
have right : Hom.right.comp (Hom.id zero) = Hom.right
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ f.comp (Hom.id Y) = f
have reflexion : Hom.reflexion.comp (Hom.id one) = Hom.reflexion
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ f.comp (Hom.id Y) = f
have leftCompReflexion : Hom.leftCompReflexion.comp (Hom.id one) = Hom.leftCompReflexion
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ f.comp (Hom.id Y) = f
have rightCompReflexion : Hom.rightCompReflexion.comp (Hom.id one) = Hom.rightCompReflexion
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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
⊢ f.comp (Hom.id Y) = f
have id : (Hom.id X).comp (Hom.id X) = Hom.id X
Tactic: cases f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W 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)
have left : ∀ (g : zero.Hom Y), (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have right : ∀ (g : zero.Hom Y), (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have reflexion : ∀ (g : one.Hom Y), (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have leftCompReflexion : ∀ (g : one.Hom Y), (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have rightCompReflexion : ∀ (g : one.Hom Y), (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: W, X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have id : ∀ (g : W.Hom Y), ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
Tactic: cases f
Cleared hypotheses: X, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : zero.Hom Y
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)
have left : ∀ (h : one.Hom Z), (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.left.comp g).comp h = Hom.left.comp (g.comp h)
have left₁ : ∀ (h : zero.Hom Z), (Hom.left.comp (Hom.id zero)).comp h = Hom.left.comp ((Hom.id zero).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : zero.Hom Y
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)
have right : ∀ (h : one.Hom Z), (Hom.right.comp Hom.reflexion).comp h = Hom.right.comp (Hom.reflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.right.comp g).comp h = Hom.right.comp (g.comp h)
have right₁ : ∀ (h : zero.Hom Z), (Hom.right.comp (Hom.id zero)).comp h = Hom.right.comp ((Hom.id zero).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
have reflexion : ∀ (h : zero.Hom Z), (Hom.reflexion.comp Hom.left).comp h = Hom.reflexion.comp (Hom.left.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
have reflexion₁ : ∀ (h : zero.Hom Z), (Hom.reflexion.comp Hom.right).comp h = Hom.reflexion.comp (Hom.right.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
have reflexion₂ : ∀ (h : one.Hom Z), (Hom.reflexion.comp Hom.leftCompReflexion).comp h = Hom.reflexion.comp (Hom.leftCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
have reflexion₃ : ∀ (h : one.Hom Z),
  (Hom.reflexion.comp Hom.rightCompReflexion).comp h = Hom.reflexion.comp (Hom.rightCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.reflexion.comp g).comp h = Hom.reflexion.comp (g.comp h)
have reflexion₄ : ∀ (h : one.Hom Z), (Hom.reflexion.comp (Hom.id one)).comp h = Hom.reflexion.comp ((Hom.id one).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
have leftCompReflexion : ∀ (h : zero.Hom Z), (Hom.leftCompReflexion.comp Hom.left).comp h = Hom.leftCompReflexion.comp (Hom.left.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
have leftCompReflexion₁ : ∀ (h : zero.Hom Z), (Hom.leftCompReflexion.comp Hom.right).comp h = Hom.leftCompReflexion.comp (Hom.right.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
have leftCompReflexion₂ : ∀ (h : one.Hom Z),
  (Hom.leftCompReflexion.comp Hom.leftCompReflexion).comp h = Hom.leftCompReflexion.comp (Hom.leftCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
have leftCompReflexion₃ : ∀ (h : one.Hom Z),
  (Hom.leftCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.leftCompReflexion.comp (Hom.rightCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.leftCompReflexion.comp g).comp h = Hom.leftCompReflexion.comp (g.comp h)
have leftCompReflexion₄ : ∀ (h : one.Hom Z), (Hom.leftCompReflexion.comp (Hom.id one)).comp h = Hom.leftCompReflexion.comp ((Hom.id one).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Y Z : WalkingReflexivePair
h : Y.Hom Z
g : one.Hom Y
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
have rightCompReflexion : ∀ (h : zero.Hom Z), (Hom.rightCompReflexion.comp Hom.left).comp h = Hom.rightCompReflexion.comp (Hom.left.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
have rightCompReflexion₁ : ∀ (h : zero.Hom Z), (Hom.rightCompReflexion.comp Hom.right).comp h = Hom.rightCompReflexion.comp (Hom.right.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
have rightCompReflexion₂ : ∀ (h : one.Hom Z),
  (Hom.rightCompReflexion.comp Hom.leftCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.leftCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
have rightCompReflexion₃ : ∀ (h : one.Hom Z),
  (Hom.rightCompReflexion.comp Hom.rightCompReflexion).comp h =
    Hom.rightCompReflexion.comp (Hom.rightCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.rightCompReflexion.comp g).comp h = Hom.rightCompReflexion.comp (g.comp h)
have rightCompReflexion₄ : ∀ (h : one.Hom Z), (Hom.rightCompReflexion.comp (Hom.id one)).comp h = Hom.rightCompReflexion.comp ((Hom.id one).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
W Y Z : WalkingReflexivePair
h : Y.Hom Z
g : W.Hom Y
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id : ∀ (h : zero.Hom Z), ((Hom.id one).comp Hom.left).comp h = (Hom.id one).comp (Hom.left.comp h)
Tactic: cases g
Cleared hypotheses: W, Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id₁ : ∀ (h : zero.Hom Z), ((Hom.id one).comp Hom.right).comp h = (Hom.id one).comp (Hom.right.comp h)
Tactic: cases g
Cleared hypotheses: W, Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id₂ : ∀ (h : one.Hom Z), ((Hom.id zero).comp Hom.reflexion).comp h = (Hom.id zero).comp (Hom.reflexion.comp h)
Tactic: cases g
Cleared hypotheses: W, Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id₃ : ∀ (h : one.Hom Z), ((Hom.id one).comp Hom.leftCompReflexion).comp h = (Hom.id one).comp (Hom.leftCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: W, Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id₄ : ∀ (h : one.Hom Z), ((Hom.id one).comp Hom.rightCompReflexion).comp h = (Hom.id one).comp (Hom.rightCompReflexion.comp h)
Tactic: cases g
Cleared hypotheses: W, Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ ((Hom.id W).comp g).comp h = (Hom.id W).comp (g.comp h)
have id₅ : ∀ (h : W.Hom Z), ((Hom.id W).comp (Hom.id W)).comp h = (Hom.id W).comp ((Hom.id W).comp h)
Tactic: cases g
Cleared hypotheses: Y, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)
have left : (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
Goal:
Z : WalkingReflexivePair
h : one.Hom Z
left : (Hom.left.comp Hom.reflexion).comp Hom.left = Hom.left.comp (Hom.reflexion.comp Hom.left)
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)
have left₁ : (Hom.left.comp Hom.reflexion).comp Hom.right = Hom.left.comp (Hom.reflexion.comp Hom.right)
Tactic: cases h
Cleared hypotheses: Z, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Reflexive (goal)
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)
⊢ (Hom.left.comp Hom.reflexion).comp h = Hom.left.comp (Hom.reflexion.comp h)
have left₂ : (Hom.left.comp Hom.reflexion).comp Hom.leftCompReflexion = Hom.left.comp (Hom.reflexion.comp Hom.leftCompReflexion)
Tactic: cases h
Cleared hypotheses: Z, h