awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.inr 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.snd 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
-- 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 ⋯)
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (X := Opposite.unop X) (Y := Opposite.unop (pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f))
              (Quiver.Hom.unop (pullback.fst f f)) (Quiver.Hom.unop (pullback.snd f f)))
            (Fork.ofι f.unop ⋯))) ≫
      Fork.ι (Fork.ofι f.unop ⋯) =
    Fork.ι (Fork.ofι f.unop ⋯) ≫ Iso.hom (Iso.refl (Opposite.unop 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 :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
rw :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)
rw₁ :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inl f.unop f.unop)) (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop))
rw₂ rw₃ :
  Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop)) (Quiver.Hom.op (f.unop ≫ pushout.inr f.unop f.unop))
⊢ Eq.{v₁ + 1} (α := Opposite.op (pushout f.unop f.unop) ⟶ Opposite.op (Opposite.unop Y))
    (Quiver.Hom.op (pushout.inl f.unop f.unop) ≫ f.unop.op) (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ f.unop.op)

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

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.pushout.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 :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
⊢ Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f)
        (Iso.hom (Iso.symm (pullbackIsoOpPushout f f))) (pullback.fst f f) :
      Opposite.op (pushout f.unop f.unop) ⟶ X)
    (Quiver.Hom.op (pushout.inl f.unop f.unop) ≫ Iso.hom (Iso.refl (Opposite.op (Opposite.unop X))) :
      Opposite.op (pushout f.unop f.unop) ⟶ 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 :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
⊢ Eq (α := Opposite.op (pushout f.unop f.unop) ⟶ X)
    (CategoryStruct.comp (Y := pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f)
        (Iso.hom (Iso.symm (pullbackIsoOpPushout f f))) (pullback.snd f f) :
      Opposite.op (pushout f.unop f.unop) ⟶ X)
    (Quiver.Hom.op (pushout.inr f.unop f.unop) ≫ Iso.hom (Iso.refl (Opposite.op (Opposite.unop X))) :
      Opposite.op (pushout f.unop f.unop) ⟶ 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 :
  IsLimit (F := parallelPair (Y := pushout f.unop f.unop) (pushout.inl f.unop f.unop) (pushout.inr f.unop f.unop))
    (Fork.ofι f.unop ⋯)
⊢ Eq.{v₁ + 1} (α :=
    X ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F :=
        parallelPair (X := pullback.{v₁, u₁} (X := X) (Y := X) (Z := Y) f f) (pullback.fst f f) (pullback.snd f f))
        (ofπ f ⋯))
    (Iso.inv (Iso.refl (Opposite.op (Opposite.unop X))) ≫
      π (ofπ f.unop.op ⋯) ≫
        Iso.hom
          (Iso.refl
            (Cocone.pt.{0, v₁, 0, u₁} (F :=
              parallelPair (X := Opposite.op (pushout f.unop f.unop)) (Quiver.Hom.op (pushout.inl f.unop f.unop))
                (Quiver.Hom.op (pushout.inr f.unop f.unop)))
              (ofπ f.unop.op ⋯))))
    (π (ofπ f ⋯))

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 : HasPushout f f
h : IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι f ⋯)
⊢ Eq.{v₁ + 1} (α := Opposite.op (pushout f f) ⟶ Opposite.op X) (Quiver.Hom.op (pushout.inl f f) ≫ f.op)
    (Quiver.Hom.op (pushout.inr f f) ≫ f.op)

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

Premises used: CategoryTheory.op_comp, CategoryTheory.Limits.pushout.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 : HasPushout f f
h : IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι f ⋯)
⊢ Eq (α := Opposite.op (pushout f f) ⟶ Opposite.op Y)
    (Iso.hom (Iso.symm (Iso.op (pushoutIsoUnopPullback f f)) ≪≫ eqToIso ⋯) ≫ pullback.fst f.op f.op)
    (Quiver.Hom.op (pushout.inl f f) ≫ Iso.hom (Iso.refl (Opposite.op Y)))

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 : HasPushout f f
h : IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι f ⋯)
⊢ Eq (α := Opposite.op (pushout f f) ⟶ Opposite.op Y)
    (Iso.hom (Iso.symm (Iso.op (pushoutIsoUnopPullback f f)) ≪≫ eqToIso ⋯) ≫ pullback.snd f.op f.op)
    (Quiver.Hom.op (pushout.inr f f) ≫ Iso.hom (Iso.refl (Opposite.op Y)))

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 : HasPushout f f
h : IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι f ⋯)
⊢ Eq.{v₁ + 1} (α :=
    Opposite.op Y ⟶
      Cocone.pt.{0, v₁, 0, u₁} (F :=
        parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
          (pullback.fst f.op f.op) (pullback.snd f.op f.op))
        (Cofork.ofπ f.op ⋯))
    (Iso.inv (Iso.refl (Opposite.op Y)) ≫
      Cofork.π (Cofork.ofπ f.op ⋯) ≫
        Iso.hom
          (Iso.refl
            (Cocone.pt.{0, v₁, 0, u₁} (F :=
              parallelPair (X := Opposite.op (pushout f f)) (Quiver.Hom.op (pushout.inl f f))
                (Quiver.Hom.op (pushout.inr f f)))
              (Cofork.ofπ f.op ⋯))))
    (Cofork.π (Cofork.ofπ f.op ⋯))

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 : HasPushout f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
⊢ Eq (α :=
    Opposite.unop (Opposite.op X) ⟶
      Opposite.unop (pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op))
    (f.op.unop ≫ Quiver.Hom.unop (pullback.fst f.op f.op)) (f.op.unop ≫ Quiver.Hom.unop (pullback.snd f.op f.op))

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 : HasPushout f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
⊢ Iso.hom
        (Iso.refl
          (Cone.pt (F :=
            parallelPair (X := Opposite.unop (Opposite.op Y)) (Y :=
              Opposite.unop
                (pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op))
              (Quiver.Hom.unop (pullback.fst f.op f.op)) (Quiver.Hom.unop (pullback.snd f.op f.op)))
            (ofι f.op.unop ⋯ :
              Fork.{v₁, u₁} (C := C) (X := Opposite.unop (Opposite.op Y)) (Y :=
                Opposite.unop
                  (pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op))
                (Quiver.Hom.unop (pullback.fst f.op f.op)) (Quiver.Hom.unop (pullback.snd f.op f.op))))) ≫
      ι (ofι f ⋯) =
    ι (ofι f.op.unop ⋯) ≫ Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y)))

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 : HasPushout f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))
⊢ IsLimit (F := parallelPair (Y := pushout f f) (pushout.inl f f) (pushout.inr f f)) (ofι f ⋯)

Tactic:
refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitUnop f.op f.op
      pullback.condition (by simp only [← unop_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoUnopPullback f f).symm) (.refl _) ?_ ?_ (by simp)

Premises used: Quiver.Hom.op, CategoryTheory.Iso.refl, CategoryTheory.Limits.pushoutIsoUnopPullback, CategoryTheory.Limits.Fork.isLimitOfIsos, CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop, CategoryTheory.Iso.symm, CategoryTheory.Limits.pullback.condition, DFunLike.coe, rfl
-- 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 : HasPushout f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_1 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_1₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_1₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.fst f.op f.op))
refine_1₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inl f f)))
refine_1₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f) (pushout.inl f f)
refine_1₅ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inl f f)
    (pushout.inl f f)
refine_1₆ refine_1₇ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (pushout.inl f f) (pushout.inl f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inl f f)
    (Quiver.Hom.unop (pullback.fst f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))

