awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsLimit s
⊢ IsLimit.{0, v, 0, u} (J := WalkingCospan) (C := C) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
    (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
      hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip)
have h_2 : (i j : WalkingPair) → i ≠ j → WalkingPair.right ≠ WalkingPair.left → IsLimit s.flip
Tactic: split
Cleared hypotheses: i, j, hij
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      ((fun {i j : WalkingPair} (hij : i ≠ j) ↦
          (match (motive := (i j : WalkingPair) → (hij : i ≠ j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
              hij with
            | WalkingPair.left, WalkingPair.right, hij => s
            | WalkingPair.right, WalkingPair.left, hij => s.flip :
            PullbackCone (Cofan.inj c i) (Cofan.inj c j)))
        hij))
have refine_3 : IsInitial.{v, u} (C := C)
  (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
    (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
      hij with
    | WalkingPair.left, WalkingPair.right, hij => s
    | WalkingPair.right, WalkingPair.left, hij => s.flip))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
⊢ IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
        hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip))
have h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsInitial.{v, u} s.pt
Tactic: split
Cleared hypotheses: i, j, hij
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
X Y : C
c : BinaryCofan.{v, u} X Y
hc : IsColimit c
inst_1 : Mono c.inl
inst_2 : Mono c.inr
s : PullbackCone c.inl c.inr
hs : IsLimit s
H : IsInitial.{v, u} s.pt
this : ∀ (i : WalkingPair), Mono (Cofan.inj c i)
i j : WalkingPair
hij : i ≠ j
h_1 : (i j : WalkingPair) → i ≠ j → WalkingPair.left ≠ WalkingPair.right → IsInitial.{v, u} s.pt
⊢ IsInitial.{v, u} (C := C)
    (Cone.pt.{0, v, 0, u} (J := WalkingCospan) (F := cospan (Cofan.inj c i) (Cofan.inj c j))
      (match (motive := (i j : WalkingPair) → (hij : ¬i = j) → PullbackCone (Cofan.inj c i) (Cofan.inj c j)) i, j,
        hij with
      | WalkingPair.left, WalkingPair.right, hij => s
      | WalkingPair.right, WalkingPair.left, hij => s.flip))
have h_2 : (i j : WalkingPair) → i ≠ j → WalkingPair.right ≠ WalkingPair.left → IsInitial.{v, u} s.flip.pt
Tactic: split
Cleared hypotheses: i, j, hij
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
⊢ CoproductDisjoint.{v, u, 0} X
have h : ∀ (x : WalkingPair),
  X x = WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x (X WalkingPair.left) (X WalkingPair.right)
Tactic: convert! H (X .left) (X .right) using 2
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
x : WalkingPair
⊢ X x = WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x (X WalkingPair.left) (X WalkingPair.right)
have h : X WalkingPair.left =
  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left (X WalkingPair.left) (X WalkingPair.right)
Tactic: casesm WalkingPair
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
x : WalkingPair
h :
  X WalkingPair.left =
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.left (X WalkingPair.left)
      (X WalkingPair.right)
⊢ X x = WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) x (X WalkingPair.left) (X WalkingPair.right)
have h₁ : X WalkingPair.right =
  WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right (X WalkingPair.left) (X WalkingPair.right)
