awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
this_2 :
  Mono (X := colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)) (Y :=
    (E.coconeAt X).pt)
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
this :
  IsIso (X := colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (Y := (E.coconeAt X).pt)
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X

Tactic:
⟨IsColimit.ofIsoColimit (colimit.isColimit _) (Cocone.ext
      (asIso (colimit.desc _ (E.coconeAt X))))⟩

Premises used: CategoryTheory.Limits.Cocone.ext, CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.IsColimit.ofIsoColimit, CategoryTheory.Functor.isDenseAt, CategoryTheory.Functor.LeftExtension.coconeAt, Nonempty.intro, CategoryTheory.Limits.colimit.desc, CategoryTheory.asIso
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this_1 : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
this_2 :
  Mono (X := colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)) (Y :=
    (E.coconeAt X).pt)
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
this :
  IsIso (X := colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι))
    (Y := (E.coconeAt X).pt)
    (colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
      (E.coconeAt X))
⊢ (P.colimitsCardinalClosure κ).ι.isDenseAt X

Tactic:
exact ⟨IsColimit.ofIsoColimit (colimit.isColimit _) (Cocone.ext
      (asIso (colimit.desc _ (E.coconeAt X))))⟩
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
hP : P ≤ isCardinalPresentable C κ
⊢ P.colimitsCardinalClosure κ ≤ isCardinalPresentable C κ

Tactic:
P.colimitsCardinalClosure_le κ
    (fun _ _ hJ ↦ isClosedUnderColimitsOfShape_isCardinalPresentable C hJ) hP

Premises used: CategoryTheory.isClosedUnderColimitsOfShape_isCardinalPresentable, CategoryTheory.ObjectProperty.colimitsCardinalClosure_le
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable, le_antisymm
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
refine : isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
refine le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure_le_isCardinalPresentable, le_antisymm
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ (P.colimitsCardinalClosure κ).ι.IsDense

Tactic:
have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
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.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
rw : (P.colimitsCardinalClosure κ).retractClosure X
⊢ P.colimitsCardinalClosure κ X

Tactic:
rw [← (P.colimitsCardinalClosure κ).retractClosure_eq_self]

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.ObjectProperty.retractClosure_eq_self
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
obtain :
  ∀ (j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X)
    (φ : X ⟶ (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι).obj j)
    (hφ :
      φ ≫ ((Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv).coconeAt X).ι.app j = 𝟙 X),
    (P.colimitsCardinalClosure κ).retractClosure X
⊢ (P.colimitsCardinalClosure κ).retractClosure X

Tactic:
obtain ⟨j, φ, hφ⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ
    ((P.colimitsCardinalClosure κ).ι.denseAt X) (𝟙 X)

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.ObjectProperty.ι, CategoryTheory.CategoryStruct.id, CategoryTheory.IsCardinalPresentable.exists_hom_of_isColimit, CategoryTheory.Functor.denseAt
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ : X ⟶ (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι).obj j
hφ : φ ≫ ((Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv).coconeAt X).ι.app j = 𝟙 X
⊢ (P.colimitsCardinalClosure κ).retractClosure X

Tactic:
⟨_, j.left.2, ⟨{ i := _, r := _, retract := hφ }⟩⟩

Premises used: CategoryTheory.ObjectProperty.colimitsCardinalClosure, CategoryTheory.Functor.LeftExtension.mk, CategoryTheory.ObjectProperty.ι, CategoryTheory.Functor.rightUnitor, CategoryTheory.ObjectProperty.FullSubcategory.property, CategoryTheory.Functor.id, CategoryTheory.Functor.LeftExtension.coconeAt, Nonempty.intro, CategoryTheory.Limits.Cocone.ι, Exists.intro, CategoryTheory.Retract.mk, CategoryTheory.CostructuredArrow.left, CategoryTheory.Iso.inv, CategoryTheory.NatTrans.app, CategoryTheory.ObjectProperty.retractClosure
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
P : ObjectProperty.{v, u} C
inst_4 : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
X : C
hX : IsCardinalPresentable.{w, v, u} X κ
j : CostructuredArrow (P.colimitsCardinalClosure κ).ι X
φ : X ⟶ (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι).obj j
hφ : φ ≫ ((Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv).coconeAt X).ι.app j = 𝟙 X
⊢ (P.colimitsCardinalClosure κ).retractClosure X

Tactic:
exact ⟨_, j.left.2, ⟨{ i := _, r := _, retract := hφ }⟩⟩
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ ↔
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
⟨fun _ ↦ ?_, fun ⟨P, _, hS₁, hS₂⟩ ↦ ?_⟩

Premises used: _private.0.CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator.match_1, Iff.intro, CategoryTheory.IsCardinalLocallyPresentable
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
refine_1 :
  IsCardinalLocallyPresentable.{w, v, u} C κ →
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
refine_2 :
  (∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ) →
    ∀ (P : ObjectProperty.{v, u} C),
      ObjectProperty.Small.{w, v, u} P →
        ∀ (hS₁ : P.IsStrongGenerator) (hS₂ : P ≤ isCardinalPresentable C κ), IsCardinalLocallyPresentable.{w, v, u} C κ
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ ↔
    ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
      P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
refine ⟨fun _ ↦ ?_, fun ⟨P, _, hS₁, hS₂⟩ ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h : IsCardinalLocallyPresentable.{w, v, u} C κ
refine_1 :
  ∀ (P : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} P →
      ∀ (hP : P.IsCardinalFilteredGenerator κ),
        ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
          P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

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

Premises used: CategoryTheory.HasCardinalFilteredGenerator.exists_small_generator
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h : IsCardinalLocallyPresentable.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
⟨_, inferInstance, hP.isStrongGenerator, hP.le_isCardinalPresentable⟩

