awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
inst_2 : HasLimit F
j : Jᵒᵖ
⊢ Eq (α := op (F.obj j) ⟶ colimit F.rightOp)
    (CategoryStruct.comp (Y := op (limit F)) (Quiver.Hom.op (limit.π F j)) (Iso.inv (colimitRightOpIsoUnopLimit F)) :
      op (F.obj j) ⟶ colimit F.rightOp)
    (colimit.ι F.rightOp (unop j) : F.rightOp.obj (unop j) ⟶ colimit F.rightOp)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
inst_2 : HasLimit F
j : J
⊢ Eq (α := F.unop.obj j ⟶ unop (limit F)) (colimit.ι F.unop j ≫ Iso.hom (colimitUnopIsoOpLimit F))
    (Quiver.Hom.unop (limit.π F (op j)))

Tactic:
simp [colimitUnopIsoOpLimit]

Premises used: CategoryTheory.Limits.colimitUnopIsoOpLimit
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ Cᵒᵖ
inst_2 : HasLimit F
j : Jᵒᵖ
⊢ Eq (α := unop (F.obj j) ⟶ colimit F.unop)
    (CategoryStruct.comp (Y := unop (limit F)) (Quiver.Hom.unop (limit.π F j)) (Iso.inv (colimitUnopIsoOpLimit F)) :
      unop (F.obj j) ⟶ colimit F.unop)
    (colimit.ι F.unop (unop j) : F.unop.obj (unop j) ⟶ colimit F.unop)

Tactic:
simp [Iso.comp_inv_eq]

Premises used: CategoryTheory.Iso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
{ has_colimit := fun F => hasColimit_of_hasLimit_op F }

Premises used: CategoryTheory.Limits.HasColimitsOfShape.mk, CategoryTheory.Limits.hasColimit_of_hasLimit_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasLimitsOfSize.{v₂, u₂, v₁, u₁} C
⊢ HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ
⊢ HasColimitsOfSize.{v₂, u₂, v₁, u₁} C

Tactic:
{ has_colimits_of_shape := fun _ _ => hasColimitsOfShape_of_hasLimitsOfShape_op }

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op, CategoryTheory.Limits.HasColimitsOfSize.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasColimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ ↔ HasLimitsOfSize.{v₂, u₂, v₁, u₁} C

Tactic:
⟨fun _ ↦ hasLimits_of_hasColimits_op, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.hasLimits_of_hasColimits_op, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ ↔ HasColimitsOfSize.{v₂, u₂, v₁, u₁} C

Tactic:
⟨fun _ ↦ hasColimits_of_hasLimits_op, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Limits.hasColimits_of_hasLimits_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteLimits.{v₁, u₁} C
⊢ HasFiniteColimits.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun _ _ _ => hasColimitsOfShape_op_of_hasLimitsOfShape⟩

Premises used: CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteColimits.{v₁, u₁} C
⊢ HasFiniteLimits.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun _ _ _ => hasLimitsOfShape_op_of_hasColimitsOfShape⟩

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteLimits.{v₁, u₁} Cᵒᵖ ↔ HasFiniteColimits.{v₁, u₁} C

Tactic:
⟨fun _ ↦ ⟨fun _ _ _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op⟩, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op, Iff.intro, CategoryTheory.Limits.HasFiniteColimits.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasFiniteColimits.{v₁, u₁} Cᵒᵖ ↔ HasFiniteLimits.{v₁, u₁} C

Tactic:
⟨fun _ ↦ ⟨fun _ _ _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op⟩, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op, inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J C
⊢ HasColimit F.op ↔ HasLimit F

Tactic:
⟨fun _ ↦ hasLimit_of_hasColimit_op F, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Limits.hasLimit_of_hasColimit_op, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
⊢ HasColimit F.leftOp ↔ HasLimit F

Tactic:
⟨fun _ ↦ hasLimit_of_hasColimit_leftOp F, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
⊢ HasColimit F.rightOp ↔ HasLimit F

Tactic:
⟨fun _ ↦ hasLimit_of_hasColimit_rightOp F, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J C
⊢ HasLimit F.op ↔ HasColimit F

Tactic:
⟨fun _ ↦ hasColimit_of_hasLimit_op F, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Limits.hasColimit_of_hasLimit_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} J Cᵒᵖ
⊢ HasLimit F.leftOp ↔ HasColimit F

Tactic:
⟨fun _ ↦ hasColimit_of_hasLimit_leftOp F, fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp, inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
F : Functor.{v₂, v₁, u₂, u₁} Jᵒᵖ C
⊢ HasLimit F.rightOp ↔ HasColimit F

Tactic:
⟨fun _ ↦ hasColimit_of_hasLimit_rightOp F, fun _ ↦ inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
refine : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ → HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ

Tactic:
have : HasLimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
hasColimitsOfShape_of_hasLimitsOfShape_op

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
exact hasColimitsOfShape_of_hasLimitsOfShape_op

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
refine : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ → HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ

Tactic:
have : HasColimitsOfShape Jᵒᵖᵒᵖ Cᵒᵖ := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
hasLimitsOfShape_of_hasColimitsOfShape_op

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ
this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C

Tactic:
exact hasLimitsOfShape_of_hasColimitsOfShape_op

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
refine : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C → HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
refine ⟨fun _ ↦ hasColimitsOfShape_of_hasLimitsOfShape_op, fun _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C

