awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type w
inst_3 : SmallCategory J
inst_4 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
(coyoneda.obj (op X)).preservesColimitsOfShape_of_isCardinalAccessible κ J

Premises used: CategoryTheory.coyoneda, Opposite.op, CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₃
inst_3 : Category.{v₃, u₃} J
inst_4 : EssentiallySmall.{w, v₃, u₃} J
inst_5 : IsCardinalFiltered.{w, v₃, u₃} J κ
⊢ PreservesColimitsOfShape.{v₃, u₃, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
(coyoneda.obj (op X)).preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall κ J

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ'

Tactic:
(coyoneda.obj (op X)).isCardinalAccessible_of_le h

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.isCardinalAccessible_of_le, Opposite.op, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
κ' : Cardinal.{w}
inst_2 : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : isCardinalPresentable.{w, v₁, u₁} C κ X
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ

Tactic:
rw [isCardinalPresentable_iff] at hX ⊢

Premises used: CategoryTheory.isCardinalPresentable_iff
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
κ' : Cardinal.{w}
inst_2 : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ'

Tactic:
isCardinalPresentable_of_le _ h

Premises used: CategoryTheory.isCardinalPresentable_of_le
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
κ' : Cardinal.{w}
inst_2 : Fact κ'.IsRegular
h : κ ≤ κ'
X : C
hX : IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ'

Tactic:
exact isCardinalPresentable_of_le _ h

Premises used: CategoryTheory.isCardinalPresentable_of_le
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X Y : C
e : X ≅ Y
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ IsCardinalPresentable.{w, v₁, u₁} Y κ

Tactic:
Functor.isCardinalAccessible_of_natIso (coyoneda.mapIso e.symm.op) κ

Premises used: CategoryTheory.coyoneda, CategoryTheory.Functor.isCardinalAccessible_of_natIso, CategoryTheory.Iso.op, CategoryTheory.Iso.symm, CategoryTheory.Functor.mapIso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e_1 : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X_1 Y_1 : C
e : X_1 ≅ Y_1
hX : isCardinalPresentable.{w, v₁, u₁} C κ X_1
⊢ IsCardinalPresentable.{w, v₁, u₁} X_1 κ

Tactic:
rw [isCardinalPresentable_iff] at hX ⊢

Premises used: CategoryTheory.isCardinalPresentable_iff
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e_1 : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X_1 Y_1 : C
e : X_1 ≅ Y_1
hX : IsCardinalPresentable.{w, v₁, u₁} X_1 κ
⊢ IsCardinalPresentable.{w, v₁, u₁} Y_1 κ

Tactic:
isCardinalPresentable_of_iso e _

Premises used: CategoryTheory.isCardinalPresentable_of_iso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e_1 : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X_1 Y_1 : C
e : X_1 ≅ Y_1
hX : IsCardinalPresentable.{w, v₁, u₁} X_1 κ
⊢ IsCardinalPresentable.{w, v₁, u₁} Y_1 κ

Tactic:
exact isCardinalPresentable_of_iso e _

Premises used: CategoryTheory.isCardinalPresentable_of_iso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
⊢ IsCardinalPresentable.{w, v₃, u₃} (e.functor.obj X) κ

Tactic:
⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩

Premises used: CategoryTheory.Functor.IsCardinalAccessible.mk, CategoryTheory.Limits.PreservesColimitsOfShape.mk
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
refine :
  ∀ (J : Type w) (x : SmallCategory J),
    IsCardinalFiltered J κ →
      ∀ {Y : Functor.{w, v₃, w, u₃} J C'}, PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)))
⊢ IsCardinalPresentable.{w, v₃, u₃} (e.functor.obj X) κ

Tactic:
refine ⟨fun J _ _ ↦ ⟨fun {Y} ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
⊢ PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable X κ J
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
suffices : PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)))

Tactic:
suffices PreservesColimit Y (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) from
    ⟨fun {c} hc ↦ ⟨isColimitOfReflects uliftFunctor.{v₁}
        (isColimitOfPreserves (coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁}) hc)⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
