awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ IsAccessibleCategory.{w, v', u'} D

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

Premises used: inferInstance, CategoryTheory.IsAccessibleCategory.mk, CategoryTheory.Equivalence.isCardinalAccessibleCategory, 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 : IsAccessibleCategory.{w, v, u} C
κ : Cardinal.{w}
w : Fact κ.IsRegular
h : IsCardinalAccessibleCategory.{w, v, u} C κ
⊢ IsAccessibleCategory.{w, v', u'} D

Tactic:
exact ⟨κ, inferInstance, e.isCardinalAccessibleCategory κ⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type w
inst_4 : SmallCategory J
inst_5 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
IsCardinalAccessible.preservesColimitOfShape κ _

Premises used: CategoryTheory.Functor.IsCardinalAccessible.preservesColimitOfShape
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
⊢ IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ

Tactic:
have := IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J)
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
⊢ PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (SmallModel.{w, v₃, u₃} J) F

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ (SmallModel.{w} J)
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
this_1 : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
this : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (SmallModel.{w, v₃, u₃} J) F
⊢ PreservesColimitsOfShape.{v₃, u₃, v₁, v₂, u₁, u₂} J F

Tactic:
preservesColimitsOfShape_of_equiv (equivSmallModel.{w} J).symm F

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_equiv, CategoryTheory.Equivalence.symm, CategoryTheory.equivSmallModel
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type u₃
inst_4 : Category.{v₃, u₃} J
inst_5 : EssentiallySmall.{w, v₃, u₃} J
inst_6 : IsCardinalFiltered.{w, v₃, u₃} J κ
this_1 : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
this : PreservesColimitsOfShape.{w, w, v₁, v₂, u₁, u₂} (SmallModel.{w, v₃, u₃} J) F
⊢ PreservesColimitsOfShape.{v₃, u₃, v₁, v₂, u₁, u₂} J F

Tactic:
exact preservesColimitsOfShape_of_equiv (equivSmallModel.{w} J).symm F
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ'
⊢ IsCardinalFiltered J κ

Tactic:
have := IsCardinalFiltered.of_le J h
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
F.preservesColimitsOfShape_of_isCardinalAccessible κ J

Premises used: CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
κ' : Cardinal.{w}
inst_4 : Fact κ'.IsRegular
h : κ ≤ κ'
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ'
this : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
exact F.preservesColimitsOfShape_of_isCardinalAccessible κ J

Premises used: CategoryTheory.Functor.preservesColimitsOfShape_of_isCardinalAccessible
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type w
x : SmallCategory J
hκ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ J
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type w
x : SmallCategory J
hκ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J G

Tactic:
preservesColimitsOfShape_of_natIso e

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_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
F G : Functor.{v₁, v₂, u₁, u₂} C D
e : F ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
inst_3 : F.IsCardinalAccessible κ
J : Type w
x : SmallCategory J
hκ : IsCardinalFiltered J κ
this : PreservesColimitsOfShape J F
⊢ PreservesColimitsOfShape J G

Tactic:
exact preservesColimitsOfShape_of_natIso e

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_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
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
⊢ ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
this : ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
⊢ ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J G

Tactic:
have := G.preservesColimitsOfShape_of_isCardinalAccessible κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
this_1 : ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
this : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J G
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:

Premises used: CategoryTheory.Functor.IsCardinalAccessible.mk
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G_1 : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G_1
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
E : Type u₃
inst_3 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_4 : F.IsCardinalAccessible κ
inst_5 : G.IsCardinalAccessible κ
this_1 : ∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J F
this : ∀ (J : Type w) [inst : SmallCategory J] [IsCardinalFiltered J κ], PreservesColimitsOfShape J G
⊢ (F ⋙ G).IsCardinalAccessible κ

Tactic:
exact { }
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
⊢ IsFiltered J

Tactic:
have h := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
j : J
dsimp : IsIso.{v₁, u₁} (𝟙 A)
⊢ IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
    obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
    (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
j : J
⊢ IsIso.{v₁, u₁} (𝟙 A)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
⊢ ∀ (j : J),
    IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
      obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)

Tactic:
have (j : J) : IsIso ((((const C).obj A).mapCocone c).ι.app j) := by
              dsimp
              infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this :
  ∀ (j : J),
    IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
      obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
x_1 : J
x_2 : Nonempty.some ⋯ ⟶ x_1
dsimp : IsIso.{v₁, u₁} (𝟙 A)
⊢ IsIso (X := obj (F ⋙ obj (const C) A) (Nonempty.some ⋯)) (map (F ⋙ obj (const C) A) x_2)

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this :
  ∀ (j : J),
    IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
      obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
x_1 : J
x_2 : Nonempty.some ⋯ ⟶ x_1
⊢ IsIso.{v₁, u₁} (𝟙 A)

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 G : Functor.{v₁, v₂, u₁, u₂} C D
e : F_1 ≅ G
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
A : C
J : Type w
x : SmallCategory J
h_1 : IsCardinalFiltered J κ
F : Functor.{w, v₁, w, u₁} J C
c : Cocone F
hc : IsColimit c
h : IsFiltered J
this :
  ∀ (j : J),
    IsIso (X := obj (F ⋙ obj (const C) A) j) (Y :=
      obj.{w, v₁, w, u₁} (obj (const J) (Cocone.pt (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c))) j)
      (NatTrans.app (Cocone.ι (mapCocone (obj (const C) A) c)) j)
⊢ IsColimit (F := F ⋙ obj (const C) A) (mapCocone (obj (const C) A) c)