Tactic:
have : HasColimitsOfShape Jᵒᵖᵒᵖ C := hasColimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C
this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ

Tactic:
hasLimitsOfShape_op_of_hasColimitsOfShape

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasColimitsOfShape.{v₂, u₂, v₁, u₁} J C
this : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ

Tactic:
exact hasLimitsOfShape_op_of_hasColimitsOfShape

Premises used: CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
⟨fun _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op, fun _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
refine : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C → HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ ↔ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
refine ⟨fun _ ↦ hasLimitsOfShape_of_hasColimitsOfShape_op, fun _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C

Tactic:
have : HasLimitsOfShape Jᵒᵖᵒᵖ C := hasLimitsOfShape_of_equivalence (opOpEquivalence J).symm
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C
this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ

Tactic:
hasColimitsOfShape_op_of_hasLimitsOfShape

Premises used: CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
h : HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C
this : HasLimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖᵒᵖ C
⊢ HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ

Tactic:
exact hasColimitsOfShape_op_of_hasLimitsOfShape

Premises used: CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePullbacks.{w, v₁, u₁} C
ι : Type w
rw : HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ C
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) Cᵒᵖ

Tactic:
rw [hasColimitsOfShape_opposite_iff]

Premises used: CategoryTheory.Limits.hasColimitsOfShape_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePullbacks.{w, v₁, u₁} C
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ C

Tactic:
hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePullbacks.{w, v₁, u₁} C
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ C

Tactic:
exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePushouts.{w, v₁, u₁} C
ι : Type w
rw : HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ C
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) Cᵒᵖ

Tactic:
rw [hasLimitsOfShape_opposite_iff]

Premises used: CategoryTheory.Limits.hasLimitsOfShape_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePushouts.{w, v₁, u₁} C
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ C

Tactic:
hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasWidePushouts.{w, v₁, u₁} C
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ C

Tactic:
exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePushouts.{w, v₁, u₁} C

Tactic:
⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
refine : ∀ (h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ) (ι : Type w), HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) C
⊢ HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePushouts.{w, v₁, u₁} C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ
ι : Type w
rw : HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ Cᵒᵖ
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι) C

Tactic:
rw [← hasLimitsOfShape_opposite_opposite_iff]

Premises used: CategoryTheory.Limits.hasLimitsOfShape_opposite_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ Cᵒᵖ

Tactic:
hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePullbacks.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePushoutShape ι)ᵒᵖ Cᵒᵖ

Tactic:
exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
⊢ HasWidePushouts.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePullbacks.{w, v₁, u₁} C

Tactic:
⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
refine : ∀ (h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ) (ι : Type w), HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) C
⊢ HasWidePushouts.{w, v₁, u₁} Cᵒᵖ ↔ HasWidePullbacks.{w, v₁, u₁} C

Tactic:
refine ⟨fun h ι ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ
ι : Type w
rw : HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι) C

Tactic:
rw [← hasColimitsOfShape_opposite_opposite_iff]

Premises used: CategoryTheory.Limits.hasColimitsOfShape_opposite_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ Cᵒᵖ

Tactic:
hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : HasWidePushouts.{w, v₁, u₁} Cᵒᵖ
ι : Type w
⊢ HasColimitsOfShape.{w, w, v₁, u₁} (WidePullbackShape ι)ᵒᵖ Cᵒᵖ

Tactic:
exact hasColimitsOfShape_of_equivalence (widePullbackShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasColimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePullbackShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun J _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.HasFiniteWidePushouts.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
refine : ∀ (J : Type), Finite J → HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) Cᵒᵖ
⊢ HasFiniteWidePushouts.{v₁, u₁} Cᵒᵖ

Tactic:
refine ⟨fun J _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
J : Type
h : Finite J
rw : HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ C
⊢ HasColimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J) Cᵒᵖ

Tactic:
rw [hasColimitsOfShape_opposite_iff]

Premises used: CategoryTheory.Limits.hasColimitsOfShape_opposite_iff
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ C

Tactic:
hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePullbacks.{v₁, u₁} C
J : Type
h : Finite J
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePushoutShape J)ᵒᵖ C

Tactic:
exact hasLimitsOfShape_of_equivalence (widePushoutShapeOpEquiv _).symm

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Limits.widePushoutShapeOpEquiv
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ

Tactic:
⟨fun J _ ↦ ?_⟩

Premises used: CategoryTheory.Limits.HasFiniteWidePullbacks.mk
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J : Type u₂
inst_1 : Category.{v₂, u₂} J
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
refine : ∀ (J : Type), Finite J → HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) Cᵒᵖ
⊢ HasFiniteWidePullbacks.{v₁, u₁} Cᵒᵖ

Tactic:
refine ⟨fun J _ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Limits.Opposites
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
J_1 : Type u₂
inst_1 : Category.{v₂, u₂} J_1
inst_2 : HasFiniteWidePushouts.{v₁, u₁} C
J : Type
h : Finite J
rw : HasColimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J)ᵒᵖ C
⊢ HasLimitsOfShape.{0, 0, v₁, u₁} (WidePullbackShape J) Cᵒᵖ

Tactic:
rw [hasLimitsOfShape_opposite_iff]

Premises used: CategoryTheory.Limits.hasLimitsOfShape_opposite_iff