awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
⊢ W.isLocal.ι.IsRightAdjoint

Tactic:
have := isRightAdjoint_ι_isLocal W κ hW
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
this : W.isLocal.ι.IsRightAdjoint
⊢ W.isLocal.ι.IsCardinalAccessible κ

Tactic:
have := MorphismProperty.isCardinalAccessible_ι_isLocal W κ hW
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
this_1 : W.isLocal.ι.IsRightAdjoint
this : W.isLocal.ι.IsCardinalAccessible κ
⊢ IsCardinalLocallyPresentable.{w, v, u} W.isLocal.FullSubcategory κ

Tactic:
(Adjunction.ofIsRightAdjoint W.isLocal.ι).isCardinalLocallyPresentable κ

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Adjunction.isCardinalLocallyPresentable, CategoryTheory.MorphismProperty.isLocal, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Presentable.OrthogonalReflection
Goal:
C : Type u
inst : Category.{v, u} C
W : MorphismProperty.{v, u} C
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v, u} C κ
inst_3 : IsSmall.{w, v, u} W
hW : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), W f → IsCardinalPresentable.{w, v, u} X κ ∧ IsCardinalPresentable.{w, v, u} Y κ
this_1 : W.isLocal.ι.IsRightAdjoint
this : W.isLocal.ι.IsCardinalAccessible κ
⊢ IsCardinalLocallyPresentable.{w, v, u} W.isLocal.FullSubcategory κ

Tactic:
exact (Adjunction.ofIsRightAdjoint W.isLocal.ι).isCardinalLocallyPresentable κ

Premises used: CategoryTheory.ObjectProperty.ι, CategoryTheory.Adjunction.isCardinalLocallyPresentable, CategoryTheory.MorphismProperty.isLocal, CategoryTheory.Adjunction.ofIsRightAdjoint
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
preservesColimitOfShape :
  autoParam
    (∀ (J : Type w) [inst_6 : SmallCategory J] [IsCardinalFiltered J κ],
      PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M))))
    Functor.IsCardinalAccessible.preservesColimitOfShape._autoParam
⊢ IsCardinalPresentable (C := Functor.{v, v', u, u'} Cᵒᵖ A) (freeYoneda X M) κ

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
preservesColimitOfShape :
  ∀ [inst_6 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))
⊢ ∀ [inst_6 : SmallCategory J] [IsCardinalFiltered J κ],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
inst_6 : SmallCategory J
preservesColimitOfShape :
  ∀ [IsCardinalFiltered J κ],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))
⊢ ∀ [IsCardinalFiltered J κ],
    PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
inst_6 : SmallCategory J
inst_7 : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape.{w, w, v', v', u', v' + 1} J (Functor.obj coyoneda (op M))

Tactic:
have := preservesColimitsOfShape_of_isCardinalPresentable M κ J
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
inst_6 : SmallCategory J
inst_7 : IsCardinalFiltered J κ
this : PreservesColimitsOfShape.{w, w, v', v', u', v' + 1} J (Functor.obj coyoneda (op M))
⊢ PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))

