awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPairOpIso f g).hom.app WalkingParallelPair.zero =
    𝟙 (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.zero)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPairOpIso f g).hom.app WalkingParallelPair.one =
    𝟙 (obj.{0, v₁, 0, u₁} (parallelPair f.op g.op) WalkingParallelPair.one)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPairOpIso f g).inv.app WalkingParallelPair.zero =
    𝟙 ((walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj WalkingParallelPair.zero)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (parallelPairOpIso f g).inv.app WalkingParallelPair.one =
    𝟙 ((walkingParallelPairOpEquiv.functor ⋙ (parallelPair f g).op).obj WalkingParallelPair.one)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.zero) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.zero))

Tactic:
simp [opParallelPairIso]

Premises used: CategoryTheory.Limits.opParallelPairIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ (opParallelPairIso f g).hom.app (op WalkingParallelPair.one) =
    𝟙 ((parallelPair f g).op.obj (op WalkingParallelPair.one))

Tactic:
simp [opParallelPairIso]

Premises used: CategoryTheory.Limits.opParallelPairIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op) (op WalkingParallelPair.zero) ⟶
      (parallelPair f g).op.obj (op WalkingParallelPair.zero))
    ((opParallelPairIso f g).inv.app (op WalkingParallelPair.zero))
    (𝟙 (obj.{0, v₁, 0, u₁} (walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op) (op WalkingParallelPair.zero)))

Tactic:
simp [opParallelPairIso]

Premises used: CategoryTheory.Limits.opParallelPairIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
⊢ Eq (α :=
    obj.{0, v₁, 0, u₁} (walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op) (op WalkingParallelPair.one) ⟶
      (parallelPair f g).op.obj (op WalkingParallelPair.one))
    ((opParallelPairIso f g).inv.app (op WalkingParallelPair.one))
    (𝟙 (obj.{0, v₁, 0, u₁} (walkingParallelPairOpEquiv.inverse ⋙ parallelPair f.op g.op) (op WalkingParallelPair.one)))

Tactic:
simp [opParallelPairIso]

Premises used: CategoryTheory.Limits.opParallelPairIso
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.π.app WalkingParallelPair.one = (c.ι.app WalkingParallelPair.zero).unop

Tactic:
simp [unop]

Premises used: CategoryTheory.Limits.Cofork.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.π.app WalkingParallelPair.zero = (c.ι.app WalkingParallelPair.one).unop

Tactic:
simp [unop]

Premises used: CategoryTheory.Limits.Cofork.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.ι = c.π.unop

Tactic:
simp [Cofork.unop, Fork.ι]

Premises used: CategoryTheory.Limits.Cofork.unop, CategoryTheory.Limits.Fork.ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.π.app WalkingParallelPair.one = (c.ι.app WalkingParallelPair.zero).op

Tactic:
simp [op]

Premises used: CategoryTheory.Limits.Cofork.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.π.app WalkingParallelPair.zero = (c.ι.app WalkingParallelPair.one).op

Tactic:
simp [op]

Premises used: CategoryTheory.Limits.Cofork.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.ι = c.π.op

Tactic:
simp [Cofork.op, Fork.ι]

Premises used: CategoryTheory.Limits.Fork.ι, CategoryTheory.Limits.Cofork.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.ι.app WalkingParallelPair.one = (c.π.app WalkingParallelPair.zero).unop

Tactic:
simp [unop]

Premises used: CategoryTheory.Limits.Fork.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.ι.app WalkingParallelPair.zero = (c.π.app WalkingParallelPair.one).unop

Tactic:
simp [unop]

Premises used: CategoryTheory.Limits.Fork.unop
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.ι.app WalkingParallelPair.one = (c.π.app WalkingParallelPair.zero).op

Tactic:
simp [op]

Premises used: CategoryTheory.Limits.Fork.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.ι.app WalkingParallelPair.zero = (c.π.app WalkingParallelPair.one).op

Tactic:
simp [op]

Premises used: CategoryTheory.Limits.Fork.op
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.π = c.ι.op

Tactic:
simp [Fork.op, Cofork.π]

Premises used: CategoryTheory.Limits.Fork.op, CategoryTheory.Limits.Cofork.π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.unop.π = c.π

Tactic:
simp [Fork.unop_π, Cofork.op_ι]

