awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Limits
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
X : Cᵒᵖ
⊢ PreservesLimits.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda X)

Tactic:
show PreservesLimits (preadditiveCoyonedaObj (unop X) ⋙ forget₂ _ _) from inferInstance

Premises used: CategoryTheory.Functor.comp, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
rw :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
⊢ Projective.{v, u} P ↔ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Premises used: CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))

Tactic:
⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
refine_1 :
  ∀
    (h :
      Functor.PreservesEpimorphisms
        (Functor.obj preadditiveCoyoneda (op P) ⋙
          forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
            AddCommGrpCat.carrier))),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
refine_2 :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P)) →
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))

Tactic:
refine ⟨fun h : (preadditiveCoyoneda.obj (op P) ⋙
      forget AddCommGrpCat).PreservesEpimorphisms => ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h :
  Functor.PreservesEpimorphisms
    (Functor.obj preadditiveCoyoneda (op P) ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))

Tactic:
Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P))
        (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, Opposite.op, CategoryTheory.forget, CategoryTheory.preadditiveCoyoneda, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h :
  Functor.PreservesEpimorphisms
    (Functor.obj preadditiveCoyoneda (op P) ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))

Tactic:
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyoneda.obj (op P))
        (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, Opposite.op, CategoryTheory.forget, CategoryTheory.preadditiveCoyoneda, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))

Tactic:
(inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)

Premises used: CategoryTheory.Functor.comp, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op P))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))

Tactic:
exact (inferInstance : (preadditiveCoyoneda.obj (op P) ⋙ forget _).PreservesEpimorphisms)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
rw :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Projective.{v, u} P ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
rw [projective_iff_preservesEpimorphisms_coyoneda_obj]

Premises used: CategoryTheory.Projective.projective_iff_preservesEpimorphisms_coyoneda_obj
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
refine_1 :
  ∀
    (h :
      (preadditiveCoyonedaObj P ⋙
          forget (ModuleCat (End P)ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End P)ᵐᵒᵖ) ↦
            LinearMap (R := (End P)ᵐᵒᵖ) (RingHom.id (End P)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
            ModuleCat.carrier)).PreservesEpimorphisms),
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
refine_2 :
  Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P) →
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P)) ↔
    Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
refine ⟨fun h : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms => ?_, ?_⟩
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h :
  (preadditiveCoyonedaObj P ⋙
      forget (ModuleCat (End P)ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End P)ᵐᵒᵖ) ↦
        LinearMap (R := (End P)ᵐᵒᵖ) (RingHom.id (End P)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
        ModuleCat.carrier)).PreservesEpimorphisms
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyonedaObj P)
        (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h :
  (preadditiveCoyonedaObj P ⋙
      forget (ModuleCat (End P)ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End P)ᵐᵒᵖ) ↦
        LinearMap (R := (End P)ᵐᵒᵖ) (RingHom.id (End P)ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v)) (CC :=
        ModuleCat.carrier)).PreservesEpimorphisms
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)

Tactic:
exact Functor.preservesEpimorphisms_of_preserves_of_reflects (preadditiveCoyonedaObj P)
        (forget _)

Premises used: CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.forget
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))

Tactic:
(inferInstance : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms)

Premises used: CategoryTheory.Functor.comp, inferInstance
-- Module: Mathlib.CategoryTheory.Preadditive.Yoneda.Projective
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
P : C
h : Functor.PreservesEpimorphisms.{v, v, u, v + 1} (D := ModuleCat (End P)ᵐᵒᵖ) (preadditiveCoyonedaObj P)
⊢ Functor.PreservesEpimorphisms.{v, v, u, v + 1} (Functor.obj coyoneda (op P))

Tactic:
exact (inferInstance : (preadditiveCoyonedaObj P ⋙ forget _).PreservesEpimorphisms)

Premises used: inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
inst_3 : IsCardinalPresentable.{w, v, u} X κ
inst_4 : G.IsCardinalAccessible κ
rw : Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{v, v', u'} (op (F.obj X))) κ
⊢ IsCardinalPresentable.{w, v', u'} (F.obj X) κ

Tactic:
rw [isCardinalPresentable_iff_isCardinalAccessible_uliftCoyoneda_obj.{v}]
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
inst_3 : IsCardinalPresentable.{w, v, u} X κ
inst_4 : G.IsCardinalAccessible κ
⊢ Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{v, v', u'} (op (F.obj X))) κ

Tactic:
Functor.isCardinalAccessible_of_natIso
    (show G ⋙ _ ≅ _ from (Adjunction.compUliftCoyonedaIso.{0} adj).symm.app (op X)) κ

Premises used: CategoryTheory.Adjunction.compUliftCoyonedaIso, CategoryTheory.Functor.isCardinalAccessible_of_natIso, Opposite.op, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
inst_3 : IsCardinalPresentable.{w, v, u} X κ
inst_4 : G.IsCardinalAccessible κ
⊢ Functor.IsCardinalAccessible (Functor.obj uliftCoyoneda.{v, v', u'} (op (F.obj X))) κ

Tactic:
exact Functor.isCardinalAccessible_of_natIso
    (show G ⋙ _ ≅ _ from (Adjunction.compUliftCoyonedaIso.{0} adj).symm.app (op X)) κ

Premises used: CategoryTheory.Adjunction.compUliftCoyonedaIso, CategoryTheory.Functor.isCardinalAccessible_of_natIso, Opposite.op, CategoryTheory.Iso.symm, CategoryTheory.Iso.app
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
⊢ isCardinalPresentable.{w, v, u} C κ X

Tactic:
have hX' := hP.le_isCardinalPresentable X hX
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
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.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable.{w, v, u} X κ
⊢ IsCardinalPresentable.{w, v', u'} (F.obj X) κ

Tactic:
have := adj.isCardinalPresentable_leftAdjoint_obj κ X
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable.{w, v, u} X κ
this : IsCardinalPresentable.{w, v', u'} (F.obj X) κ
⊢ IsCardinalPresentable.{w, v', u'} Y κ

Tactic:
isCardinalPresentable_of_iso e κ

Premises used: CategoryTheory.isCardinalPresentable_of_iso
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
X : C
hX : P X
e : F.obj X ≅ Y
hX' : IsCardinalPresentable.{w, v, u} X κ
this : IsCardinalPresentable.{w, v', u'} (F.obj X) κ
⊢ IsCardinalPresentable.{w, v', u'} Y κ

Tactic:
exact isCardinalPresentable_of_iso e κ

Premises used: CategoryTheory.isCardinalPresentable_of_iso
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
⊢ F.IsLeftAdjoint

Tactic:
have := adj.isLeftAdjoint
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
this : F.IsLeftAdjoint
obtain :
  ∀ (J : Type w) (w : SmallCategory J),
    IsCardinalFiltered J κ →
      ∀ (hY : P.ColimitOfShape J (G.obj Y)),
        ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y

Tactic:
obtain ⟨J, _, _, ⟨hY⟩⟩ := hP.exists_colimitsOfShape (G.obj Y)

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.exists_colimitsOfShape, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
this : F.IsLeftAdjoint
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hY : P.ColimitOfShape J (G.obj Y)
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y

Tactic:
⟨J, inferInstance, inferInstance,
      ObjectProperty.prop_of_isIso _ (adj.counit.app Y) ⟨{
        diag := _
        ι := _
        isColimit := isColimitOfPreserves F hY.isColimit
        prop_diag_obj j := P.prop_map_obj _ (hY.prop_diag_obj j) }⟩⟩

Premises used: CategoryTheory.Limits.ColimitPresentation.isColimit, CategoryTheory.ObjectProperty.prop_map_obj, CategoryTheory.Limits.ColimitPresentation.ι, CategoryTheory.NatTrans.mk', CategoryTheory.Functor.comp, inferInstance, CategoryTheory.Limits.Cocone.mk, CategoryTheory.Limits.ColimitPresentation.mk, Nonempty.intro, CategoryTheory.Functor.map, CategoryTheory.Adjunction.counit, CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj, CategoryTheory.Limits.ColimitPresentation.diag, CategoryTheory.Limits.Cocone.ι, Exists.intro, CategoryTheory.Limits.Cocone.functoriality._proof_1, CategoryTheory.ObjectProperty.ColimitOfShape.mk, CategoryTheory.Functor.obj, CategoryTheory.NatTrans.app, CategoryTheory.Limits.isColimitOfPreserves, CategoryTheory.ObjectProperty.prop_of_isIso, CategoryTheory.ObjectProperty.ColimitOfShape.toColimitPresentation
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
P : ObjectProperty.{v, u} C
hP : P.IsCardinalFilteredGenerator κ
inst_3 : G.IsCardinalAccessible κ
inst_4 : G.Full
inst_5 : G.Faithful
Y : D
this : F.IsLeftAdjoint
J : Type w
w : SmallCategory J
w_1 : IsCardinalFiltered J κ
hY : P.ColimitOfShape J (G.obj Y)
⊢ ∃ (J : Type w) (x : SmallCategory J) (_ : IsCardinalFiltered J κ), (P.map F).colimitsOfShape J Y