Tactic:
preservesColimitsOfShape_of_natIso e.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasColimitsOfSize.{w, w, v', u'} A
inst_3 : HasCoproducts.{v, v', u'} A
κ : Cardinal.{w}
inst_4 : Fact κ.IsRegular
X : C
M : A
inst_5 : IsCardinalPresentable.{w, v', u'} M κ
e : Iso (C := Functor.{v, v', u, u'} Cᵒᵖ A ⥤ Type (max u v')) (Functor.obj coyoneda (op (freeYoneda X M)))
  (Functor.obj (evaluation Cᵒᵖ A) (op X) ⋙ Functor.obj coyoneda (op M) ⋙ uliftFunctor.{u, v'}) :=
  NatIso.ofComponents
    (fun (P : Functor.{v, v', u, u'} Cᵒᵖ A) ↦ Equiv.toIso (Equiv.trans freeYonedaHomEquiv (Equiv.symm Equiv.ulift))) ⋯
J : Type w
inst_6 : SmallCategory J
inst_7 : IsCardinalFiltered J κ
this : PreservesColimitsOfShape.{w, w, v', v', u', v' + 1} J (Functor.obj coyoneda (op M))
⊢ PreservesColimitsOfShape (C := Functor.{v, v', u, u'} Cᵒᵖ A) J (Functor.obj coyoneda (op (freeYoneda X M)))

Tactic:
exact preservesColimitsOfShape_of_natIso e.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
e : Iso (C := (Cᵒᵖ ⥤ Type (max u' u)) ⥤ Type (max u u'))
  (Functor.obj coyoneda (op (Functor.obj uliftYoneda.{u', u, u} X)))
  (Functor.obj (evaluation Cᵒᵖ (Type (max u' u))) (op X) ⋙ uliftFunctor.{max u u', max u u'}) :=
  NatIso.ofComponents
    (fun (P : Cᵒᵖ ⥤ Type (max u' u)) ↦ Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift))) ⋯
⊢ PreservesColimitsOfShape (C := Cᵒᵖ ⥤ Type (max u' u)) J
    (Functor.obj coyoneda (op (Functor.obj uliftYoneda.{u', u, u} X)))

Tactic:
preservesColimitsOfShape_of_natIso e.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
C : Type u
inst : SmallCategory C
inst_1 : HasColimitsOfSize.{w, w, max u u', max (u + 1) (u' + 1)} (Type (max u u'))
κ : Cardinal.{w}
inst_2 : Fact κ.IsRegular
X : C
J : Type w
x : SmallCategory J
h : IsCardinalFiltered J κ
e : Iso (C := (Cᵒᵖ ⥤ Type (max u' u)) ⥤ Type (max u u'))
  (Functor.obj coyoneda (op (Functor.obj uliftYoneda.{u', u, u} X)))
  (Functor.obj (evaluation Cᵒᵖ (Type (max u' u))) (op X) ⋙ uliftFunctor.{max u u', max u u'}) :=
  NatIso.ofComponents
    (fun (P : Cᵒᵖ ⥤ Type (max u' u)) ↦ Equiv.toIso (Equiv.trans uliftYonedaEquiv (Equiv.symm Equiv.ulift))) ⋯
⊢ PreservesColimitsOfShape (C := Cᵒᵖ ⥤ Type (max u' u)) J
    (Functor.obj coyoneda (op (Functor.obj uliftYoneda.{u', u, u} X)))

Tactic:
exact preservesColimitsOfShape_of_natIso e.symm

Premises used: CategoryTheory.Limits.preservesColimitsOfShape_of_natIso, CategoryTheory.Iso.symm
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP : P.IsStrongGenerator
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
rw :
  ∀
    (hP :
      P.IsSeparating ∧
        ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
          (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i)
    [inst_4 : HasCoproducts.{w, v', u'} A] [HasPullbacks.{v', u'} A] (C : Type w) [inst_6 : SmallCategory C],
    ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
        (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
      ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
        (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
            ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
              Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
          IsIso i
⊢ ObjectProperty.IsStrongGenerator (C := Functor.{w, v', w, u'} Cᵒᵖ A)
    (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A))

Tactic:
rw [ObjectProperty.isStrongGenerator_iff] at hP ⊢

Premises used: CategoryTheory.ObjectProperty.isStrongGenerator_iff
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP :
  P.IsSeparating ∧
    ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
⊢ P.IsSeparating

Tactic:
obtain ⟨hP₁, hP₂⟩ := hP
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
hP :
  P.IsSeparating ∧
    ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
⊢ ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
obtain ⟨hP₁, hP₂⟩ := hP
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
⊢ ObjectProperty.IsSeparating.{v', u'} (C := A) (ObjectProperty.ofObj (ι := Subtype P) (Subtype.val (p := P)))

Tactic:
simpa using hP₁
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
refine :
  ∀ (P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A) (i : P₁ ⟶ P₂),
    Mono i →
      ∀
        (hi :
          ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
            ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
              Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i),
        IsIso i
⊢ ObjectProperty.IsSeparating (C := Functor.{w, v', w, u'} Cᵒᵖ A)
      (ObjectProperty.ofObj fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) ∧
    ∀ ⦃X Y : Functor.{w, v', w, u'} Cᵒᵖ A⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
          ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
            Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) →
        IsIso i

Tactic:
refine ⟨Presheaf.isSeparating (C := C) (ι := Subtype P) (S := Subtype.val)
    (by simpa using hP₁),
    fun P₁ P₂ i _ hi ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
rw : ∀ (X : Cᵒᵖ), IsIso (i.app X)
⊢ IsIso i

Tactic:
rw [NatTrans.isIso_iff_isIso_app]

Premises used: CategoryTheory.NatTrans.isIso_iff_isIso_app
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
⊢ IsIso (X := P₁.obj (op X)) (i.app (op X))

Tactic:
hP₂ _ (fun G hG f ↦ ?_)
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
refine :
  ∀ (G : A) (hG : P G) (f : G ⟶ P₂.obj (op X)),
    ∃ (a : G ⟶ P₁.obj (op X)), (fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a = f
⊢ IsIso (X := P₁.obj (op X)) (i.app (op X))

Tactic:
refine hP₂ _ (fun G hG f ↦ ?_)
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
f : G ⟶ P₂.obj (op X)
obtain :
  ∀ (y : freeYoneda X G ⟶ P₂),
    ∃ (a : G ⟶ P₁.obj (op X)),
      Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a : G ⟶ P₂.obj (op X))
        ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) y : G ⟶ P₂.obj (op X))
⊢ ∃ (a : G ⟶ P₁.obj (op X)), (fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a = f

Tactic:
obtain ⟨y, rfl⟩ := freeYonedaHomEquiv.surjective f

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
y : freeYoneda X G ⟶ P₂
obtain :
  ∀ (x : freeYoneda X G ⟶ P₁),
    ∃ (a : G ⟶ P₁.obj (op X)),
      Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a)
        ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X))
          ((fun (f : freeYoneda X G ⟶ P₁) ↦ f ≫ i) x))
⊢ ∃ (a : G ⟶ P₁.obj (op X)),
    Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a : G ⟶ P₂.obj (op X))
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) y : G ⟶ P₂.obj (op X))

Tactic:
obtain ⟨x, rfl⟩ := hi (freeYoneda X G)
    (ObjectProperty.ofObj_apply (fun (T : C × (Subtype P)) ↦
      freeYoneda T.1 T.2.1) ⟨X, G, hG⟩) y

Premises used: CategoryTheory.ObjectProperty.ofObj_apply, Prod.mk, Prod.fst, CategoryTheory.Presheaf.freeYoneda, Subtype.mk, Subtype.val, Prod.snd, rfl
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
x : freeYoneda X G ⟶ P₁
⊢ Eq.{v' + 1} (α := G ⟶ P₂.obj (op X))
    ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X))
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₁) → G ⟶ P₁.obj (op X)) x))
    ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) ((fun (f : freeYoneda X G ⟶ P₁) ↦ f ≫ i) x))

Tactic:
simp [freeYonedaHomEquiv_comp]

Premises used: CategoryTheory.Presheaf.freeYonedaHomEquiv_comp
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
P : ObjectProperty.{v', u'} A
inst_1 : HasCoproducts.{w, v', u'} A
inst_2 : HasPullbacks.{v', u'} A
C : Type w
inst_3 : SmallCategory C
hP₁ : P.IsSeparating
hP₂ :
  ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : A), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
P₁ P₂ : Functor.{w, v', w, u'} Cᵒᵖ A
i : P₁ ⟶ P₂
h : Mono i
hi :
  ∀ (G : Functor.{w, v', w, u'} Cᵒᵖ A),
    ObjectProperty.ofObj (fun (T : Prod.{w, u'} C (Subtype P)) ↦ freeYoneda T.1 (↑T.2 : A)) G →
      Function.Surjective (β := G ⟶ P₂) fun (f : G ⟶ P₁) ↦ f ≫ i
X : C
G : A
hG : P G
x : freeYoneda X G ⟶ P₁
⊢ ∃ (a : G ⟶ P₁.obj (op X)),
    Eq.{v' + 1} (α := G ⟶ P₂.obj (op X)) ((fun (f : G ⟶ P₁.obj (op X)) ↦ f ≫ i.app (op X)) a)
      ((freeYonedaHomEquiv : (a : freeYoneda X G ⟶ P₂) → G ⟶ P₂.obj (op X)) ((fun (f : freeYoneda X G ⟶ P₁) ↦ f ≫ i) x))

Tactic:
exact ⟨freeYonedaHomEquiv x, by simp [freeYonedaHomEquiv_comp]⟩
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
⊢ ∃ (P : ObjectProperty.{v', u'} A) (_ : ObjectProperty.Small.{w, v', u'} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable A κ

Tactic:
have hA := (IsCardinalLocallyPresentable.iff_exists_isStrongGenerator A κ).1 inferInstance
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
hA :
  ∃ (P : ObjectProperty.{v', u'} A) (_ : ObjectProperty.Small.{w, v', u'} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable A κ
obtain :
  ∀ (P : ObjectProperty.{v', u'} A),
    ObjectProperty.Small.{w, v', u'} P →
      ∀ (hP₁ : P.IsStrongGenerator) (hP₂ : P ≤ isCardinalPresentable A κ),
        IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
⊢ IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
obtain ⟨P, _, hP₁, hP₂⟩ := hA
-- Module: Mathlib.CategoryTheory.Presentable.Presheaf
Goal:
A : Type u'
inst : Category.{v', u'} A
κ : Cardinal.{w}
inst_1 : Fact κ.IsRegular
inst_2 : IsCardinalLocallyPresentable.{w, v', u'} A κ
inst_3 : HasPullbacks.{v', u'} A
C : Type w
inst_4 : SmallCategory C
P : ObjectProperty.{v', u'} A
w : ObjectProperty.Small.{w, v', u'} P
hP₁ : P.IsStrongGenerator
hP₂ : P ≤ isCardinalPresentable A κ
rw :
  ∃ (P : ObjectProperty (Functor.{w, v', w, u'} Cᵒᵖ A)) (_ : ObjectProperty.Small.{w, max v' w, max (max u' v') w} P),
    P.IsStrongGenerator ∧ P ≤ isCardinalPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ
⊢ IsCardinalLocallyPresentable (Functor.{w, v', w, u'} Cᵒᵖ A) κ

Tactic:
rw [IsCardinalLocallyPresentable.iff_exists_isStrongGenerator]

Premises used: CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGenerator