awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : ObjectProperty.Small.{w, v_1, u_1} P
inst_5 : LocallySmall.{w, v_1, u_1} C
inst_6 : Small.{w, u'} J
inst_7 : LocallySmall.{w, v', u'} J
F : Functor.{v', v_1, u', u_1} J C
inst_8 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ HasColimit (P.lift F hF ⋙ P.ι)

Tactic:
assumption
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : ObjectProperty.Small.{w, v_1, u_1} P
inst_5 : LocallySmall.{w, v_1, u_1} C
inst_6 : Small.{w, u'} J
inst_7 : LocallySmall.{w, v', u'} J
F : Functor.{v', v_1, u', u_1} J C
inst_8 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ ∃ (a : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasColimit (F ⋙ P.ι) }),
    (fun (F : { F : Functor.{v', v_1, u', u_1} J P.FullSubcategory // HasColimit (F ⋙ P.ι) }) ↦
          (Subtype.mk (p := strictColimitsOfShape.{v', u', v_1, u_1} P J) (colimit ((↑F : J ⥤ P.FullSubcategory) ⋙ P.ι))
              ⋯ :
            Subtype (strictColimitsOfShape.{v', u', v_1, u_1} P J)))
        a =
      Subtype.mk (p := strictColimitsOfShape.{v', u', v_1, u_1} P J) (colimit F) ⋯

Tactic:
exact ⟨⟨P.lift F hF, by assumption⟩, rfl⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
rw : P.isoClosure
| P

Tactic:
rw [← P.isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
conv_rhs : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure
⊢ colimitsOfShape.{v', u', v_1, u_1} P J ≤ P

Tactic:
conv_rhs => rw [← P.isoClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.isoClosure_eq_self
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
rw : (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure
⊢ colimitsOfShape.{v', u', v_1, u_1} P J ≤ P.isoClosure

Tactic:
rw [← isoClosure_strictColimitsOfShape]

Premises used: CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure

Tactic:
monotone_isoClosure h

Premises used: CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : P.IsClosedUnderIsomorphisms
h : strictColimitsOfShape.{v', u', v_1, u_1} P J ≤ P
⊢ (strictColimitsOfShape.{v', u', v_1, u_1} P J).isoClosure ≤ P.isoClosure

Tactic:
exact monotone_isoClosure h

Premises used: CategoryTheory.ObjectProperty.monotone_isoClosure
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
inst_4 : Nonempty J
rw rw₁ : LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) ⊥ ⊥
⊢ LE.le.{u_1} (α := ObjectProperty.{v_1, u_1} C) (colimitsOfShape.{v', u', v_1, u_1} ⊥ J) ⊥

Tactic:
rw [colimitsOfShape_bot]

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape_bot
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
x : C
h : colimitsOfShape.{v', u', v_1, u_1} ⊤ J x
⊢ ⊤ x

Tactic:
trivial
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J
X : C
h : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ P X

Tactic:
P.colimitsOfShape_le J _ ⟨h⟩

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le, Nonempty.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J
F : Functor.{v', v_1, u', u_1} J C
c : Cocone F
hc : IsColimit c
hF : ∀ (j : J), P (F.obj j)
⊢ P c.pt

Tactic:
P.colimitsOfShape_le J _ ⟨{ diag := _, ι := _, isColimit := hc, prop_diag_obj := hF }⟩

Premises used: CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le, CategoryTheory.Limits.ColimitPresentation.mk, Nonempty.intro, CategoryTheory.Limits.Cocone.ι, CategoryTheory.ObjectProperty.ColimitOfShape.mk
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
inst_2 : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J
F : Functor.{v', v_1, u', u_1} J C
inst_3 : HasColimit F
hF : ∀ (j : J), P (F.obj j)
⊢ P (colimit F)

Tactic:
P.prop_of_isColimit (colimit.isColimit F) hF

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.ObjectProperty.prop_of_isColimit
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
G : Functor.{v', v'', u', u''} J J'
inst_3 : G.Final
⊢ colimitsOfShape.{v'', u'', v_1, u_1} P J' ≤ colimitsOfShape.{v', u', v_1, u_1} P J

Tactic:
fun _h ⟨h⟩ ↦ ⟨h.reindex G⟩

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.reindex, CategoryTheory.ObjectProperty.colimitsOfShape, Nonempty.intro, _private.0.CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape.match_1
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
⊢ colimitsOfShape.{v', u', v_1, u_1} P J = colimitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
le_antisymm (P.colimitsOfShape_le_of_final e.inverse)
    (P.colimitsOfShape_le_of_final e.functor)

Premises used: CategoryTheory.ObjectProperty.colimitsOfShape_le_of_final, CategoryTheory.Equivalence.functor, le_antisymm, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
simp [isClosedUnderColimitsOfShape_iff, P.colimitsOfShape_congr e]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.colimitsOfShape_congr
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
J' : Type u''
inst_2 : Category.{v'', u''} J'
e : Equivalence.{v', v'', u', u''} J J'
inst_3 rwa rwa₁ rwa₂ rwa₃ : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J
⊢ IsClosedUnderColimitsOfShape.{v'', u'', v_1, u_1} P J'

Tactic:
rwa [← P.isClosedUnderColimitsOfShape_iff_of_equivalence e]

Premises used: CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_of_equivalence
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
P_1 : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_2 : Category.{v', u'} J
J' : Type u''
inst_3 : Category.{v'', u''} J'
P : ObjectProperty.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J
inst_5 : PreservesColimitsOfShape.{v', u', v_1, v_2, u_1, u_2} J F
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage F) J

Tactic:
⟨fun _ ⟨c, H⟩ ↦ ColimitOfShape.prop (P := P) ⟨c.map F, H⟩⟩

Premises used: CategoryTheory.ObjectProperty.ColimitOfShape.prop, _private.0.CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.inverseImage.match_1, CategoryTheory.Limits.ColimitPresentation.map, CategoryTheory.ObjectProperty.ColimitOfShape.mk, CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk, CategoryTheory.ObjectProperty.inverseImage
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J

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

Premises used: inferInstance, Iff.intro
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
refine :
  ∀ (H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J),
    IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J ↔
    IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ inferInstance⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
⊢ IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} ((P.inverseImage e.functor).inverseImage e.inverse) J

Tactic:
(inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderColimitsOfShape J)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
h : P = (P.inverseImage e.functor).inverseImage e.inverse
⊢ IsClosedUnderColimitsOfShape.{v', u', v_2, u_2} P J

Tactic:
convert!
    (inferInstance :
      ((P.inverseImage e.functor).inverseImage e.inverse).IsClosedUnderColimitsOfShape J)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
h : ∀ (X : D), P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X
⊢ P = (P.inverseImage e.functor).inverseImage e.inverse

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
J : Type u'
inst_2 : Category.{v', u'} J
P : ObjectProperty.{v_2, u_2} D
inst_3 : P.IsClosedUnderIsomorphisms
e : Equivalence.{v_1, v_2, u_1, u_2} C D
H : IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} (P.inverseImage e.functor) J
X : D
⊢ P X ↔ (P.inverseImage e.functor).inverseImage e.inverse X

Tactic:
simpa using P.prop_iff_of_iso (e.counitIso.app X).symm

Premises used: CategoryTheory.ObjectProperty.prop_iff_of_iso, CategoryTheory.Iso.symm, CategoryTheory.Iso.app, CategoryTheory.Equivalence.counitIso
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
h :
  ∀ (X : C),
    colimitsOfShape.{v', u', v_1, u_1} P J X ↔
      ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J = ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X

Tactic:
⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩

Premises used: Opposite, CategoryTheory.ObjectProperty.colimitsOfShape, CategoryTheory.ObjectProperty.unop, Nonempty.intro, _private.0.CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShape.match_1, Iff.intro, CategoryTheory.ObjectProperty.limitsOfShape, _private.0.CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape.match_1, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h :
  colimitsOfShape.{v', u', v_1, u_1} P J X →
    (h : ColimitOfShape.{v', u', v_1, u_1} P J X) → LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
h₁ :
  ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X →
    (h : LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)) → ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ colimitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X

Tactic:
refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : colimitsOfShape.{v', u', v_1, u_1} P J X
h : ColimitOfShape.{v', u', v_1, u_1} P J X
⊢ LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)

