awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.HomologicalComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
⊢ p ≫ f.f j = p ≫ g.f j
have h₁ : ∀
  (H :
    Functor.CorepresentableBy (C := HomologicalComplex.{v, u, w} C c)
      (eval C c j ⋙ Functor.obj coyoneda (Opposite.op (X a))) (evalCompCoyonedaCorepresentative c (X a) j)),
  p ≫ f.f j = p ≫ g.f j
Tactic: have H := evalCompCoyonedaCorepresentable c (X a) j
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.HomologicalComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasZeroMorphisms.{v, u} C
inst_3 : HasZeroObject.{v, u} C
α : Type t
X : α → C
hX : ObjectProperty.IsSeparating.{v, u} (ObjectProperty.ofObj X)
K L : HomologicalComplex.{v, u, w} C c
f g : K ⟶ L
h :
  ∀ (G : HomologicalComplex.{v, u, w} C c), ObjectProperty.ofObj (separatingFamily c X) G → ∀ (h : G ⟶ K), h ≫ f = h ≫ g
j : ι
a : α
p : X a ⟶ K.X j
H :
  Functor.CorepresentableBy (C := HomologicalComplex.{v, u, w} C c)
    (eval C c j ⋙ Functor.obj coyoneda (Opposite.op (X a))) (evalCompCoyonedaCorepresentative c (X a) j)
⊢ p ≫ f.f j = p ≫ g.f j
have h₁ : Eq (α := evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
  ((Equiv.symm H.homEquiv :
        (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) → evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
      (p ≫ f.f j) :
    evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
  ((Equiv.symm H.homEquiv :
        (a_1 : (eval C c j ⋙ coyoneda.obj (Opposite.op (X a))).obj L) → evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
      (p ≫ g.f j) :
    evalCompCoyonedaCorepresentative c (X a) j ⟶ L)
Tactic: apply H.homEquiv.symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.HomologicalComplex (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type w
c : ComplexShape ι
inst_1 : c.HasNoLoop
inst_2 : HasCoproductsOfShape.{w, u, v} ι C
inst_3 : Preadditive.{v, u} C
inst_4 : HasZeroObject.{v, u} C
X : C
hX : IsSeparator.{v, u} X
φ : (i : ι) → HomologicalComplex.{v, u, w} C c := fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i)
⊢ IsSeparator (C := HomologicalComplex.{v, u, w} C c)
    (∐ fun (i : ι) ↦ separatingFamily c (fun (x : Unit) ↦ X) (PUnit.unit, i))
have refine : IsColimit (J := Discrete (Unit × ι)) (F := Discrete.functor (separatingFamily c fun (x : Unit) ↦ X))
  (Cofan.mk (∐ φ) fun (x : Unit × ι) ↦
    match (motive := (x : Unit × ι) → separatingFamily c (fun (x : Unit) ↦ X) x ⟶ ∐ φ) x with
    | (fst, i) => Sigma.ι φ i)
Tactic: refine isSeparator_of_isColimit_cofan
    (isSeparating_separatingFamily c (X := fun (_ : Unit) ↦ X) (by simpa using hX))
      (c := Cofan.mk (∐ φ) (fun ⟨_, i⟩ ↦ Sigma.ι φ i)) ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Indization (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ ObjectProperty.IsSeparating (C := Ind.{v, u} C) (ObjectProperty.ofObj (Functor.obj Ind.yoneda))
have refine : ∀ (X Y : Ind.{v, u} C) (f g : X ⟶ Y)
  (h : ∀ (G : Ind.{v, u} C), ObjectProperty.ofObj (Functor.obj Ind.yoneda) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g),
  X.colimitPresentationCompYoneda.hom ≫ f = X.colimitPresentationCompYoneda.hom ≫ g
Tactic: refine fun X Y f g h => (cancel_epi (Ind.colimitPresentationCompYoneda X).hom).1 ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Preadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ IsSeparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))
have rw : Functor.Faithful
    (Functor.obj preadditiveCoyoneda (op G) ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier)) ↔
  Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveCoyoneda (op G))
Tactic: rw [isSeparator_iff_faithful_coyoneda_obj, ← whiskering_preadditiveCoyoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Preadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ IsSeparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
have rw : Functor.Faithful
    (preadditiveCoyonedaObj (unop (op G)) ⋙
      forget₂ (ModuleCat (End (unop (op G)))ᵐᵒᵖ) (FC := fun (x1 x2 : ModuleCat (End (unop (op G)))ᵐᵒᵖ) ↦
        LinearMap (R := (End (unop (op G)))ᵐᵒᵖ) (RingHom.id (End (unop (op G)))ᵐᵒᵖ) (↑x1 : Type v) (↑x2 : Type v))
        (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
        (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)) ↔
  Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)ᵐᵒᵖ) (preadditiveCoyonedaObj G)
Tactic: rw [isSeparator_iff_faithful_preadditiveCoyoneda, preadditiveCoyoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Preadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ IsCoseparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveYoneda G)
have rw : Functor.Faithful
    (Functor.obj preadditiveYoneda G ⋙
      forget AddCommGrpCat (FC := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CC :=
        AddCommGrpCat.carrier)) ↔
  Functor.Faithful.{v, v, u, v + 1} (Functor.obj preadditiveYoneda G)
Tactic: rw [isCoseparator_iff_faithful_yoneda_obj, ← whiskering_preadditiveYoneda, Functor.comp_obj,
    Functor.whiskeringRight_obj_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Preadditive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
G : C
⊢ IsCoseparator.{v, u} G ↔ Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)) (preadditiveYonedaObj G)
have rw : Functor.Faithful
    (preadditiveYonedaObj G ⋙
      forget₂ (ModuleCat (End G)) (FC := fun (x1 x2 : ModuleCat (End G)) ↦
        LinearMap (R := End G) (RingHom.id (End G)) (↑x1 : Type v) (↑x2 : Type v)) (CC := ModuleCat.carrier)
        AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦ (↑x1 : Type v) →+ (↑x2 : Type v)) (CD :=
        AddCommGrpCat.carrier)) ↔
  Functor.Faithful.{v, v, u, v + 1} (D := ModuleCat (End G)) (preadditiveYonedaObj G)
