awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
Goal:
C : Type u
inst : Category.{v, u} C
H : ∀ (X Y : C), BinaryCoproductDisjoint.{v, u} X Y
X : WalkingPair → C
⊢ X WalkingPair.right =
    WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) WalkingPair.right (X WalkingPair.left)
      (X WalkingPair.right)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
W₁ W₂ : Wedge F
e : W₁.pt ≅ W₂.pt
he : ∀ (j : J), Multifork.ι W₁ j = e.hom ≫ Multifork.ι W₂ j
j : WalkingMulticospan (multicospanShapeEnd.{v, u} J)
f : (multicospanShapeEnd.{v, u} J).R
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (WalkingMulticospan (multicospanShapeEnd.{v, u} J))) W₁.pt)
        (WalkingMulticospan.right f) ⟶
      (multicospanIndexEnd F).multicospan.obj (WalkingMulticospan.right f))
    (W₁.π.app (WalkingMulticospan.right f)) (e.hom ≫ W₂.π.app (WalkingMulticospan.right f))

Tactic:
simpa using (he f.left) =≫ _

Premises used: CategoryTheory.Arrow.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
pt : C
π : (j : J) → pt ⟶ (F.obj (op j)).obj j
hπ : ∀ ⦃i j : J⦄ (f : i ⟶ j), π i ≫ (F.obj (op i)).map f = π j ≫ (F.map f.op).app j
j : J
⊢ Multifork.ι (mk pt π hπ) j = π j

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multifork.ι, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Wedge F
i j : J
f : i ⟶ j
⊢ Multifork.ι c i ≫ (F.obj (op i)).map f = Multifork.ι c j ≫ (F.map f.op).app j

Tactic:
Multifork.condition c (Arrow.mk f)

Premises used: CategoryTheory.Limits.Multifork.condition, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Wedge F
hc : IsLimit c
X : C
f g : X ⟶ c.pt
h : ∀ (j : (multicospanShapeEnd.{v, u} J).L), f ≫ Multifork.ι c j = g ≫ Multifork.ι c j
⊢ f = g

Tactic:
Multifork.IsLimit.hom_ext hc h

Premises used: CategoryTheory.Limits.Multifork.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Wedge F
hc : IsLimit c
X : C
f : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ lift hc f hf ≫ Multifork.ι c j = f j

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
W₁ W₂ : Cowedge F
e : W₁.pt ≅ W₂.pt
he : ∀ (j : J), Multicofork.π W₁ j ≫ e.hom = Multicofork.π W₂ j
j : WalkingMultispan (multispanShapeCoend.{v, u} J)
f : (multispanShapeCoend.{v, u} J).L
⊢ Eq (α := (multispanIndexCoend F).multispan.obj (WalkingMultispan.left f) ⟶ W₂.pt)
    (W₁.ι.app (WalkingMultispan.left f) ≫ e.hom) (W₂.ι.app (WalkingMultispan.left f))

Tactic:
simpa using _ ≫= (he f.left)

Premises used: CategoryTheory.Arrow.left
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
pt : C
ι : (j : J) → (F.obj (op j)).obj j ⟶ pt
hι : ∀ ⦃i j : J⦄ (f : i ⟶ j), (F.map f.op).app i ≫ ι i = (F.obj (op j)).map f ≫ ι j
j : J
⊢ Multicofork.π (mk pt ι hι) j = ι j

Tactic:
rfl

Premises used: CategoryTheory.Limits.Multicofork.π, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Cowedge F
i j : J
f : i ⟶ j
⊢ (F.map f.op).app i ≫ Multicofork.π c i = (F.obj (op j)).map f ≫ Multicofork.π c j

Tactic:
Multicofork.condition c (Arrow.mk f)

Premises used: CategoryTheory.Limits.Multicofork.condition, CategoryTheory.Arrow.mk
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Cowedge F
hc : IsColimit c
X : C
f g : c.pt ⟶ X
h : ∀ (j : (multispanShapeCoend.{v, u} J).R), Multicofork.π c j ≫ f = Multicofork.π c j ≫ g
⊢ f = g

Tactic:
Multicofork.IsColimit.hom_ext hc h

Premises used: CategoryTheory.Limits.Multicofork.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
c : Cowedge F
hc : IsColimit c
X : C
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
j : J
⊢ Multicofork.π c j ≫ desc hc f hf = f j

Tactic:
apply IsColimit.fac

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
i j : J
f : i ⟶ j
⊢ Eq (α := end_ F ⟶ (F.obj (op i)).obj j) (π F i ≫ (F.obj (op i)).map f) (π F j ≫ (F.map f.op).app j)

Tactic:
apply Wedge.condition