Premises used: CategoryTheory.Limits.Cofork.op_ι, CategoryTheory.Limits.Fork.unop_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.op.π = c.π

Tactic:
simp [Fork.op_π, Cofork.unop_ι]

Premises used: CategoryTheory.Limits.Fork.op_π, CategoryTheory.Limits.Cofork.unop_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
⊢ c.op.unop.π ≫ Iso.hom (Iso.refl c.op.unop.pt) = c.π

Tactic:
simp [op_unop_π]

Premises used: CategoryTheory.Limits.Cofork.op_unop_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.op.π ≫ Iso.hom (Iso.refl c.unop.op.pt) = c.π

Tactic:
simp [unop_op_π]

Premises used: CategoryTheory.Limits.Cofork.unop_op_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ c.op.unop.ι = c.ι

Tactic:
simp [Cofork.unop_ι, Fork.op_π]

Premises used: CategoryTheory.Limits.Fork.op_π, CategoryTheory.Limits.Cofork.unop_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ c.unop.op.ι = c.ι

Tactic:
simp [Fork.unop_π, Cofork.op_ι]

Premises used: CategoryTheory.Limits.Cofork.op_ι, CategoryTheory.Limits.Fork.unop_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Fork f g
⊢ Iso.hom (Iso.refl c.op.unop.pt) ≫ c.ι = c.op.unop.ι

Tactic:
simp [op_unop_ι]

Premises used: CategoryTheory.Limits.Fork.op_unop_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Fork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
⊢ Iso.hom (Iso.refl c.unop.op.pt) ≫ c.ι = c.unop.op.ι

Tactic:
simp [unop_op_ι]

Premises used: CategoryTheory.Limits.Fork.unop_op_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
f₁ : IsColimit c → IsLimit c.op
g₁ : IsLimit c.op → IsColimit c
⊢ IsColimit c ≃ IsLimit c.op

Tactic:
apply equivOfSubsingletonOfSubsingleton

Premises used: equivOfSubsingletonOfSubsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
h : IsColimit c
⊢ IsLimit c.op

Tactic:
exact (IsLimit.postcomposeHomEquiv _ _).invFun ((IsLimit.whiskerEquivalenceEquiv _).toFun h.op)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, Equiv.toFun, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv, Equiv.invFun
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f g : X ⟶ Y
c : Cofork f g
h : IsLimit c.op
⊢ IsColimit c