Tactic:
exact
      { diag := h.diag.op
        π := NatTrans.op h.ι
        isLimit := isLimitOfUnop h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.unop.{v_1, u_1} (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
h : LimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
⊢ ColimitOfShape.{v', u', v_1, u_1} P J X

Tactic:
exact
      { diag := h.diag.unop
        ι := NatTrans.unop h.π
        isColimit := isColimitOfOp h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
h :
  ∀ (X : C),
    limitsOfShape.{v', u', v_1, u_1} P J X ↔
      ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
⊢ limitsOfShape.{v', u', v_1, u_1} P J = ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X

Tactic:
⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩

Premises used: Opposite, CategoryTheory.ObjectProperty.colimitsOfShape, CategoryTheory.ObjectProperty.unop, _private.0.CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape.match_2, Nonempty.intro, _private.0.CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape.match_1, Iff.intro, CategoryTheory.ObjectProperty.limitsOfShape, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h :
  limitsOfShape.{v', u', v_1, u_1} P J X →
    (h : LimitOfShape.{v', u', v_1, u_1} P J X) → ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
h₁ :
  ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X →
    (h : ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)) → LimitOfShape.{v', u', v_1, u_1} P J X
⊢ limitsOfShape.{v', u', v_1, u_1} P J X ↔
    ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X

Tactic:
refine ⟨fun ⟨h⟩ => ⟨?_⟩, fun ⟨h⟩ => ⟨?_⟩⟩
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : limitsOfShape.{v', u', v_1, u_1} P J X
h : LimitOfShape.{v', u', v_1, u_1} P J X
⊢ ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)

Tactic:
exact
      { diag := h.diag.op
        ι := NatTrans.op h.π
        isColimit := isColimitOfUnop h.isLimit
        prop_diag_obj _ := h.prop_diag_obj _ }
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
X : C
h_1 : ObjectProperty.unop.{v_1, u_1} (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) X
h : ColimitOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ (Opposite.op X)
⊢ LimitOfShape.{v', u', v_1, u_1} P J X

Tactic:
exact
      { diag := h.diag.unop
        π := NatTrans.unop h.ι
        isLimit := isLimitOfOp h.isColimit
        prop_diag_obj _ := h.prop_diag_obj _ }
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
rw₁ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
rw₂ rw₃ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (limitsOfShape.{v', u', v_1, u_1} P.op J)
    (limitsOfShape.{v', u', v_1, u_1} P.op J)
⊢ limitsOfShape.{v', u', v_1, u_1} P.op J = (colimitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op

Tactic:
rw [colimitsOfShape_eq_unop_limitsOfShape, op_unop,
    P.op.limitsOfShape_congr (opOpEquivalence J)]

Premises used: CategoryTheory.opOpEquivalence, CategoryTheory.ObjectProperty.limitsOfShape_congr, CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShape, CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.op
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
rw :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)))
rw₁ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖᵒᵖ)
rw₂ rw₃ :
  Eq (α := ObjectProperty.{v_1, u_1} Cᵒᵖ) (colimitsOfShape.{v', u', v_1, u_1} P.op J)
    (colimitsOfShape.{v', u', v_1, u_1} P.op J)