Tactic:
rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_fst, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.pushoutIsoUnopPullback, CategoryTheory.unop_comp, CategoryTheory.Iso.inv, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_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 : HasPushout f f
h :
  IsColimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := pullback.{v₁, u₁} (X := Opposite.op Y) (Y := Opposite.op Y) (Z := Opposite.op X) f.op f.op)
      (pullback.fst f.op f.op) (pullback.snd f.op f.op))
    (Cofork.ofπ f.op ⋯)
refine_2 :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.inv (pushoutIsoUnopPullback f f))
refine_2₁ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f))))
refine_2₂ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (Iso.inv (pushoutIsoUnopPullback f f)) ≫ pullback.snd f.op f.op))
refine_2₃ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (Quiver.Hom.op (pushout.inr f f)))
refine_2₄ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f) (pushout.inr f f)
refine_2₅ :
  Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (𝟙 (Opposite.unop (Opposite.op Y)) ≫ pushout.inr f f)
    (pushout.inr f f)
refine_2₆ refine_2₇ : Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f) (pushout.inr f f) (pushout.inr f f)
⊢ Eq (α := Opposite.unop (Opposite.op Y) ⟶ pushout f f)
    (Iso.hom (Iso.refl (Opposite.unop (Opposite.op Y))) ≫ pushout.inr f f)
    (Quiver.Hom.unop (pullback.snd f.op f.op) ≫ Iso.hom (Iso.symm (pushoutIsoUnopPullback f f)))

Tactic:
rw [Iso.symm_hom, ← Quiver.Hom.unop_op (pushoutIsoUnopPullback f f).inv, ← unop_comp,
        pushoutIsoUnopPullback_inv_snd, Quiver.Hom.unop_op, Iso.refl_hom, Category.id_comp]

Premises used: Quiver.Hom.unop_op, CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd, CategoryTheory.Iso.symm_hom, CategoryTheory.Limits.pushoutIsoUnopPullback, CategoryTheory.unop_comp, CategoryTheory.Iso.inv, CategoryTheory.Iso.refl_hom, CategoryTheory.Category.id_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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
⊢ Eq (α := Opposite.unop (pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) ⟶ Opposite.unop X)
    (Quiver.Hom.unop (pushout.inl f f) ≫ f.unop) (Quiver.Hom.unop (pushout.inr f f) ≫ f.unop)

Tactic:
simp only [← 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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
⊢ Eq (α := Opposite.unop (pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) ⟶ Opposite.unop Y)
    (Iso.hom (Iso.symm (Iso.unop (pushoutIsoOpPullback f f)) ≪≫ eqToIso ⋯) ≫ pullback.fst f.unop f.unop)
    (Quiver.Hom.unop (pushout.inl f f) ≫ Iso.hom (Iso.refl (Opposite.unop Y)))

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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
⊢ Eq (α := Opposite.unop (pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) ⟶ Opposite.unop Y)
    (Iso.hom (Iso.symm (Iso.unop (pushoutIsoOpPullback f f)) ≪≫ eqToIso ⋯) ≫ pullback.snd f.unop f.unop)
    (Quiver.Hom.unop (pushout.inr f f) ≫ Iso.hom (Iso.refl (Opposite.unop Y)))

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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)
⊢ Iso.inv (Iso.refl (Opposite.unop Y)) ≫
      Cofork.π (Cofork.ofπ f.unop ⋯) ≫
        Iso.hom
          (Iso.refl
            (Cocone.pt (F :=
              parallelPair (X := Opposite.unop (pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)) (Y := Opposite.unop Y)
                (Quiver.Hom.unop (pushout.inl f f)) (Quiver.Hom.unop (pushout.inr f f)))
              (Cofork.ofπ f.unop ⋯))) =
    Cofork.π (Cofork.ofπ f.unop ⋯)

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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsColimit (F := parallelPair (X := pullback f.unop f.unop) (pullback.fst f.unop f.unop) (pullback.snd f.unop f.unop))
    (Cofork.ofπ f.unop ⋯)