Tactic:
exact Functor.IsEventuallyConstantFrom.isColimitOfIsIso
              (i₀ := h.nonempty.some) (fun _ _ ↦ by dsimp; infer_instance) _

Premises used: CategoryTheory.Functor.IsEventuallyConstantFrom.isColimitOfIsIso
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
obtain :
  ∀ (κF : Cardinal.{w}) (w : Fact κF.IsRegular), F.IsCardinalAccessible κF → IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
obtain ⟨κF, _, _⟩ := IsAccessible.exists_cardinal (F := F)

Premises used: CategoryTheory.Functor.IsAccessible.exists_cardinal
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
obtain :
  ∀ (κG : Cardinal.{w}) (w : Fact κG.IsRegular), G.IsCardinalAccessible κG → IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
obtain ⟨κG, _, _⟩ := IsAccessible.exists_cardinal (F := G)

Premises used: CategoryTheory.Functor.IsAccessible.exists_cardinal
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
⊢ Fact (Cardinal.IsRegular.{w} (max κF κG))

Tactic:
have : Fact (κF ⊔ κG).IsRegular := ⟨iteInduction (fun _ ↦ Fact.out) (fun _ ↦ Fact.out)⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this : Fact (Cardinal.IsRegular.{w} (max κF κG))
⊢ κF ≤ max κF κG

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this : Fact (Cardinal.IsRegular.{w} (max κF κG))
⊢ IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)

Tactic:
have := isCardinalAccessible_of_le F (by simp : κF ≤ κF ⊔ κG)
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this_1 : Fact (Cardinal.IsRegular.{w} (max κF κG))
this : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
⊢ κG ≤ max κF κG

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this_1 : Fact (Cardinal.IsRegular.{w} (max κF κG))
this : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
⊢ IsCardinalAccessible.{w, v₂, v₃, u₂, u₃} G (max κF κG)

Tactic:
have := isCardinalAccessible_of_le G (by simp : κG ≤ κF ⊔ κG)
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this_1 : Fact (Cardinal.IsRegular.{w} (max κF κG))
this_2 : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
this : IsCardinalAccessible.{w, v₂, v₃, u₂, u₃} G (max κF κG)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
isAccessible_of_isCardinalAccessible (F ⋙ G) (κF ⊔ κG)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.isAccessible_of_isCardinalAccessible, Max.max
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F_1 : Functor.{v₁, v₂, u₁, u₂} C D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₃, u₂, u₃} D E
inst_3 : IsAccessible.{w, v₁, v₂, u₁, u₂} F
inst_4 : IsAccessible.{w, v₂, v₃, u₂, u₃} G
κF : Cardinal.{w}
w : Fact κF.IsRegular
h : F.IsCardinalAccessible κF
κG : Cardinal.{w}
w_1 : Fact κG.IsRegular
h_1 : G.IsCardinalAccessible κG
this_1 : Fact (Cardinal.IsRegular.{w} (max κF κG))
this_2 : IsCardinalAccessible.{w, v₁, v₂, u₁, u₂} F (max κF κG)
this : IsCardinalAccessible.{w, v₂, v₃, u₂, u₃} G (max κF κG)
⊢ IsAccessible.{w, v₁, v₃, u₁, u₃} (F ⋙ G)

Tactic:
exact isAccessible_of_isCardinalAccessible (F ⋙ G) (κF ⊔ κG)

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.isAccessible_of_isCardinalAccessible, Max.max
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : C
⊢ Fact Cardinal.aleph0.IsRegular

Tactic:
have : Fact Cardinal.aleph0.IsRegular := Cardinal.fact_isRegular_aleph0
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : C
this : Fact Cardinal.aleph0.IsRegular
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} (obj (const C) A)

Tactic:
⟨Cardinal.aleph0, inferInstance, inferInstance⟩

Premises used: inferInstance, Cardinal.aleph0, Exists.intro, CategoryTheory.Functor.IsAccessible.mk
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
A : C
this : Fact Cardinal.aleph0.IsRegular
⊢ IsAccessible.{w, v₁, v₁, u₁, u₁} (obj (const C) A)

Tactic:
exact ⟨Cardinal.aleph0, inferInstance, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 Y : C
e : X_1 ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : ObjectProperty.FullSubcategory.{v₁, u₁} (isCardinalPresentable C κ)
⊢ IsCardinalPresentable.{w, v₁, u₁} (X.obj (P := isCardinalPresentable C κ)) κ

Tactic:
X.property

Premises used: CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.isCardinalPresentable
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 Y : C
e : X_1 ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : ObjectProperty.FullSubcategory.{v₁, u₁} (isCardinalPresentable C κ)
dsimp : IsCardinalPresentable.{w, v₁, u₁} (X.obj (P := isCardinalPresentable C κ)) κ
⊢ IsCardinalPresentable.{w, v₁, u₁} (Functor.obj (ObjectProperty.ι (isCardinalPresentable C κ)) X) κ

Tactic:
dsimp
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
X_1 Y : C
e : X_1 ≅ Y
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : ObjectProperty.FullSubcategory.{v₁, u₁} (isCardinalPresentable C κ)
⊢ IsCardinalPresentable.{w, v₁, u₁} (X.obj (P := isCardinalPresentable C κ)) κ

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
⊢ IsCardinalPresentable.{w, v₁, u₁} X κ ↔
    Functor.IsCardinalAccessible.{w, v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op X)) κ

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Presentable.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
X : C
⊢ isCardinalPresentable.{w, v₁, u₁} C κ X ↔ IsCardinalPresentable.{w, v₁, u₁} X κ

Tactic:
Iff.rfl

Premises used: Iff.rfl, CategoryTheory.isCardinalPresentable