X_1 : C'
_ :
  ∀ {Y : C'} (f : X_1 ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) X_1 ⟶
        (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).obj Y)
      (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
        Iso.hom
          ((fun (Z : C') ↦
              (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
            Y))
      (Iso.hom
          ((fun (Z : C') ↦
              (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
            X_1) ≫
        (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)
⊢ ∀ {Y : C'} (f : X_1 ⟶ Y),
    Eq (α :=
      Functor.obj (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) X_1 ⟶
        (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).obj Y)
      (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
        Iso.hom
          ((fun (Z : C') ↦
              (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
            Y))
      (Iso.hom
          ((fun (Z : C') ↦
              (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
            X_1) ≫
        (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
X_1 Y_1 : C'
f : X_1 ⟶ Y_1
h :
  ∀ (g : Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1),
    TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
            Iso.hom
              ((fun (Z : C') ↦
                  (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
                Y_1)))
        { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) } =
      TypeCat.Fun.toFun
        (ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
              ((fun (Z : C') ↦
                  (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
                X_1) ≫
            (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f))
        { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) }
⊢ Eq (α :=
    Functor.obj (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) X_1 ⟶
      (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).obj Y_1)
    (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
      Iso.hom
        ((fun (Z : C') ↦ (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
          Y_1))
    (Iso.hom
        ((fun (Z : C') ↦ (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
          X_1) ≫
      (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f)

Tactic:
ext ⟨g⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
X_1 Y_1 : C'
f : X_1 ⟶ Y_1
g : Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1
⊢ TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Functor.map (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃}) f ≫
          Iso.hom
            ((fun (Z : C') ↦
                (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
              Y_1)))
      { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) } =
    TypeCat.Fun.toFun
      (ConcreteCategory.hom (FC := TypeCat.Fun)
        (Iso.hom
            ((fun (Z : C') ↦
                (Equiv.trans Equiv.ulift ((e.toAdjunction.homEquiv X Z).trans (Equiv.symm Equiv.ulift))).toIso)
              X_1) ≫
          (e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}).map f))
      { down := g : ULift.{v₁, v₃} (Functor.obj (Functor.obj coyoneda (op (e.functor.obj X))) X_1) }

Tactic:
simp [Adjunction.homEquiv_unit]

Premises used: CategoryTheory.Adjunction.homEquiv_unit
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
have :
  ∀
    (iso :
      Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅
        e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}),
    PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
have iso : coyoneda.obj (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁} ≅
    e.inverse ⋙ coyoneda.obj (op X) ⋙ uliftFunctor.{v₃} :=
    NatIso.ofComponents (fun Z ↦
      (Equiv.ulift.trans ((e.toAdjunction.homEquiv X Z).trans Equiv.ulift.symm)).toIso) (by
        intro _ _ f
        ext ⟨g⟩
        simp [Adjunction.homEquiv_unit])
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
iso :
  Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅
    e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
preservesColimit_of_natIso Y iso.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
inst_3 : IsCardinalPresentable.{w, v₁, u₁} X κ
e : Equivalence.{v₁, v₃, u₁, u₃} C C'
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
Y : Functor.{w, v₃, w, u₃} J C'
this : PreservesColimitsOfShape.{w, w, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
iso :
  Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃} ≅
    e.inverse ⋙ Functor.obj coyoneda (op X) ⋙ uliftFunctor.{v₃, v₁}
⊢ PreservesColimit Y (Functor.obj coyoneda (op (e.functor.obj X)) ⋙ uliftFunctor.{v₁, v₃})

Tactic:
exact preservesColimit_of_natIso Y iso.symm

Premises used: CategoryTheory.Iso.symm, CategoryTheory.Limits.preservesColimit_of_natIso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X Y : C
e : X ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
C' : Type u₃
inst_3 : Category.{v₃, u₃} C'
inst_4 : IsCardinalPresentable.{w, v₁, u₁} X κ
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_5 : F.IsEquivalence
⊢ IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ

Tactic:
isCardinalPresentable_of_equivalence X κ F.asEquivalence

Premises used: CategoryTheory.Functor.asEquivalence, CategoryTheory.isCardinalPresentable_of_equivalence
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
mp : IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ → IsCardinalPresentable.{w, v₁, u₁} X κ
mpr : IsCardinalPresentable.{w, v₁, u₁} X κ → IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ
⊢ IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ ↔ IsCardinalPresentable.{w, v₁, u₁} X κ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
h : IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ

Tactic:
isCardinalPresentable_of_iso
      (show F.inv.obj (F.obj X) ≅ X from F.asEquivalence.unitIso.symm.app X :) κ

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.isCardinalPresentable_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
h : IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ

Tactic:
exact isCardinalPresentable_of_iso
      (show F.inv.obj (F.obj X) ≅ X from F.asEquivalence.unitIso.symm.app X :) κ

Premises used: CategoryTheory.Equivalence.unitIso, CategoryTheory.isCardinalPresentable_of_iso, CategoryTheory.Functor.asEquivalence, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
C' : Type u₃
inst_2 : Category.{v₃, u₃} C'
F : Functor.{v₁, v₃, u₁, u₃} C C'
inst_3 : F.IsEquivalence
h : IsCardinalPresentable.{w, v₁, u₁} X κ
⊢ IsCardinalPresentable.{w, v₃, u₃} (F.obj X) κ

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
f : X ⟶ c.pt
⊢ PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
f : X ⟶ c.pt
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ ∃ (j : J) (f' : X ⟶ F.obj j), f' ≫ c.ι.app j = f

Tactic:
Types.jointly_surjective_of_isColimit (isColimitOfPreserves (coyoneda.obj (op X)) hc) f

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, Opposite.op, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
f : X ⟶ c.pt
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ ∃ (j : J) (f' : X ⟶ F.obj j), f' ≫ c.ι.app j = f

Tactic:
exact Types.jointly_surjective_of_isColimit (isColimitOfPreserves (coyoneda.obj (op X)) hc) f

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, Opposite.op, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
⊢ PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
⊢ IsFiltered.{v₂, u₂} J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this_1 : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
this : IsFiltered.{v₂, u₂} J
⊢ ∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
(Types.FilteredColimit.isColimit_eq_iff _
    (isColimitOfPreserves (coyoneda.obj (op X)) hc)).1 hf

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, Opposite.op, Iff.mp, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i₁ i₂ : J
f₁ : X ⟶ F.obj i₁
f₂ : X ⟶ F.obj i₂
hf : f₁ ≫ c.ι.app i₁ = f₂ ≫ c.ι.app i₂
this_1 : PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))
this : IsFiltered.{v₂, u₂} J
⊢ ∃ (j : J) (u : i₁ ⟶ j) (v : i₂ ⟶ j), f₁ ≫ F.map u = f₂ ≫ F.map v

Tactic:
exact (Types.FilteredColimit.isColimit_eq_iff _
    (isColimitOfPreserves (coyoneda.obj (op X)) hc)).1 hf

Premises used: CategoryTheory.coyoneda, CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff, Opposite.op, Iff.mp, CategoryTheory.Functor.obj, CategoryTheory.Limits.isColimitOfPreserves
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
X : C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalPresentable.{w, v₁, u₁} X κ
J : Type u₂
inst_3 : Category.{v₂, u₂} J
inst_4 : EssentiallySmall.{w, v₂, u₂} J
inst_5 : IsCardinalFiltered.{w, v₂, u₂} J κ
F : Functor.{v₂, v₁, u₂, u₁} J C
c : Cocone F
hc : IsColimit c
i : J
f₁ f₂ : X ⟶ F.obj i
hf : f₁ ≫ c.ι.app i = f₂ ≫ c.ι.app i
⊢ PreservesColimitsOfShape.{v₂, u₂, v₁, v₁, u₁, v₁ + 1} J (Functor.obj coyoneda (op X))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable_of_essentiallySmall X κ J