Tactic: rw [isCoseparator_iff_faithful_preadditiveYoneda, preadditiveYoneda_obj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
f : freeYoneda X M ⟶ F
⊢ (fun (g : M ⟶ F.obj (op X)) ↦
        ({
            app := fun (Y : Cᵒᵖ) ↦
              Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
            naturality := ⋯ } :
          NatTrans (freeYoneda X M) F))
      ((fun (f : freeYoneda X M ⟶ F) ↦
          Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
            f.app (op X))
        f) =
    f
have w : ∀ (Y : Cᵒᵖ),
  NatTrans.app
      ((fun (g : M ⟶ F.obj (op X)) ↦
          ({
              app := fun (Y : Cᵒᵖ) ↦
                Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
              naturality := sorry } :
            NatTrans (freeYoneda X M) F))
        ((fun (f : freeYoneda X M ⟶ F) ↦
            Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
              f.app (op X))
          f))
      Y =
    f.app Y
Tactic: ext Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F : Functor.{v, v', u, u'} Cᵒᵖ A
f : freeYoneda X M ⟶ F
Y : Cᵒᵖ
⊢ NatTrans.app
      ((fun (g : M ⟶ F.obj (op X)) ↦
          ({
              app := fun (Y : Cᵒᵖ) ↦
                Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
              naturality := ⋯ } :
            NatTrans (freeYoneda X M) F))
        ((fun (f : freeYoneda X M ⟶ F) ↦
            Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M) (𝟙 (unop (op X))) ≫
              f.app (op X))
          f))
      Y =
    f.app Y
have w : ∀ (φ : Functor.obj (Functor.obj yoneda X) Y),
  CategoryStruct.comp (Y := sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
      (Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ :
        M ⟶ sigmaObj.{v, v', u'} fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M)
      (NatTrans.app
          ((fun (g : M ⟶ F.obj (op X)) ↦
              ({
                  app := fun (Y : Cᵒᵖ) ↦
                    Sigma.desc fun (φ : Functor.obj (Functor.obj yoneda X) Y) ↦ g ≫ F.map (Quiver.Hom.op φ),
                  naturality := sorry } :
                NatTrans (freeYoneda X M) F))
            ((fun (f : freeYoneda X M ⟶ F) ↦
                Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) (op X)) ↦ M)
                    (𝟙 (unop (op X))) ≫
                  f.app (op X))
              f))
          Y :
        Functor.obj.{v, v', u, u'} (freeYoneda X M) Y ⟶ F.obj Y) =
    Sigma.ι.{v, v', u'} (C := A) (fun (i : Functor.obj (Functor.obj yoneda X) Y) ↦ M) φ ≫ f.app Y
Tactic: refine Sigma.hom_ext _ _ (fun φ ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
X : C
M : A
F G : Functor.{v, v', u, u'} Cᵒᵖ A
α : M ⟶ F.obj (op X)
f : F ⟶ G
⊢ Eq (α := freeYoneda X M ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ F.obj (op X)) → freeYoneda X M ⟶ F) α ≫ f : freeYoneda X M ⟶ G)
    ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ G.obj (op X)) → freeYoneda X M ⟶ G) (α ≫ f.app (op X)) :
      freeYoneda X M ⟶ G)
have a : Eq.{v' + 1} (α := M ⟶ G.obj (op X))
  ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
      ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ F.obj (op X)) → freeYoneda X M ⟶ F) α ≫ f) :
    M ⟶ G.obj (op X))
  ((freeYonedaHomEquiv : (a : freeYoneda X M ⟶ G) → M ⟶ G.obj (op X))
      ((Equiv.symm freeYonedaHomEquiv : (a : M ⟶ G.obj (op X)) → freeYoneda X M ⟶ G) (α ≫ f.app (op X))) :
    M ⟶ G.obj (op X))
Tactic: apply freeYonedaHomEquiv.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
⊢ f = g
have w : ∀ (X : C), Eq (α := F.obj (op X) ⟶ G.obj (op X)) (f.app (op X)) (g.app (op X))
Tactic: ext ⟨X⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
⊢ Eq (α := F.obj (op X) ⟶ G.obj (op X)) (f.app (op X)) (g.app (op X))
have w : ∀ (G_1 : A), ObjectProperty.ofObj.{v', u', w} S G_1 → ∀ (h : G_1 ⟶ F.obj (op X)), h ≫ f.app (op X) = h ≫ g.app (op X)
Tactic: refine hS _ _ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Presheaf (goal)
Goal:
C : Type u
inst : Category.{v, u} C
A : Type u'
inst_1 : Category.{v', u'} A
inst_2 : HasCoproducts.{v, v', u'} A
ι : Type w
S : ι → A
hS : ObjectProperty.IsSeparating.{v', u'} (ObjectProperty.ofObj S)
F G : Functor.{v, v', u, u'} Cᵒᵖ A
f g : F ⟶ G
h :
  ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
    ObjectProperty.ofObj
        (fun (x : C × ι) ↦
          match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
          | (X, i) => freeYoneda X (S i))
        G_1 →
      ∀ (h : G_1 ⟶ F), h ≫ f = h ≫ g
X : C
i : ι
α : S i ⟶ F.obj (op X)
⊢ α ≫ f.app (op X) = α ≫ g.app (op X)
have w : Eq (α := freeYoneda X (S i) ⟶ G)
  ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ f.app (op X)) :
    freeYoneda X (S i) ⟶ G)
  ((Equiv.symm freeYonedaHomEquiv : (a : S i ⟶ G.obj (op X)) → freeYoneda X (S i) ⟶ G) (α ≫ g.app (op X)) :
    freeYoneda X (S i) ⟶ G)
Tactic: apply freeYonedaHomEquiv.symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Sheaf (goal)
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
⊢ f = g
have refine : ∀ (G_1 : Functor.{v, v', u, u'} Cᵒᵖ A),
  ObjectProperty.ofObj
      (fun (x : C × ι) ↦
        match (motive := C × ι → Functor.{v, v', u, u'} Cᵒᵖ A) x with
        | (X, i) => Presheaf.freeYoneda X (S i))
      G_1 →
    ∀ (h : G_1 ⟶ Functor.obj (sheafToPresheaf J A) F),
      h ≫ Functor.map (sheafToPresheaf J A) f = h ≫ Functor.map (sheafToPresheaf J A) g
Tactic: refine (sheafToPresheaf J A).map_injective (Presheaf.isSeparating C hS _ _ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Sheaf (goal)
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
⊢ a ≫ Functor.map (sheafToPresheaf J A) f = a ≫ Functor.map (sheafToPresheaf J A) g
have a₁ : 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: apply ((sheafificationAdjunction _ _).homEquiv _ _).symm.injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
have 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
Tactic: refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ 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
have 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 = ⊤
Tactic: refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ IsIso i
have refine_1 : Subobject.mk i = ⊤
Tactic: rw [Subobject.isIso_iff_mk_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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 = ⊤
have refine_1 : ∀ (G : C) (hG : P G) (g : G ⟶ Y), (Subobject.mk i).Factors g
Tactic: refine hS₂ _ (fun G hG g ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ A = ⊤
have refine_2 : IsIso A.arrow
Tactic: rw [← Subobject.isIso_arrow_iff_eq_top]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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 ≠ ⊤
⊢ ∃ (G : C) (_ : P G) (f : G ⟶ X), ¬A.Factors f
have by_contra! : ∀ (this : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ ∃ (G : C) (_ : P G) (g : G ⟶ Y), ∀ (f : G ⟶ X), f ≫ i ≠ g
have by_contra! : ∀ (this : ∀ (G : C), P G → ∀ (g : G ⟶ Y), ∃ (f : G ⟶ X), f ≫ i = g), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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.IsStrongGenerator
have 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
Tactic: rw [isStrongGenerator_iff]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
have 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
Tactic: refine ⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.StrongGenerator (goal)
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
⊢ 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
have 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
Tactic: refine ⟨IsSeparating.mk_of_exists_epi.{w} (fun X ↦ ?_), fun X Y i _ hi ↦ ?_⟩