Premises used: CategoryTheory.Limits.Wedge.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 g : X ⟶ end_ F
h : ∀ (j : J), f ≫ π F j = g ≫ π F j
⊢ f = g

Tactic:
Multiequalizer.hom_ext _ _ _ (fun _ ↦ h _)

Premises used: CategoryTheory.Limits.end_, CategoryTheory.Limits.Multiequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : (j : J) → X ⟶ (F.obj (op j)).obj j
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), f i ≫ (F.obj (op i)).map g = f j ≫ (F.map g.op).app j
j : J
⊢ CategoryStruct.comp (Y := end_ F) (lift f hf) (π F j) = f j

Tactic:
apply IsLimit.fac

Premises used: CategoryTheory.Limits.IsLimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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'
⊢ (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 φ
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 φ
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')
⊢ 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')

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 φ
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')
⊢ 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:
rw [← e, reassoc_of% end_.condition F φ]

Premises used: CategoryTheory.Limits.end_.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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' ≫ (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:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasEnd F'
f : F ⟶ F'
j : J
⊢ Eq (α := end_ F ⟶ (F'.obj (op j)).obj j) (CategoryStruct.comp (Y := end_ F') (map f) (π F' j))
    (π F j ≫ NatTrans.app (f.app (op j)) j)

Tactic:
simp [end_.map]

Premises used: CategoryTheory.Limits.end_.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : HasCoend F
i j : J
f : i ⟶ j
⊢ Eq (α := (F.obj (op j)).obj i ⟶ coend F) ((F.map f.op).app i ≫ ι F i) ((F.obj (op j)).map f ≫ ι F j)

Tactic:
apply Cowedge.condition

Premises used: CategoryTheory.Limits.Cowedge.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : HasCoend F
X : C
f g : coend F ⟶ X
h : ∀ (j : J), ι F j ≫ f = ι F j ≫ g
⊢ f = g

Tactic:
Multicoequalizer.hom_ext _ _ _ (fun _ ↦ h _)

Premises used: CategoryTheory.Limits.coend, CategoryTheory.Limits.Multicoequalizer.hom_ext
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : HasCoend F
X : C
f : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f i = (F.obj (op j)).map g ≫ f j
j : J
⊢ CategoryStruct.comp (Y := coend F) (ι F j) (desc f hf) = f j

Tactic:
apply IsColimit.fac

Premises used: CategoryTheory.Limits.IsColimit.fac
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : HasCoend F
X : C
f_1 : (j : J) → (F.obj (op j)).obj j ⟶ X
hf : ∀ ⦃i j : J⦄ (g : i ⟶ j), (F.map g.op).app i ≫ f_1 i = (F.obj (op j)).map g ≫ f_1 j
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasCoend F'
f : F ⟶ F'
j j' : J
φ : j ⟶ j'
⊢ Eq (α := (F.obj (op j')).obj j ⟶ coend F')
    ((F.map φ.op).app j ≫ (fun (x : J) ↦ (NatTrans.app (f.app (op x)) x ≫ ι F' x : (F.obj (op x)).obj x ⟶ coend F')) j)
    ((F.obj (op j')).map φ ≫
      (fun (x : J) ↦ (NatTrans.app (f.app (op x)) x ≫ ι F' x : (F.obj (op x)).obj x ⟶ coend F')) j')

Tactic:
simp [coend.condition]

Premises used: CategoryTheory.Limits.coend.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.End
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 : HasCoend F
F' : Jᵒᵖ ⥤ Functor.{v, v', u, u'} J C
inst_3 : HasCoend F'
f : F ⟶ F'
j : J
⊢ Eq (α := (F.obj (op j)).obj j ⟶ coend F') (CategoryStruct.comp (Y := coend F) (ι F j) (map f))
    (NatTrans.app (f.app (op j)) j ≫ ι F' j)

Tactic:
simp [coend.map]

Premises used: CategoryTheory.Limits.coend.map
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X Y : WalkingParallelPair
g : WalkingParallelPairHom X Y
⊢ (id X).comp g = g

Tactic:
rfl

Premises used: CategoryTheory.Limits.WalkingParallelPairHom.comp, rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X Y : WalkingParallelPair
f : WalkingParallelPairHom X Y
left : WalkingParallelPairHom.left.comp (WalkingParallelPairHom.id one) = WalkingParallelPairHom.left
right : WalkingParallelPairHom.right.comp (WalkingParallelPairHom.id one) = WalkingParallelPairHom.right
id : (WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X) = WalkingParallelPairHom.id X
⊢ f.comp (WalkingParallelPairHom.id Y) = f

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

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
⊢ (id X).comp (id X) = id X

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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)
id :
  ∀ (g : WalkingParallelPairHom X Z),
    ((WalkingParallelPairHom.id X).comp g).comp h = (WalkingParallelPairHom.id X).comp (g.comp h)
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
left :
  ∀ (h : WalkingParallelPairHom one W),
    (WalkingParallelPairHom.left.comp (id one)).comp h = WalkingParallelPairHom.left.comp ((id one).comp h)
⊢ (WalkingParallelPairHom.left.comp g).comp h = WalkingParallelPairHom.left.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
Z W : WalkingParallelPair
h : WalkingParallelPairHom Z W
g : WalkingParallelPairHom one Z
right :
  ∀ (h : WalkingParallelPairHom one W),
    (WalkingParallelPairHom.right.comp (id one)).comp h = WalkingParallelPairHom.right.comp ((id one).comp h)
⊢ (WalkingParallelPairHom.right.comp g).comp h = WalkingParallelPairHom.right.comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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)
id₂ :
  ∀ (h : WalkingParallelPairHom X W),
    ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp h =
      (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp h)
⊢ ((WalkingParallelPairHom.id X).comp g).comp h = (WalkingParallelPairHom.id X).comp (g.comp h)

Tactic:
cases g
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
left :
  (WalkingParallelPairHom.left.comp (id one)).comp (id one) = WalkingParallelPairHom.left.comp ((id one).comp (id one))
⊢ (WalkingParallelPairHom.left.comp (id one)).comp h = WalkingParallelPairHom.left.comp ((id one).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
right :
  (WalkingParallelPairHom.right.comp (id one)).comp (id one) =
    WalkingParallelPairHom.right.comp ((id one).comp (id one))
⊢ (WalkingParallelPairHom.right.comp (id one)).comp h = WalkingParallelPairHom.right.comp ((id one).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
id :
  ((WalkingParallelPairHom.id zero).comp left).comp (WalkingParallelPairHom.id one) =
    (WalkingParallelPairHom.id zero).comp (left.comp (WalkingParallelPairHom.id one))
⊢ ((WalkingParallelPairHom.id zero).comp left).comp h = (WalkingParallelPairHom.id zero).comp (left.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
W : WalkingParallelPair
h : WalkingParallelPairHom one W
id :
  ((WalkingParallelPairHom.id zero).comp right).comp (WalkingParallelPairHom.id one) =
    (WalkingParallelPairHom.id zero).comp (right.comp (WalkingParallelPairHom.id one))
⊢ ((WalkingParallelPairHom.id zero).comp right).comp h = (WalkingParallelPairHom.id zero).comp (right.comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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)
id₂ :
  ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp (WalkingParallelPairHom.id X) =
    (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X))
⊢ ((WalkingParallelPairHom.id X).comp (WalkingParallelPairHom.id X)).comp h =
    (WalkingParallelPairHom.id X).comp ((WalkingParallelPairHom.id X).comp h)

Tactic:
cases h
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ (left.comp (id one)).comp (id one) = left.comp ((id one).comp (id one))

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ ((id zero).comp left).comp (id one) = (id zero).comp (left.comp (id one))

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ ((id zero).comp (id zero)).comp left = (id zero).comp ((id zero).comp left)

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

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
⊢ ((id X).comp (id X)).comp (id X) = (id X).comp ((id X).comp (id X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
X : WalkingParallelPair
⊢ WalkingParallelPairHom.id X = 𝟙 X

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
x zero one : WalkingParallelPair
⊢ WalkingParallelPair

Tactic:
cases x
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
⊢ WalkingParallelPair

Tactic:
exacts [one, zero]

Premises used: CategoryTheory.Limits.WalkingParallelPair.one, CategoryTheory.Limits.WalkingParallelPair.zero
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
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ᵒᵖ)
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) ⋯) :
      WalkingParallelPairᵒᵖ)
    (op
        (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : X = t) → WalkingParallelPair) X
          (fun (h : X = zero) ↦ one) (fun (h : X = 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ᵒᵖ)

Tactic:
cases f
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
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) ⋯ :
      WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
        (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯ :
      WalkingParallelPair)
⊢ 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ᵒᵖ)

Tactic:
apply Quiver.Hom.op

Premises used: Quiver.Hom.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Equalizers
Goal:
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) ⋯ :
      WalkingParallelPair)
    (WalkingParallelPair.casesOn (motive := fun (t : WalkingParallelPair) ↦ (h : zero = t) → WalkingParallelPair) zero
        (fun (h : zero = zero) ↦ one) (fun (h : zero = one) ↦ zero) ⋯ :
      WalkingParallelPair)
⊢ 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ᵒᵖ)

Tactic:
apply Quiver.Hom.op

Premises used: Quiver.Hom.op