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