⊢ colimitsOfShape.{v', u', v_1, u_1} P.op J = (limitsOfShape.{v', u', v_1, u_1} P Jᵒᵖ).op

Tactic:
rw [limitsOfShape_eq_unop_colimitsOfShape, op_unop,
    P.op.colimitsOfShape_congr (opOpEquivalence J)]

Premises used: CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape, CategoryTheory.opOpEquivalence, CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.op, CategoryTheory.ObjectProperty.colimitsOfShape_congr
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
rw : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ
rw₁ : colimitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₃ :
  ObjectProperty.op (ObjectProperty.unop (limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
    limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₄ rw₅ : limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op ↔ limitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ

Tactic:
rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    colimitsOfShape_eq_unop_limitsOfShape, ← op_monotone_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.colimitsOfShape_eq_unop_limitsOfShape, CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff
-- Module: Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
P : ObjectProperty.{v_1, u_1} C
J : Type u'
inst_1 : Category.{v', u'} J
rw : IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₁ : limitsOfShape.{v', u', v_1, u_1} P J ≤ P ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₂ :
  ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ) ≤ P ↔
    colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₃ :
  ObjectProperty.op (ObjectProperty.unop (colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ)) ≤ P.op ↔
    colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
rw₄ rw₅ : colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op ↔ colimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ ≤ P.op
⊢ IsClosedUnderLimitsOfShape.{v', u', v_1, u_1} P J ↔ IsClosedUnderColimitsOfShape.{v', u', v_1, u_1} P.op Jᵒᵖ

Tactic:
rw [isClosedUnderColimitsOfShape_iff, isClosedUnderLimitsOfShape_iff,
    limitsOfShape_eq_unop_colimitsOfShape, ← op_monotone_iff, op_unop]

Premises used: CategoryTheory.ObjectProperty.op_monotone_iff, CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff, CategoryTheory.ObjectProperty.limitsOfShape_eq_unop_colimitsOfShape, CategoryTheory.ObjectProperty.op_unop, CategoryTheory.ObjectProperty.isClosedUnderLimitsOfShape_iff