Tactic:
exact (IsColimit.equivIsoColimit c.opUnopIso).toFun (((IsLimit.postcomposeHomEquiv _ _).invFun
      ((IsLimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop)

Premises used: CategoryTheory.Limits.IsLimit.postcomposeHomEquiv, CategoryTheory.Limits.Cofork.opUnopIso, CategoryTheory.Limits.IsColimit.equivIsoColimit, CategoryTheory.Limits.IsLimit.unop, Equiv.toFun, CategoryTheory.Limits.IsLimit.whiskerEquivalenceEquiv, CategoryTheory.Equivalence.symm, Equiv.invFun, CategoryTheory.Limits.walkingParallelPairOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
f₁ : IsColimit c → IsLimit c.unop
g₁ : IsLimit c.unop → IsColimit c
⊢ IsColimit c ≃ IsLimit c.unop

Tactic:
apply equivOfSubsingletonOfSubsingleton

Premises used: equivOfSubsingletonOfSubsingleton
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
h : IsColimit c
⊢ IsLimit c.unop

Tactic:
exact ((IsColimit.precomposeHomEquiv _ _).invFun
      ((IsColimit.whiskerEquivalenceEquiv walkingParallelPairOpEquiv.symm).toFun h)).unop

Premises used: Equiv.toFun, CategoryTheory.Limits.IsColimit.unop, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, Equiv.invFun, CategoryTheory.Limits.walkingParallelPairOpEquiv, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f g : X ⟶ Y
c : Cofork.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) f g
h : IsLimit c.unop
⊢ IsColimit c

Tactic:
exact (IsColimit.equivIsoColimit c.unopOpIso).toFun
      ((IsColimit.precomposeHomEquiv _ _).invFun ((IsColimit.whiskerEquivalenceEquiv _).toFun h.op))

Premises used: CategoryTheory.Limits.IsLimit.op, CategoryTheory.Limits.IsColimit.equivIsoColimit, Equiv.toFun, CategoryTheory.Limits.Cofork.unopOpIso, CategoryTheory.Limits.IsColimit.precomposeHomEquiv, Equiv.invFun, CategoryTheory.Limits.IsColimit.whiskerEquivalenceEquiv
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y P : C
f g : X ⟶ Y
π π' : Y ⟶ P
w : f ≫ π = g ≫ π
w' : Eq.{v₁ + 1} (α := Opposite.op P ⟶ Opposite.op X) (π'.op ≫ f.op) (π'.op ≫ g.op)
h : π = π'
⊢ Iso.hom (Iso.refl (ofπ π w).op.pt) ≫ Fork.ι (Fork.ofι π'.op w') = (ofπ π w).op.ι

Tactic:
simp [Cofork.op_ι, h]

Premises used: CategoryTheory.Limits.Cofork.op_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y P : Cᵒᵖ
f g : X ⟶ Y
π π' : Y ⟶ P
w : Eq.{v₁ + 1} (α := X ⟶ P) (f ≫ π) (g ≫ π)
w' : π'.unop ≫ f.unop = π'.unop ≫ g.unop
h : π = π'
⊢ Iso.hom (Iso.refl (Cone.pt.{0, v₁, 0, u₁} (F := parallelPair f.unop g.unop) (unop (ofπ π w)))) ≫
      (Fork.ofι π'.unop w').ι =
    Fork.ι (unop (ofπ π w))

Tactic:
simp [Cofork.unop_ι, h]

Premises used: CategoryTheory.Limits.Cofork.unop_ι
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y P : C
f g : X ⟶ Y
ι ι' : P ⟶ X
w : ι ≫ f = ι ≫ g
w' : Eq.{v₁ + 1} (α := Opposite.op Y ⟶ Opposite.op P) (f.op ≫ ι'.op) (g.op ≫ ι'.op)
h : ι = ι'
⊢ (ofι ι w).op.π ≫ Iso.hom (Iso.refl (ofι ι w).op.pt) = Cofork.π (Cofork.ofπ ι'.op w')

Tactic:
simp [Fork.op_π, h]

Premises used: CategoryTheory.Limits.Fork.op_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y P : Cᵒᵖ
f g : X ⟶ Y
ι ι' : P ⟶ X
w : Eq.{v₁ + 1} (α := P ⟶ Y) (ι ≫ f) (ι ≫ g)
w' : f.unop ≫ ι'.unop = g.unop ≫ ι'.unop
h : ι = ι'
⊢ Cofork.π (unop (ofι ι w)) ≫
      Iso.hom (Iso.refl (Cocone.pt.{0, v₁, 0, u₁} (F := parallelPair f.unop g.unop) (unop (ofι ι w)))) =
    (Cofork.ofπ ι'.unop w').π

Tactic:
simp [Fork.unop_π, h]

Premises used: CategoryTheory.Limits.Fork.unop_π
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h : IsColimit (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (ofπ f ⋯)
⊢ Eq.{v₁ + 1} (α := Opposite.op Y ⟶ Opposite.op (pullback f f)) (f.op ≫ Quiver.Hom.op (pullback.fst f f))
    (f.op ≫ Quiver.Hom.op (pullback.snd f f))

Tactic:
simp only [← op_comp, pullback.condition]

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h : IsColimit (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (ofπ f ⋯)
⊢ Eq (α := Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)
    (Iso.hom (Iso.refl (Opposite.op X)) ≫ pushout.inl f.op f.op :
      Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)
    (CategoryStruct.comp (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.fst f f))
        (Iso.hom (Iso.symm (Iso.op (pullbackIsoUnopPushout f f)))) :
      Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h : IsColimit (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (ofπ f ⋯)
⊢ Eq (α := Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)
    (Iso.hom (Iso.refl (Opposite.op X)) ≫ pushout.inr f.op f.op :
      Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)
    (CategoryStruct.comp (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.snd f f))
        (Iso.hom (Iso.symm (Iso.op (pullbackIsoUnopPushout f f)))) :
      Opposite.op X ⟶ pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op)

Tactic:
simp [← op_comp]

Premises used: CategoryTheory.op_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h : IsColimit (F := parallelPair (X := pullback f f) (pullback.fst f f) (pullback.snd f f)) (ofπ f ⋯)
⊢ Eq.{v₁ + 1} (α :=
    Cone.pt.{0, v₁, 0, u₁} (F :=
        parallelPair (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.fst f f))
          (Quiver.Hom.op (pullback.snd f f)))
        (Fork.ofι f.op ⋯) ⟶
      Opposite.op X)
    (Iso.hom
          (Iso.refl
            (Cone.pt.{0, v₁, 0, u₁} (F :=
              parallelPair (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.fst f f))
                (Quiver.Hom.op (pullback.snd f f)))
              (Fork.ofι f.op ⋯))) ≫
        Fork.ι (Fork.ofι f.op ⋯) :
      Cone.pt.{0, v₁, 0, u₁} (F :=
          parallelPair (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.fst f f))
            (Quiver.Hom.op (pullback.snd f f)))
          (Fork.ofι f.op ⋯) ⟶
        Opposite.op X)
    (Fork.ι (Fork.ofι f.op ⋯) ≫ Iso.hom (Iso.refl (Opposite.op X)) :
      Cone.pt.{0, v₁, 0, u₁} (F :=
          parallelPair (Y := Opposite.op (pullback f f)) (Quiver.Hom.op (pullback.fst f f))
            (Quiver.Hom.op (pullback.snd f f)))
          (Fork.ofι f.op ⋯) ⟶
        Opposite.op X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
rw :
  Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)
rw₁ :
  Eq.{v₁ + 1} (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inl f.op f.op)) (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op)) (Quiver.Hom.unop (f.op ≫ pushout.inr f.op f.op))
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶
      Opposite.unop (Opposite.op Y))
    (Quiver.Hom.unop (pushout.inl f.op f.op) ≫ f.op.unop) (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ f.op.unop)

Tactic:
rw [← unop_comp, ← unop_comp, pushout.condition]

Premises used: CategoryTheory.Limits.pushout.condition, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) (Iso.hom (Iso.symm (pullbackIsoUnopPushout f f))) (pullback.fst f f) :
      Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)
    (Quiver.Hom.unop (pushout.inl f.op f.op) ≫ Iso.hom (Iso.refl (Opposite.unop (Opposite.op X))) :
      Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : C
f : X ⟶ Y
inst_2 : HasPullback f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Opposite.op X) (Y :=
      pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) (pushout.inl f.op f.op)
      (pushout.inr f.op f.op))
    (Fork.ofι f.op ⋯)
⊢ Eq (α :=
    Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)
    (CategoryStruct.comp (Y := pullback f f) (Iso.hom (Iso.symm (pullbackIsoUnopPushout f f))) (pullback.snd f f) :
      Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)
    (Quiver.Hom.unop (pushout.inr f.op f.op) ≫ Iso.hom (Iso.refl (Opposite.unop (Opposite.op X))) :
      Opposite.unop (pushout.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op X) (Z := Opposite.op X) f.op f.op) ⟶ X)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := X) (Z := Y) f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f) (pullback.fst f f) (pullback.snd f f))
    (ofπ f ⋯)
⊢ Eq (α := Opposite.unop Y ⟶ Opposite.unop (pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f))
    (f.unop ≫ Quiver.Hom.unop (pullback.fst f f)) (f.unop ≫ Quiver.Hom.unop (pullback.snd f f))

Tactic:
simp only [← unop_comp, pullback.condition]

Premises used: CategoryTheory.unop_comp, CategoryTheory.Limits.pullback.condition
-- Module: Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
X Y : Cᵒᵖ
f : X ⟶ Y
inst_2 : HasPullback.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := X) (Z := Y) f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f) (pullback.fst f f) (pullback.snd f f))
    (ofπ f ⋯)
⊢ Eq (α := Opposite.unop X ⟶ pushout f.unop f.unop)
    (Iso.hom (Iso.refl (Opposite.unop X)) ≫ pushout.inl f.unop f.unop : Opposite.unop X ⟶ pushout f.unop f.unop)
    (CategoryStruct.comp (Y := Opposite.unop (pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f))
        (Quiver.Hom.unop (pullback.fst f f)) (Iso.hom (Iso.symm (Iso.unop (pullbackIsoOpPushout f f)))) :
      Opposite.unop X ⟶ pushout f.unop f.unop)

Tactic:
simp [← unop_comp]

Premises used: CategoryTheory.unop_comp