Tactic:
exact ⟨J, inferInstance, inferInstance,
      ObjectProperty.prop_of_isIso _ (adj.counit.app Y) ⟨{
        diag := _
        ι := _
        isColimit := isColimitOfPreserves F hY.isColimit
        prop_diag_obj j := P.prop_map_obj _ (hY.prop_diag_obj j) }⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
inst_4 : G.IsCardinalAccessible κ
inst_5 : G.Full
inst_6 : G.Faithful
obtain :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.EssentiallySmall.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ),
        ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P),
          P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ

Tactic:
obtain ⟨P, _, hP⟩ := HasCardinalFilteredGenerator.exists_generator C κ

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_generator
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
inst_4 : G.IsCardinalAccessible κ
inst_5 : G.Full
inst_6 : G.Faithful
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ

Tactic:
⟨P.map F, inferInstance, adj.isCardinalFilteredGenerator hP⟩

Premises used: inferInstance, Exists.intro, CategoryTheory.Adjunction.isCardinalFilteredGenerator, CategoryTheory.ObjectProperty.map
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
F : Functor.{v, v', u, u'} C D
G : Functor.{v', v, u', u} D C
adj : F ⊣ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
inst_4 : G.IsCardinalAccessible κ
inst_5 : G.Full
inst_6 : G.Faithful
P : ObjectProperty.{v, u} C
w : ObjectProperty.EssentiallySmall.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v', u'} D) (_ : ObjectProperty.EssentiallySmall.{w, v', u'} P), P.IsCardinalFilteredGenerator κ

Tactic:
exact ⟨P.map F, inferInstance, adj.isCardinalFilteredGenerator hP⟩
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ HasCardinalFilteredGenerator.{w, v', u'} D κ

Tactic:
e.toAdjunction.hasCardinalFilteredGenerator κ

Premises used: CategoryTheory.Adjunction.hasCardinalFilteredGenerator, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ IsCardinalLocallyPresentable.{w, v', u'} D κ

Tactic:
e.toAdjunction.isCardinalLocallyPresentable κ

Premises used: CategoryTheory.Adjunction.isCardinalLocallyPresentable, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ IsCardinalAccessibleCategory.{w, v', u'} D κ

Tactic:
e.toAdjunction.isCardinalAccessibleCategory κ

Premises used: CategoryTheory.Adjunction.isCardinalAccessibleCategory, CategoryTheory.Equivalence.toAdjunction
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsLocallyPresentable.{w, v, u} C
obtain :
  ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
    IsCardinalLocallyPresentable.{w, v, u} C κ → IsLocallyPresentable.{w, v', u'} D
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
obtain ⟨κ, _, _⟩ := IsLocallyPresentable.exists_cardinal.{w} C
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
⟨κ, inferInstance, e.isCardinalLocallyPresentable κ⟩

Premises used: inferInstance, CategoryTheory.Equivalence.isCardinalLocallyPresentable, CategoryTheory.IsLocallyPresentable.mk, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsLocallyPresentable.{w, v, u} C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ IsLocallyPresentable.{w, v', u'} D

Tactic:
exact ⟨κ, inferInstance, e.isCardinalLocallyPresentable κ⟩
-- Module: Mathlib.CategoryTheory.Presentable.Adjunction
Goal:
C : Type u
D : Type u'
inst : Category.{v, u} C
inst_1 : Category.{v', u'} D
e : Equivalence.{v, v', u, u'} C D
inst_2 : IsAccessibleCategory.{w, v, u} C
obtain :
  ∀ (κ : Cardinal.{w}) (w : Fact κ.IsRegular),
    IsCardinalAccessibleCategory.{w, v, u} C κ → IsAccessibleCategory.{w, v', u'} D
⊢ IsAccessibleCategory.{w, v', u'} D

Tactic:
obtain ⟨κ, _, _⟩ := IsAccessibleCategory.exists_cardinal.{w} C