awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Sheaf.{v, v', u, u'} J A
f g : F ⟶ G
hfg :
  ∀ (G_1 : Sheaf.{v, v', u, u'} J A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
          | (X, i) => freeYoneda J X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
a :
  (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
    | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
    Functor.obj (sheafToPresheaf J A) F
⊢ Eq (α :=
    Functor.obj (presheafToSheaf J A)
        (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
        | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
      G)
    ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J A)
              (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
              | (X, i) => Presheaf.freeYoneda X (S i))
              G) :
          (a :
              (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
                (sheafToPresheaf J A).obj G) →
            (presheafToSheaf J A).obj
                (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
              G)
        (a ≫ Functor.map (sheafToPresheaf J A) f) :
      Functor.obj (presheafToSheaf J A)
          (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
        G)
    ((Equiv.symm
            (Adjunction.homEquiv (sheafificationAdjunction J A)
              (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
              | (X, i) => Presheaf.freeYoneda X (S i))
              G) :
          (a :
              (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
                (sheafToPresheaf J A).obj G) →
            (presheafToSheaf J A).obj
                (match (motive := C × ι → Cᵒᵖ ⥤ A) (X, i) with
                | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
              G)
        (a ≫ Functor.map (sheafToPresheaf J A) g) :
      Functor.obj (presheafToSheaf J A)
          (match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) (X, i) with
          | (X, i) => Presheaf.freeYoneda X (S i)) ⟶
        G)

Tactic:
simpa only [← Adjunction.homEquiv_naturality_right_symm] using
    hfg _ (ObjectProperty.ofObj_apply _ ⟨X, i⟩)
      (((sheafificationAdjunction _ _).homEquiv _ _).symm a)

Premises used: CategoryTheory.ObjectProperty.ofObj_apply, CategoryTheory.sheafificationAdjunction, CategoryTheory.Adjunction.homEquiv_naturality_right_symm, CategoryTheory.Adjunction.homEquiv, Equiv.symm, DFunLike.coe
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
inst_4 :
  HasCoproduct (C := Sheaf.{v, v', u, u'} J A) fun (x : C × ι) ↦
    match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
    | (X, i) => freeYoneda J X (S i)
inst_5 : Preadditive.{v', u'} A
⊢ IsSeparator (C := Sheaf.{v, v', u, u'} J A)
    (∐ fun (x : C × ι) ↦
      match (motive := C × ι → Sheaf.{v, v', u, u'} J A) x with
      | (X, i) => freeYoneda J X (S i))

Tactic:
(isSeparating J hS).isSeparator_coproduct

Premises used: CategoryTheory.Sheaf.isSeparating, CategoryTheory.ObjectProperty.IsSeparating.isSeparator_coproduct
-- Module: Mathlib.CategoryTheory.Generator.Sheaf
Goal:
C : Type u
inst : Category.{v, u} C
J : GrothendieckTopology.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
inst_3 : HasWeakSheafify.{v, v', u, u'} J A
inst_4 : HasSeparator.{v', u'} A
inst_5 : Preadditive.{v', u'} A
inst_6 : HasCoproducts.{u, v', u'} A
⊢ ObjectProperty.IsSeparating.{v', u'} (C := A) (ObjectProperty.ofObj fun (x : Unit) ↦ separator.{v', u'} A)

Tactic:
simpa using isSeparator_separator A

Premises used: CategoryTheory.isSeparator_separator
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
⊢ P.IsStrongGenerator ↔
    P.IsSeparating ∧
      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
        (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator, _private.0.CategoryTheory.ObjectProperty.isStrongGenerator_iff.match_1, And, And.intro, Iff.intro, CategoryTheory.ObjectProperty.IsSeparating, _private.0.CategoryTheory.ObjectProperty.isStrongGenerator_iff.match_2
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
refine_1 :
  P.IsStrongGenerator →
    ∀ (hS₁ : P.IsSeparating)
      (hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤) (X Y : C)
      (i : X ⟶ Y), Mono i → ∀ (h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i), IsIso i
refine_2 :
  (P.IsSeparating ∧
      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
        (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i) →
    ∀ (hS₁ : P.IsSeparating)
      (hS₂ :
        ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
          (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i)
      (X : C) (A : Subobject.{v, u} X) (hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f), A = ⊤
⊢ P.IsStrongGenerator ↔
    P.IsSeparating ∧
      ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
        (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
h_2 : Mono i
h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
refine_1 : Subobject.mk i = ⊤
⊢ IsIso i

Tactic:
rw [Subobject.isIso_iff_mk_eq_top]

Premises used: CategoryTheory.Subobject.isIso_iff_mk_eq_top
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
h_2 : Mono i
h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
⊢ Subobject.mk i = ⊤

Tactic:
hS₂ _ (fun G hG g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
h_2 : Mono i
h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
refine_1 : ∀ (G : C) (hG : P G) (g : G ⟶ Y), (Subobject.mk i).Factors g
⊢ Subobject.mk i = ⊤

Tactic:
refine hS₂ _ (fun G hG g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
h_2 : Mono i
h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (MonoOver.mk i).Factors g

Tactic:
h G hG g

Premises used: CategoryTheory.MonoOver.Factors
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h_1 : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject.{v, u} X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
h_2 : Mono i
h : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
G : C
hG : P G
g : G ⟶ Y
⊢ (MonoOver.mk i).Factors g

Tactic:
exact h G hG g
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h :
  P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ :
  ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
X : C
A : Subobject.{v, u} X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
refine_2 : IsIso A.arrow
⊢ A = ⊤

Tactic:
rw [← Subobject.isIso_arrow_iff_eq_top]

Premises used: CategoryTheory.Subobject.isIso_arrow_iff_eq_top
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h :
  P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ :
  ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
X : C
A : Subobject.{v, u} X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ IsIso A.arrow

Tactic:
hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.factorThru, CategoryTheory.Subobject.factorThru_arrow, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
h :
  P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ :
  ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
    (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
X : C
A : Subobject.{v, u} X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ IsIso A.arrow

Tactic:
exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.factorThru, CategoryTheory.Subobject.factorThru_arrow, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
⊢ P.IsSeparating

Tactic:
hP.1

Premises used: And.left
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X : C
A : Subobject.{v, u} X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ A = ⊤

Tactic:
hP.2 _ hA

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst_1 : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
⊢ IsIso i

Tactic:
(isStrongGenerator_iff.1 hP).2 i hi

Premises used: CategoryTheory.ObjectProperty.isStrongGenerator_iff, And.right, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X : C
A : Subobject.{v, u} X
hA : A ≠ ⊤
by_contra! : ∀ (this : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f), False
⊢ ∃ (G : C) (_ : P G) (f : G ⟶ X), ¬A.Factors f

Tactic:
by_contra!
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X : C
A : Subobject.{v, u} X
hA : A ≠ ⊤
this : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ False

Tactic:
hA (hP.subobject_eq_top this)

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X : C
A : Subobject.{v, u} X
hA : A ≠ ⊤
this : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ False

Tactic:
exact hA (hP.subobject_eq_top this)

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator.subobject_eq_top
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst_1 : Mono i
hi : ¬IsIso i
by_contra! : ∀ (this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ (f : G ⟶ X), f ≫ i = g), False
⊢ ∃ (G : C) (_ : P G) (g : G ⟶ Y), ∀ (f : G ⟶ X), f ≫ i ≠ g

Tactic:
by_contra!
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst_1 : Mono i
hi : ¬IsIso i
this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ (f : G ⟶ X), f ≫ i = g
⊢ False

Tactic:
hi (hP.isIso_of_mono i this)

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator.isIso_of_mono
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X Y : C
i : X ⟶ Y
inst_1 : Mono i
hi : ¬IsIso i
this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ (f : G ⟶ X), f ≫ i = g
⊢ False

Tactic:
exact hi (hP.isIso_of_mono i this)

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator.isIso_of_mono
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
rw :
  P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i
⊢ P.IsStrongGenerator

Tactic:
rw [isStrongGenerator_iff]

Premises used: CategoryTheory.ObjectProperty.isStrongGenerator_iff
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
⊢ P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩

Premises used: CategoryTheory.ObjectProperty.IsSeparating.mk_of_exists_epi, And.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
refine_1 :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X), Epi p
refine_2 :
  ∀ (X Y : C) (i : X ⟶ Y),
    Mono i → ∀ (hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i), IsIso i
⊢ P.IsSeparating ∧
    ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i],
      (∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X : C
refine_1 :
  ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (hc : IsColimit c) (p : c.pt ⟶ X),
    ExtremalEpi p →
      ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
        Epi p
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X), Epi p

Tactic:
obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS X

Premises used: CategoryTheory.ObjectProperty.ι
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X : C
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ X
h : ExtremalEpi p
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X), Epi p

Tactic:
⟨ι, s, hs, c, hc, p, inferInstance⟩

Premises used: inferInstance, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X : C
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ X
h : ExtremalEpi p
⊢ ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X), Epi p

Tactic:
exact ⟨ι, s, hs, c, hc, p, inferInstance⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
refine_2 :
  ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (hc : IsColimit c) (p : c.pt ⟶ Y),
    ExtremalEpi p → IsIso i
⊢ IsIso i

Tactic:
obtain ⟨ι, s, hs, c, hc, p, _⟩ := hS Y

Premises used: CategoryTheory.ObjectProperty.ι
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
hi : ∀ (G : C), P G → Function.Surjective (β := G ⟶ Y) fun (f : G ⟶ X) ↦ f ≫ i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
⊢ ∀ (j : ι), ∃ (a : s j ⟶ X), (fun (f : s j ⟶ X) ↦ f ≫ i) a = c.inj j ≫ p

Tactic:
replace hi (j : ι) := hi (s j) (hs j) (c.inj j ≫ p)
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
hi : ∀ (j : ι), ∃ (a : s j ⟶ X), (fun (f : s j ⟶ X) ↦ f ≫ i) a = c.inj j ≫ p
refine_2 : ∀ (φ : (j : ι) → s j ⟶ X) (hφ : ∀ (j : ι), (fun (f : s j ⟶ X) ↦ f ≫ i) (φ j) = c.inj j ≫ p), IsIso i
⊢ IsIso i

Tactic:
choose φ hφ using hi
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
φ : (j : ι) → s j ⟶ X
hφ : ∀ (j : ι), (fun (f : s j ⟶ X) ↦ f ≫ i) (φ j) = c.inj j ≫ p
⊢ ∀ (i_1 : ι), c.inj i_1 ≫ Cofan.IsColimit.desc hc φ ≫ i = c.inj i_1 ≫ p

Tactic:
simp [hφ]
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hS :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
X Y : C
i : X ⟶ Y
h : Mono i
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v, u} s
hc : IsColimit c
p : c.pt ⟶ Y
h_1 : ExtremalEpi p
φ : (j : ι) → s j ⟶ X
hφ : ∀ (j : ι), (fun (f : s j ⟶ X) ↦ f ≫ i) (φ j) = c.inj j ≫ p
⊢ IsIso i

Tactic:
exact ExtremalEpi.isIso p (Cofan.IsColimit.desc hc φ) _
      (Cofan.IsColimit.hom_ext hc _ _ (by simp [hφ]))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.desc, CategoryTheory.ExtremalEpi.isIso, CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
hP : P.IsStrongGenerator
X : C
inst_1 : HasCoproduct (P.coproductFromFamily X)
Z : C
p : ∐ P.coproductFromFamily X ⟶ Z
i : Z ⟶ X
fac : p ≫ i = P.coproductFrom X
h : Mono i
G : C
hG : P G
f : G ⟶ X
⊢ (fun (f : G ⟶ Z) ↦ f ≫ i) (P.ιCoproductFrom f hG ≫ p) = f

Tactic:
simp [fac]
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
⊢ P.IsStrongGenerator ↔
    ∀ (X : C),
      ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
        ExtremalEpi p

Tactic:
⟨fun hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩

Premises used: CategoryTheory.ObjectProperty.IsStrongGenerator.mk_of_exists_extremalEpi, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
refine :
  ∀ (hP : P.IsStrongGenerator) (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
      ExtremalEpi p
⊢ P.IsStrongGenerator ↔
    ∀ (X : C),
      ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Cofan.{w, v, u} s) (x : IsColimit c) (p : c.pt ⟶ X),
        ExtremalEpi p

Tactic:
refine ⟨fun hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩
-- Module: Mathlib.CategoryTheory.Generator.StrongGenerator
Goal:
C : Type u
inst : Category.{v, u} C
P : ObjectProperty.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : LocallySmall.{w, v, u} C
inst_3 : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
⊢ HasCoproductsOfShape (CostructuredArrow P.ι X) C

Tactic:
have := hasCoproductsOfShape_of_small.{w} C (CostructuredArrow P.ι X)