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
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))

Tactic:
Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- 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
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : J),
    Eq (α := unop (F.rightOp.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
      (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))) ≫ c.π.app j))
⊢ m = Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))

Tactic:
refine Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- 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
c : Cone F.rightOp
hc : IsLimit c
s : Cocone F
m : (coconeOfConeRightOp c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeRightOp c).ι.app j ≫ m = s.ι.app j
j : J
⊢ Eq (α := unop (F.rightOp.obj j) ⟶ unop (op s.pt)) (Quiver.Hom.unop (m.op ≫ c.π.app j))
    (Quiver.Hom.unop (Quiver.Hom.op (Quiver.Hom.unop (hc.lift (coneRightOpOfCocone s))) ≫ c.π.app j))

Tactic:
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (op j)

Premises used: Quiver.Hom.op_unop, Opposite.op, CategoryTheory.Limits.IsLimit.fac
-- 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ᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
j : Jᵒᵖ
⊢ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeUnopOfCone s)) ≫ (coneOfCoconeUnop c).π.app j) = (s.π.app j).unop

Tactic:
simp
-- 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ᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j
⊢ m = Quiver.Hom.op (hc.desc (coconeUnopOfCone s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- 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ᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j
refine :
  ∀ (j : J),
    (c.ι.app j ≫ m.unop).op = Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeUnopOfCone s))))
⊢ m = Quiver.Hom.op (hc.desc (coconeUnopOfCone s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- 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ᵒᵖ
c : Cocone F.unop
hc : IsColimit c
s : Cone F
m : s.pt ⟶ (coneOfCoconeUnop c).pt
w : ∀ (j : Jᵒᵖ), m ≫ (coneOfCoconeUnop c).π.app j = s.π.app j
j : J
⊢ (c.ι.app j ≫ m.unop).op = Quiver.Hom.op (c.ι.app j ≫ Quiver.Hom.unop (Quiver.Hom.op (hc.desc (coconeUnopOfCone s))))

Tactic:
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (op j)

Premises used: CategoryTheory.Limits.IsColimit.fac, Quiver.Hom.unop_op, Opposite.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ᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
j : Jᵒᵖ
⊢ Quiver.Hom.unop ((coconeOfConeUnop c).ι.app j ≫ Quiver.Hom.op (hc.lift (coneUnopOfCocone s))) = (s.ι.app j).unop

Tactic:
simp
-- 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ᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
⊢ m = Quiver.Hom.op (hc.lift (coneUnopOfCocone s))

Tactic:
Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, CategoryTheory.Limits.IsLimit.hom_ext, Quiver.Hom.unop_inj
-- 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ᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
refine :
  ∀ (j : J),
    (m.unop ≫ c.π.app j).op = Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneUnopOfCocone s))) ≫ c.π.app j)
⊢ m = Quiver.Hom.op (hc.lift (coneUnopOfCocone s))

Tactic:
refine Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.unop_inj
-- 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ᵒᵖ
c : Cone F.unop
hc : IsLimit c
s : Cocone F
m : (coconeOfConeUnop c).pt ⟶ s.pt
w : ∀ (j : Jᵒᵖ), (coconeOfConeUnop c).ι.app j ≫ m = s.ι.app j
j : J
⊢ (m.unop ≫ c.π.app j).op = Quiver.Hom.op (Quiver.Hom.unop (Quiver.Hom.op (hc.lift (coneUnopOfCocone s))) ≫ c.π.app j)

Tactic:
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (op j)

Premises used: Quiver.Hom.unop_op, Opposite.op, CategoryTheory.Limits.IsLimit.fac
-- 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 : HasColimit F.leftOp
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := coneOfCoconeLeftOp (colimit.cocone F.leftOp)
      isLimit := isLimitConeOfCoconeLeftOp _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isLimitConeOfCoconeLeftOp, CategoryTheory.Limits.coneOfCoconeLeftOp, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Functor.leftOp
-- 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 : HasColimit F.op
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := (colimit.cocone F.op).unop
      isLimit := (colimit.isColimit _).unop }

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.Cocone.unop, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.IsColimit.unop, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasColimit F.rightOp
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := coneOfCoconeRightOp (colimit.cocone F.rightOp)
      isLimit := isLimitConeOfCoconeRightOp _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isLimitConeOfCoconeRightOp, CategoryTheory.Limits.coneOfCoconeRightOp, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Functor.rightOp, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasColimit F.unop
⊢ HasLimit F

Tactic:
HasLimit.mk
    { cone := coneOfCoconeUnop (colimit.cocone F.unop)
      isLimit := isLimitConeOfCoconeUnop _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.coneOfCoconeUnop, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.isLimitConeOfCoconeUnop, CategoryTheory.Functor.unop, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasColimit F
⊢ HasLimit F.op

Tactic:
HasLimit.mk
    { cone := (colimit.cocone F).op
      isLimit := (colimit.isColimit _).op }

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.op, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.Cocone.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ᵒᵖ
inst_2 : HasColimit F
⊢ HasLimit F.leftOp

Tactic:
HasLimit.mk
    { cone := coneLeftOpOfCocone (colimit.cocone F)
      isLimit := isLimitConeLeftOpOfCocone _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.isLimitConeLeftOpOfCocone, CategoryTheory.Limits.coneLeftOpOfCocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasColimit F
⊢ HasLimit F.rightOp

Tactic:
HasLimit.mk
    { cone := coneRightOpOfCocone (colimit.cocone F)
      isLimit := isLimitConeRightOpOfCocone _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.isLimitConeRightOpOfCocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk, CategoryTheory.Limits.coneRightOpOfCocone
-- 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 : HasColimit F
⊢ HasLimit F.unop

Tactic:
HasLimit.mk
    { cone := coneUnopOfCocone (colimit.cocone F)
      isLimit := isLimitConeUnopOfCocone _ (colimit.isColimit _) }

Premises used: CategoryTheory.Limits.coneUnopOfCocone, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.HasLimit.mk, CategoryTheory.Limits.isLimitConeUnopOfCocone, CategoryTheory.Limits.colimit.cocone, CategoryTheory.Limits.LimitCone.mk
-- 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 : HasColimit F
j : Jᵒᵖ
⊢ Eq (α := op (colimit F) ⟶ F.op.obj j) (Iso.inv (limitOpIsoOpColimit F) ≫ limit.π F.op j)
    (Quiver.Hom.op (colimit.ι F (unop j)))

Tactic:
simp [limitOpIsoOpColimit]

Premises used: CategoryTheory.Limits.limitOpIsoOpColimit
-- 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 : HasColimit F
j : J
⊢ Eq (α := limit F.op ⟶ op (F.obj j))
    (CategoryStruct.comp (Y := op (colimit F)) (Iso.hom (limitOpIsoOpColimit F)) (Quiver.Hom.op (colimit.ι F j)) :
      limit F.op ⟶ op (F.obj j))
    (limit.π F.op (op j) : limit F.op ⟶ F.op.obj (op j))

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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 : HasColimit F
j : Jᵒᵖ
⊢ Eq (α := unop (colimit F) ⟶ F.leftOp.obj j) (Iso.inv (limitLeftOpIsoUnopColimit F) ≫ limit.π F.leftOp j)
    (Quiver.Hom.unop (colimit.ι F (unop j)))

Tactic:
simp [limitLeftOpIsoUnopColimit]

Premises used: CategoryTheory.Limits.limitLeftOpIsoUnopColimit
-- 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 : HasColimit F
j : J
⊢ Eq (α := limit F.leftOp ⟶ unop (F.obj j))
    (CategoryStruct.comp (Y := unop (colimit F)) (Iso.hom (limitLeftOpIsoUnopColimit F))
        (Quiver.Hom.unop (colimit.ι F j)) :
      limit F.leftOp ⟶ unop (F.obj j))
    (limit.π F.leftOp (op j) : limit F.leftOp ⟶ F.leftOp.obj (op j))

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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 : HasColimit F
j : J
⊢ Eq (α := op (colimit F) ⟶ F.rightOp.obj j) (Iso.inv (limitRightOpIsoOpColimit F) ≫ limit.π F.rightOp j)
    (Quiver.Hom.op (colimit.ι F (op j)))

Tactic:
simp [limitRightOpIsoOpColimit]

Premises used: CategoryTheory.Limits.limitRightOpIsoOpColimit
-- 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 : HasColimit F
j : Jᵒᵖ
⊢ Eq (α := limit F.rightOp ⟶ op (F.obj j))
    (CategoryStruct.comp (Y := op (colimit F)) (Iso.hom (limitRightOpIsoOpColimit F)) (Quiver.Hom.op (colimit.ι F j)) :
      limit F.rightOp ⟶ op (F.obj j))
    (limit.π F.rightOp (unop j) : limit F.rightOp ⟶ F.rightOp.obj (unop j))

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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 : HasColimit F
j : J
⊢ Eq (α := unop (colimit F) ⟶ F.unop.obj j) (Iso.inv (limitUnopIsoUnopColimit F) ≫ limit.π F.unop j)
    (Quiver.Hom.unop (colimit.ι F (op j)))

Tactic:
simp [limitUnopIsoUnopColimit]

Premises used: CategoryTheory.Limits.limitUnopIsoUnopColimit
-- 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 : HasColimit F
j : Jᵒᵖ
⊢ Eq (α := limit F.unop ⟶ unop (F.obj j))
    (CategoryStruct.comp (Y := unop (colimit F)) (Iso.hom (limitUnopIsoUnopColimit F))
        (Quiver.Hom.unop (colimit.ι F j)) :
      limit F.unop ⟶ unop (F.obj j))
    (limit.π F.unop (unop j) : limit F.unop ⟶ F.unop.obj (unop j))

Tactic:
simp [← Iso.eq_inv_comp]

Premises used: CategoryTheory.Iso.eq_inv_comp
-- 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 : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ C
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J Cᵒᵖ

Tactic:
{ has_limit := fun F => hasLimit_of_hasColimit_leftOp F }

Premises used: CategoryTheory.Limits.HasLimitsOfShape.mk, CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp
-- 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 : HasColimitsOfShape.{v₂, u₂, v₁, u₁} Jᵒᵖ Cᵒᵖ
⊢ HasLimitsOfShape.{v₂, u₂, v₁, u₁} J C

Tactic:
{ has_limit := fun F => hasLimit_of_hasColimit_op F }

Premises used: CategoryTheory.Limits.hasLimit_of_hasColimit_op, CategoryTheory.Limits.HasLimitsOfShape.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 : HasColimitsOfSize.{v₂, u₂, v₁, u₁} C
⊢ HasLimitsOfSize.{v₂, u₂, v₁, u₁} Cᵒᵖ

Tactic:
⟨fun _ => inferInstance⟩

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

Tactic:
{ has_limits_of_shape := fun _ _ => hasLimitsOfShape_of_hasColimitsOfShape_op }

Premises used: CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op, CategoryTheory.Limits.HasLimitsOfSize.mk
-- 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.leftOp
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := coconeOfConeLeftOp (limit.cone F.leftOp)
      isColimit := isColimitCoconeOfConeLeftOp _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.coconeOfConeLeftOp, CategoryTheory.Limits.isColimitCoconeOfConeLeftOp, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Functor.leftOp
-- 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.op
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := (limit.cone F.op).unop
      isColimit := (limit.isLimit _).unop }

Premises used: CategoryTheory.Functor.op, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.IsLimit.unop, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.Cone.unop
-- 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.rightOp
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := coconeOfConeRightOp (limit.cone F.rightOp)
      isColimit := isColimitCoconeOfConeRightOp _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.isColimitCoconeOfConeRightOp, CategoryTheory.Limits.coconeOfConeRightOp, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Functor.rightOp
-- 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.unop
⊢ HasColimit F

Tactic:
HasColimit.mk
    { cocone := coconeOfConeUnop (limit.cone F.unop)
      isColimit := isColimitCoconeOfConeUnop _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.coconeOfConeUnop, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Functor.unop, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isColimitCoconeOfConeUnop
-- 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
⊢ HasColimit F.op

Tactic:
HasColimit.mk
    { cocone := (limit.cone F).op
      isColimit := (limit.isLimit _).op }

Premises used: CategoryTheory.Limits.IsLimit.op, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.Cone.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ᵒᵖ
inst_2 : HasLimit F
⊢ HasColimit F.leftOp

Tactic:
HasColimit.mk
    { cocone := coconeLeftOpOfCone (limit.cone F)
      isColimit := isColimitCoconeLeftOpOfCone _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.isColimitCoconeLeftOpOfCone, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.coconeLeftOpOfCone
-- 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
⊢ HasColimit F.rightOp

Tactic:
HasColimit.mk
    { cocone := coconeRightOpOfCone (limit.cone F)
      isColimit := isColimitCoconeRightOpOfCone _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.isColimitCoconeRightOpOfCone, CategoryTheory.Limits.coconeRightOpOfCone, CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk
-- 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
⊢ HasColimit F.unop

Tactic:
HasColimit.mk
    { cocone := coconeUnopOfCone (limit.cone F)
      isColimit := isColimitCoconeUnopOfCone _ (limit.isLimit _) }

Premises used: CategoryTheory.Limits.limit.cone, CategoryTheory.Limits.HasColimit.mk, CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.ColimitCocone.mk, CategoryTheory.Limits.isColimitCoconeUnopOfCone, CategoryTheory.Limits.coconeUnopOfCone
-- 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.op.obj j ⟶ op (limit F)) (colimit.ι F.op j ≫ Iso.hom (colimitOpIsoOpLimit F))
    (Quiver.Hom.op (limit.π F (unop j)))

Tactic:
simp [colimitOpIsoOpLimit]

Premises used: CategoryTheory.Limits.colimitOpIsoOpLimit
-- 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.op)
    (CategoryStruct.comp (Y := op (limit F)) (Quiver.Hom.op (limit.π F j)) (Iso.inv (colimitOpIsoOpLimit F)) :
      op (F.obj j) ⟶ colimit F.op)
    (colimit.ι F.op (op j) : F.op.obj (op j) ⟶ colimit F.op)

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.leftOp.obj j ⟶ unop (limit F)) (colimit.ι F.leftOp j ≫ Iso.hom (colimitLeftOpIsoUnopLimit F))
    (Quiver.Hom.unop (limit.π F (unop j)))

Tactic:
simp [colimitLeftOpIsoUnopLimit]

Premises used: CategoryTheory.Limits.colimitLeftOpIsoUnopLimit
-- 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.leftOp)
    (CategoryStruct.comp (Y := unop (limit F)) (Quiver.Hom.unop (limit.π F j)) (Iso.inv (colimitLeftOpIsoUnopLimit F)) :
      unop (F.obj j) ⟶ colimit F.leftOp)
    (colimit.ι F.leftOp (op j) : F.leftOp.obj (op j) ⟶ colimit F.leftOp)

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.rightOp.obj j ⟶ op (limit F)) (colimit.ι F.rightOp j ≫ Iso.hom (colimitRightOpIsoUnopLimit F))
    (Quiver.Hom.op (limit.π F (op j)))

Tactic:
simp [colimitRightOpIsoUnopLimit]

Premises used: CategoryTheory.Limits.colimitRightOpIsoUnopLimit