Premises used: CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isStrongGenerator, CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.le_isCardinalPresentable, inferInstance, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h : IsCardinalLocallyPresentable.{w, v, u} C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hP : P.IsCardinalFilteredGenerator κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ

Tactic:
exact ⟨_, inferInstance, hP.isStrongGenerator, hP.le_isCardinalPresentable⟩
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ (P.colimitsCardinalClosure κ).ι.IsDense

Tactic:
have := hS₁.isDense_colimitsCardinalClosure_ι hS₂
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this : (P.colimitsCardinalClosure κ).ι.IsDense
⊢ HasCardinalFilteredGenerator.{w, v, u} C κ

Tactic:
have : HasCardinalFilteredGenerator C κ :=
      { exists_generator := ⟨(P.colimitsCardinalClosure κ), inferInstance,
            IsCardinalFilteredGenerator.of_isDense_ι _ _
              (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)⟩ }
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : HasColimitsOfSize.{w, w, v, u} C
inst_3 : LocallySmall.{w, v, u} C
h :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ
P : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
this_1 : (P.colimitsCardinalClosure κ).ι.IsDense
this : HasCardinalFilteredGenerator.{w, v, u} C κ
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
rw :
  ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
⊢ IsCardinalLocallyPresentable.{w, v, u} C κ'

Tactic:
rw [iff_exists_isStrongGenerator]

Premises used: CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
obtain :
  ∀ (S : ObjectProperty.{v, u} C),
    ObjectProperty.Small.{w, v, u} S →
      ∀ (h₁ : S.IsStrongGenerator) (h₂ : S ≤ isCardinalPresentable C κ),
        ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
          P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'

Tactic:
obtain ⟨S, _, h₁, h₂⟩ := (iff_exists_isStrongGenerator C κ).1 inferInstance

Premises used: CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator, inferInstance, Iff.mp
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
S : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} S
h₁ : S.IsStrongGenerator
h₂ : S ≤ isCardinalPresentable C κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'

Tactic:
⟨S, inferInstance, h₁, h₂.trans (isCardinalPresentable_monotone _ h)⟩

Premises used: CategoryTheory.isCardinalPresentable_monotone, inferInstance, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.CategoryTheory.Presentable.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
κ' : Cardinal.{w}
inst_3 : Fact κ'.IsRegular
h : κ ≤ κ'
S : ObjectProperty.{v, u} C
w : ObjectProperty.Small.{w, v, u} S
h₁ : S.IsStrongGenerator
h₂ : S ≤ isCardinalPresentable C κ
⊢ ∃ (P : ObjectProperty.{v, u} C) (_ : ObjectProperty.Small.{w, v, u} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable C κ'

Tactic:
exact ⟨S, inferInstance, h₁, h₂.trans (isCardinalPresentable_monotone _ h)⟩
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
⊢ IsFiltered J

Tactic:
have := isFiltered_of_isCardinalFiltered J κ
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
refine_1 :
  ∀ (j : (x : X) → J) (g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1)))
    (hg :
      ∀ (x_1 : X),
        Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
          ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
                (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
                  (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
              (g x_1) :
            (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
          ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
            (fun (X : Type u) ↦ X) c.pt)),
    ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
      f =
        (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
            (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
          xi
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi

Tactic:
choose j g hg using fun x ↦ Types.jointly_surjective_of_isColimit hc (f x)

Premises used: CategoryTheory.ConcreteCategory.hom, CategoryTheory.Limits.Types.jointly_surjective_of_isColimit, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Presentable.Type
Goal:
X : Type u
κ : Cardinal.{u}
hX : HasCardinalLT X κ
inst : Fact κ.IsRegular
J : Type u
x : SmallCategory J
h : IsCardinalFiltered J κ
F : J ⥤ Type u
c : Cocone F
hc : IsColimit c
this : IsFiltered J
f : X ⟶ c.pt
j : (x : X) → J
g : (x_1 : X) → (fun (X : Type u) ↦ X) (F.obj (j x_1))
hg :
  ∀ (x_1 : X),
    Eq (α := (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) (c.ι.app (j x_1)) :
            (a : (fun (X : Type u) ↦ X) (F.obj (j x_1))) →
              (fun (X : Type u) ↦ X) (((Functor.const J).obj c.pt).obj (j x_1)))
          (g x_1) :
        (fun (X : Type u) ↦ X) (Functor.obj (Functor.obj (Functor.const J) c.pt) (j x_1)))
      ((hom (FC := TypeCat.Fun) f : (a : (fun (X : Type u) ↦ X) X) → (fun (X : Type u) ↦ X) c.pt) x_1 :
        (fun (X : Type u) ↦ X) c.pt)
⊢ ∃ (i : J) (xi : (fun (X : Type u) ↦ X) ((F ⋙ Functor.obj coyoneda (op X)).obj i)),
    f =
      (hom (FC := TypeCat.Fun) (NatTrans.app (Cocone.ι (Functor.mapCocone (Functor.obj coyoneda (op X)) c)) i) :
          (a : (fun (X : Type u) ↦ X) ((F ⋙ coyoneda.obj (op X)).obj i)) →
            (fun (X : Type u) ↦ X) (((Functor.const J).obj ((coyoneda.obj (op X)).mapCocone c).pt).obj i))
        xi

Tactic:
⟨IsCardinalFiltered.max j hX,
          ↾fun x ↦ F.map (IsCardinalFiltered.toMax j hX x) (g x), ?_⟩

Premises used: CategoryTheory.ConcreteCategory.hom, TypeCat.ofHom, CategoryTheory.IsCardinalFiltered.toMax, CategoryTheory.Functor.map, Exists.intro, DFunLike.coe, CategoryTheory.IsCardinalFiltered.max