Tactic: casesm WalkingPair
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.End (hypothesis)
Goal:
J : Type u
inst : Category.{v, u} J
C : Type u'
inst_1 : Category.{v', u'} C
F : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_2 : HasEnd F
X : C
f_1 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_1 i ≫ (F.obj (op i)).map g = f_1 j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
⊢ Eq (α := end_ F ⟶ (F'.obj (op j)).obj j')
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : end_ F ⟶ (F'.obj (op x)).obj x)) j ≫ (F'.obj (op j)).map φ)
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : end_ F ⟶ (F'.obj (op x)).obj x)) j' ≫ (F'.map φ.op).app j')
have e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (F'.obj (op j)).map φ
Tactic: have e := (f.app (op j)).naturality φ
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.End (goal)
Goal:
J : Type u
inst : Category.{v, u} J
C : Type u'
inst_1 : Category.{v', u'} C
F : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_2 : HasEnd F
X : C
f_1 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_1 i ≫ (F.obj (op i)).map g = f_1 j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (F'.obj (op j)).map φ
⊢ Eq (α := end_ F ⟶ (F'.obj (op j)).obj j')
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : end_ F ⟶ (F'.obj (op x)).obj x)) j ≫ (F'.obj (op j)).map φ)
    ((fun (x : J) ↦ (π F x ≫ NatTrans.app (f.app (op x)) x : end_ F ⟶ (F'.obj (op x)).obj x)) j' ≫ (F'.map φ.op).app j')
have simp : Eq (α := end_ F ⟶ (F'.obj (op j)).obj j') (π F j ≫ NatTrans.app (f.app (op j)) j ≫ (F'.obj (op j)).map φ)
  (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (F'.map φ.op).app j')
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.End (goal)
Goal:
J : Type u
inst : Category.{v, u} J
C : Type u'
inst_1 : Category.{v', u'} C
F : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_2 : HasEnd F
X : C
f_1 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f_1 i ≫ (F.obj (op i)).map g = f_1 j ≫ (F.map g.op).app j
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasEnd F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
e : (F.obj (op j)).map φ ≫ NatTrans.app (f.app (op j)) j' = NatTrans.app (f.app (op j)) j ≫ (F'.obj (op j)).map φ
⊢ Eq (α := end_ F ⟶ (F'.obj (op j)).obj j') (π F j ≫ NatTrans.app (f.app (op j)) j ≫ (F'.obj (op j)).map φ)
    (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (F'.map φ.op).app j')
have rw : Eq (α := end_ F ⟶ (F'.obj (op j)).obj j') (π F j' ≫ (F.map φ.op).app j' ≫ NatTrans.app (f.app (op j)) j')
  (π F j' ≫ NatTrans.app (f.app (op j')) j' ≫ (F'.map φ.op).app j')
Tactic: rw [← e, reassoc_of% end_.condition F φ]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
⊢ f.comp (id Y) = f
have left : left.comp (id one) = left
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
left : WalkingParallelPairHom.left.comp (id one) = WalkingParallelPairHom.left
⊢ f.comp (id Y) = f
have right : right.comp (id one) = right
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
left : WalkingParallelPairHom.left.comp (id one) = WalkingParallelPairHom.left
right : WalkingParallelPairHom.right.comp (id one) = WalkingParallelPairHom.right
⊢ f.comp (id Y) = f
have id : (id X).comp (id X) = id X
Tactic: cases f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
⊢ (f.comp g).comp h = f.comp (g.comp h)
have left : ∀ (g : WalkingParallelPairHom one Z), (left.comp g).comp h = left.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
left :
  ∀ (g : WalkingParallelPairHom one Z),
    (WalkingParallelPairHom.left.comp g).comp h = WalkingParallelPairHom.left.comp (g.comp h)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have right : ∀ (g : WalkingParallelPairHom one Z), (right.comp g).comp h = right.comp (g.comp h)
Tactic: cases f
Cleared hypotheses: X, Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y Z W : WalkingParallelPair
f : WalkingParallelPairHom X Y
g : WalkingParallelPairHom Y Z
h : WalkingParallelPairHom Z W
left :
  ∀ (g : WalkingParallelPairHom one Z),
    (WalkingParallelPairHom.left.comp g).comp h = WalkingParallelPairHom.left.comp (g.comp h)
right :
  ∀ (g : WalkingParallelPairHom one Z),
    (WalkingParallelPairHom.right.comp g).comp h = WalkingParallelPairHom.right.comp (g.comp h)
⊢ (f.comp g).comp h = f.comp (g.comp h)
have id : ∀ (g : WalkingParallelPairHom X Z), ((id X).comp g).comp h = (id X).comp (g.comp h)
Tactic: cases f
Cleared hypotheses: Y, f, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (left.comp g).comp h = left.comp (g.comp h)
have left : ∀ (h : WalkingParallelPairHom one W), (left.comp (id one)).comp h = left.comp ((id one).comp h)
Tactic: cases g
Cleared hypotheses: Z, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
⊢ (right.comp g).comp h = right.comp (g.comp h)
have right : ∀ (h : WalkingParallelPairHom one W), (right.comp (id one)).comp h = right.comp ((id one).comp h)
Tactic: cases g
Cleared hypotheses: Z, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
⊢ ((id X).comp g).comp h = (id X).comp (g.comp h)
have id : ∀ (h : WalkingParallelPairHom one W), ((id zero).comp left).comp h = (id zero).comp (left.comp h)
Tactic: cases g
Cleared hypotheses: X, Z, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
id :
  ∀ (h : WalkingParallelPairHom one W),
    ((WalkingParallelPairHom.id zero).comp left).comp h = (WalkingParallelPairHom.id zero).comp (left.comp h)
⊢ ((WalkingParallelPairHom.id X).comp g).comp h = (WalkingParallelPairHom.id X).comp (g.comp h)
have id₁ : ∀ (h : WalkingParallelPairHom one W),
  ((WalkingParallelPairHom.id zero).comp right).comp h = (WalkingParallelPairHom.id zero).comp (right.comp h)
Tactic: cases g
Cleared hypotheses: X, Z, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom X Z
id :
  ∀ (h : WalkingParallelPairHom one W),
    ((WalkingParallelPairHom.id zero).comp left).comp h = (WalkingParallelPairHom.id zero).comp (left.comp h)
id₁ :
  ∀ (h : WalkingParallelPairHom one W),
    ((WalkingParallelPairHom.id zero).comp right).comp h = (WalkingParallelPairHom.id zero).comp (right.comp h)
⊢ ((WalkingParallelPairHom.id X).comp g).comp h = (WalkingParallelPairHom.id X).comp (g.comp h)
have id₂ : ∀ (h : WalkingParallelPairHom X W),
  ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp h =
    (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp h)
Tactic: cases g
Cleared hypotheses: Z, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (left.comp (id one)).comp h = left.comp ((id one).comp h)
have left : (left.comp (id one)).comp (id one) = left.comp ((id one).comp (id one))
Tactic: cases h
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ (right.comp (id one)).comp h = right.comp ((id one).comp h)
have right : (right.comp (id one)).comp (id one) = right.comp ((id one).comp (id one))
Tactic: cases h
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp left).comp h = (id zero).comp (left.comp h)
have id : ((id zero).comp left).comp (id one) = (id zero).comp (left.comp (id one))
Tactic: cases h
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
⊢ ((id zero).comp right).comp h = (id zero).comp (right.comp h)
have id : ((id zero).comp right).comp (id one) = (id zero).comp (right.comp (id one))
Tactic: cases h
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X W : WalkingParallelPair
h : WalkingParallelPairHom X W
⊢ ((id X).comp (id X)).comp h = (id X).comp ((id X).comp h)
have id : ((id zero).comp (id zero)).comp left = (id zero).comp ((id zero).comp left)
Tactic: cases h
Cleared hypotheses: X, W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X W : WalkingParallelPair
h : WalkingParallelPairHom X W
id :
  ((WalkingParallelPairHom.id zero).comp (WalkingParallelPairHom.id zero)).comp left =
    (WalkingParallelPairHom.id zero).comp ((WalkingParallelPairHom.id zero).comp left)
⊢ ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp h =
    (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp h)
have id₁ : ((WalkingParallelPairHom.id zero).comp (WalkingParallelPairHom.id zero)).comp right =
  (WalkingParallelPairHom.id zero).comp ((WalkingParallelPairHom.id zero).comp right)
Tactic: cases h
Cleared hypotheses: X, W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X W : WalkingParallelPair
h : WalkingParallelPairHom X W
id :
  ((WalkingParallelPairHom.id zero).comp (WalkingParallelPairHom.id zero)).comp left =
    (WalkingParallelPairHom.id zero).comp ((WalkingParallelPairHom.id zero).comp left)
id₁ :
  ((WalkingParallelPairHom.id zero).comp (WalkingParallelPairHom.id zero)).comp right =
    (WalkingParallelPairHom.id zero).comp ((WalkingParallelPairHom.id zero).comp right)
⊢ ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp h =
    (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp h)
have id₂ : ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp (WalkingParallelPairHom.id X) =
  (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X))
Tactic: cases h
Cleared hypotheses: W, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y : WalkingParallelPair
f : X ⟶ Y
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : Y = t) → WalkingParallelPair) Y
          (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
have left : Quiver.Hom (V := WalkingParallelPairᵒᵖ)
  (op
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
        (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) sorry) :
    WalkingParallelPairᵒᵖ)
  (op
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
        (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry) :
    WalkingParallelPairᵒᵖ)
Tactic: cases f
Cleared hypotheses: X, Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X Y : WalkingParallelPair
f : X ⟶ Y
left right :
  Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair)
          zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
          (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : Y = t) → WalkingParallelPair) Y
          (fun (h : Y = zero) ↦ one) (fun (h : Y = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
have id : Quiver.Hom (V := WalkingParallelPairᵒᵖ)
  (op
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
        (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) sorry) :
    WalkingParallelPairᵒᵖ)
  (op
      (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
        (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) sorry) :
    WalkingParallelPairᵒᵖ)
Tactic: cases f
Cleared hypotheses: Y, f
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair)
          zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
          (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
have left : Quiver.Hom (V := WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
      (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry :
    WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
      (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) sorry :
    WalkingParallelPair)
Tactic: apply Quiver.Hom.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair)
          zero (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
          (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
have right : Quiver.Hom (V := WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : one = t) → WalkingParallelPair) one
      (fun (h : one = zero) ↦ one) (fun (h : one = one) ↦ zero) sorry :
    WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
      (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) sorry :
    WalkingParallelPair)
Tactic: apply Quiver.Hom.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
X : WalkingParallelPair
⊢ Quiver.Hom (V := WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) ⋯) :
      WalkingParallelPairᵒᵖ)
have id : Quiver.Hom (V := WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
      (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) sorry :
    WalkingParallelPair)
  (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
      (fun (h : X = zero) ↦ one) (fun (h : X = one) ↦ zero) sorry :
    WalkingParallelPair)
Tactic: apply Quiver.Hom.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
⊢ Functor.obj (𝟭 WalkingParallelPair) j = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j
have zero : Functor.obj (𝟭 WalkingParallelPair) zero = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj zero
Tactic: cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Shapes.Equalizers (goal)
Goal:
j : WalkingParallelPair
zero :
  Functor.obj (𝟭 WalkingParallelPair) WalkingParallelPair.zero =
    (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj WalkingParallelPair.zero
⊢ Functor.obj (𝟭 WalkingParallelPair) j = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj j
have one : Functor.obj (𝟭 WalkingParallelPair) one = (walkingParallelPairOp ⋙ walkingParallelPairOp.leftOp).obj one
Tactic: cases j
Cleared hypotheses: j