⊢ Eq.{v₁ + 1} (α := Opposite.op (Opposite.unop X) ⟶ Opposite.op (pullback f.unop f.unop))
    (f.unop.op ≫ Quiver.Hom.op (pullback.fst f.unop f.unop)) (f.unop.op ≫ Quiver.Hom.op (pullback.snd f.unop f.unop))

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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsColimit (F := parallelPair (X := pullback f.unop f.unop) (pullback.fst f.unop f.unop) (pullback.snd f.unop f.unop))
    (Cofork.ofπ f.unop ⋯)
⊢ Eq.{v₁ + 1} (α :=
    Cone.pt.{0, v₁, 0, u₁} (F :=
        parallelPair (Y := Opposite.op (pullback f.unop f.unop)) (Quiver.Hom.op (pullback.fst f.unop f.unop))
          (Quiver.Hom.op (pullback.snd f.unop f.unop)))
        (ofι f.unop.op ⋯) ⟶
      Y)
    (Iso.hom
          (Iso.refl
            (Cone.pt.{0, v₁, 0, u₁} (F :=
              parallelPair (Y := Opposite.op (pullback f.unop f.unop)) (Quiver.Hom.op (pullback.fst f.unop f.unop))
                (Quiver.Hom.op (pullback.snd f.unop f.unop)))
              (ofι f.unop.op ⋯))) ≫
        ι (ofι f ⋯) :
      Cone.pt.{0, v₁, 0, u₁} (F :=
          parallelPair (Y := Opposite.op (pullback f.unop f.unop)) (Quiver.Hom.op (pullback.fst f.unop f.unop))
            (Quiver.Hom.op (pullback.snd f.unop f.unop)))
          (ofι f.unop.op ⋯) ⟶
        Y)
    (ι (ofι f.unop.op ⋯) ≫ Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) :
      Cone.pt.{0, v₁, 0, u₁} (F :=
          parallelPair (Y := Opposite.op (pullback f.unop f.unop)) (Quiver.Hom.op (pullback.fst f.unop f.unop))
            (Quiver.Hom.op (pullback.snd f.unop f.unop)))
          (ofι f.unop.op ⋯) ⟶
        Y)

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 : HasPushout.{v₁, u₁} (C := Cᵒᵖ) (X := X) (Y := Y) (Z := Y) f f
h :
  IsColimit (F := parallelPair (X := pullback f.unop f.unop) (pullback.fst f.unop f.unop) (pullback.snd f.unop f.unop))
    (Cofork.ofπ f.unop ⋯)
refine_1 :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inl f f)
    (Quiver.Hom.op (pullback.fst f.unop f.unop) ≫ Iso.hom (Iso.symm (pushoutIsoOpPullback f f)))
refine_2 :
  Eq (α := Opposite.op (Opposite.unop Y) ⟶ pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f)
    (Iso.hom (Iso.refl (Opposite.op (Opposite.unop Y))) ≫ pushout.inr f f)
    (Quiver.Hom.op (pullback.snd f.unop f.unop) ≫ Iso.hom (Iso.symm (pushoutIsoOpPullback f f)))
⊢ IsLimit.{0, v₁, 0, u₁} (C := Cᵒᵖ) (F :=
    parallelPair (X := Y) (Y := pushout.{v₁, u₁} (X := X) (Y := Y) (Z := Y) f f) (pushout.inl f f) (pushout.inr f f))
    (ofι f ⋯)

Tactic:
refine Fork.isLimitOfIsos _ (Cofork.isColimitOfπEquivIsLimitOp f.unop f.unop pullback.condition
      (by simp only [← op_comp, pullback.condition]) rfl h) _ (.refl _)
        ((pushoutIsoOpPullback f f).symm) (.refl _) ?_ ?_ (by simp)

Premises used: CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp, Quiver.Hom.unop, CategoryTheory.Iso.refl, CategoryTheory.Limits.Fork.isLimitOfIsos, CategoryTheory.Limits.pushoutIsoOpPullback, CategoryTheory.Iso.symm, CategoryTheory.Limits.pullback.condition, DFunLike.coe, rfl