awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S U : Set (Aut F)
hU : U ⊆ S
hUopen : IsOpen U
hUone : 1 ∈ U
I : Set C
w : Fintype (↑I : Type u₁)
hc : ∀ X ∈ I, IsConnected.{u₁, u₂} X
hmem : ∀ (σ : Aut F), (∀ (X : (↑I : Type u₁)), σ.hom.app (↑X : C) = 𝟙 (F.obj (↑X : C))) → σ ∈ U
P : C := piObj.{u₁, u₂, u₁} fun (X : (↑I : Type u₁)) ↦ (↑X : C)
A : C
a : (F.obj A).obj
hgal : IsGalois.{u₁, u₂} A
hbij :
  Function.Bijective.{u₂ + 1, w + 1} (β := (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
    fun (f : A ⟶ P) ↦
    (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (F.map f) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj P))
      a
t : Aut F
ht :
  (@ConcreteCategory.hom _ (ObjectProperty.FullSubcategory.category Finite)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦ TypeCat.Fun X.obj Y.obj)
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj)
          (fun (X Y : ObjectProperty.FullSubcategory Finite) ↦
            (TypeCat.instFunLikeFun : FunLike (TypeCat.Fun X.obj Y.obj) X.obj Y.obj))
          _ _ _ (t.hom.app A) :
        (a : (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A)) →
          (fun (X : ObjectProperty.FullSubcategory Finite) ↦ X.obj) (F.obj A))
      a =
    a
this : ∀ (X : (↑I : Type u₁)), IsConnected.{u₁, u₂} (↑X : C)
⊢ ∀ (X : (↑I : Type u₁)), Nonempty.{w + 1} (F.obj (↑X : C)).obj

Tactic:
haveI (X : I) : Nonempty (F.obj X.val) := nonempty_fiber_of_isConnected F X
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S : Set (Aut F)
X : PointedGaloisObject F
left : True
h : (↑(MulAction.stabilizer (Aut F) X.pt) : Set (Aut F)) ⊆ S
⊢ ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t

Tactic:
⟨MulAction.stabilizer (Aut F) X.pt, h, stabilizer_isOpen (Aut F) X.pt,
        Subgroup.one_mem _⟩

Premises used: CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt, Subgroup.one_mem, SetLike.coe, And.intro, Exists.intro, MulAction.stabilizer, CategoryTheory.Aut, stabilizer_isOpen
-- Module: Mathlib.CategoryTheory.Galois.Topology
Goal:
C : Type u₁
inst : Category.{u₂, u₁} C
F : Functor.{u₂, w, u₁, w + 1} C FintypeCat
inst_1 : GaloisCategory.{u₁, u₂} C
inst_2 : FiberFunctor F
S : Set (Aut F)
X : PointedGaloisObject F
left : True
h : (↑(MulAction.stabilizer (Aut F) X.pt) : Set (Aut F)) ⊆ S
⊢ ∃ t ⊆ S, IsOpen t ∧ 1 ∈ t

Tactic:
exact ⟨MulAction.stabilizer (Aut F) X.pt, h, stabilizer_isOpen (Aut F) X.pt,
        Subgroup.one_mem _⟩
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
⊢ WellPowered.{v, v, u} C

Tactic:
haveI : WellPowered.{v} C := wellPowered_of_isDetector G hG.isDetector
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this : WellPowered.{v, v, u} C
⊢ HasProductsOfShape (Subobject.{v, u} (op G)) C

Tactic:
haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small.{v} _ _
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
⊢ ∃ (G : C), Injective.{v, u} G ∧ IsCoseparator.{v, u} G

Tactic:
⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => ?_⟩

Premises used: Iff.mpr, inferInstance, And.intro, Exists.intro, CategoryTheory.Preadditive.isCoseparator_iff
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
refine : ∀ (X Y : C) (f : X ⟶ Y) (hf : ∀ (h : Y ⟶ T), f ≫ h = 0), f = 0
⊢ ∃ (G : C), Injective.{v, u} G ∧ IsCoseparator.{v, u} G

Tactic:
refine ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0

Tactic:
(Preadditive.isSeparator_iff _).1 hG _ fun h => ?_

Premises used: CategoryTheory.Preadditive.isSeparator_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
refine : ∀ (h : G ⟶ X), h ≫ f = 0
⊢ f = 0

Tactic:
refine (Preadditive.isSeparator_iff _).1 hG _ fun h => ?_

Premises used: CategoryTheory.Preadditive.isSeparator_iff, Iff.mp
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
rw : CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f)) (Limits.image.ι (h ≫ f)) = 0
rw₁ : Eq (α := G ⟶ Y) (CategoryStruct.comp (Y := image (h ≫ f)) 0 (Limits.image.ι (h ≫ f))) 0
rw₂ rw₃ : Eq.{v + 1} (α := G ⟶ Y) 0 0
⊢ h ≫ f = 0

Tactic:
rw [← Limits.image.fac (h ≫ f), hh, zero_comp]

Premises used: CategoryTheory.Limits.image.fac, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.zero_comp
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
suffices : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
⊢ h ≫ f = 0

Tactic:
suffices hh : factorThruImage (h ≫ f) = 0 by
    rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
rw :
  CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
      (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
    0
rw₁ : (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
rw₂ : h ≫ f ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
rw₃ : Eq (α := G ⟶ T) (h ≫ 0) 0
rw₄ rw₅ : Eq.{v + 1} (α := G ⟶ T) 0 0
⊢ factorThruImage (h ≫ f) ≫ q = 0

Tactic:
rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, CategoryTheory.Limits.image.ι, CategoryTheory.CategoryStruct.comp, CategoryTheory.Limits.image.fac_assoc, CategoryTheory.Injective.comp_factorThru
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
⊢ Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0

Tactic:
exact zero_of_comp_mono q
    (by rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero])

Premises used: CategoryTheory.Limits.zero_of_comp_mono
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasColimits.{v, u} C
inst_3 : EnoughProjectives.{v, u} C
G : C
hG : IsCoseparator.{v, u} G
obtain :
  ∀ (T : Cᵒᵖ) (hT₁ : Injective.{v, u} T) (hT₂ : IsCoseparator.{v, u} T),
    ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G
⊢ ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G

Tactic:
obtain ⟨T, hT₁, hT₂⟩ := has_injective_coseparator (op G) ((isSeparator_op_iff _).2 hG)

Premises used: Iff.mpr, Opposite.op, CategoryTheory.isSeparator_op_iff, CategoryTheory.Abelian.has_injective_coseparator
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasColimits.{v, u} C
inst_3 : EnoughProjectives.{v, u} C
G : C
hG : IsCoseparator.{v, u} G
T : Cᵒᵖ
hT₁ : Injective.{v, u} T
hT₂ : IsCoseparator.{v, u} T
⊢ ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G

Tactic:
⟨unop T, inferInstance, (isSeparator_unop_iff _).2 hT₂⟩

Premises used: Iff.mpr, inferInstance, And.intro, Exists.intro, Opposite.unop, CategoryTheory.isSeparator_unop_iff
-- Module: Mathlib.CategoryTheory.Generator.Abelian
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasColimits.{v, u} C
inst_3 : EnoughProjectives.{v, u} C
G : C
hG : IsCoseparator.{v, u} G
T : Cᵒᵖ
hT₁ : Injective.{v, u} T
hT₂ : IsCoseparator.{v, u} T
⊢ ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G

Tactic:
exact ⟨unop T, inferInstance, (isSeparator_unop_iff _).2 hT₂⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h_1 : P.IsSeparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : P Z
h : Z ⟶ α.inverse.obj X
obtain :
  ∀ (h' : α.functor.obj Z ⟶ X),
    Eq.{v₁ + 1} (α := Z ⟶ α.inverse.obj Y)
      ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map f :
        Z ⟶ α.inverse.obj Y)
      ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map g :
        Z ⟶ α.inverse.obj Y)
⊢ h ≫ α.inverse.map f = h ≫ α.inverse.map g

Tactic:
obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective h

Premises used: CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.surjective, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : P.IsSeparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : P Z
h' : α.functor.obj Z ⟶ X
⊢ Eq.{v₁ + 1} (α := Z ⟶ α.inverse.obj Y)
    ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map f :
      Z ⟶ α.inverse.obj Y)
    ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map g :
      Z ⟶ α.inverse.obj Y)

Tactic:
simp only [Adjunction.homEquiv_unit, Category.assoc, ← Functor.map_comp,
      H _ (P.strictMap_obj _ hZ) h']

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Adjunction.homEquiv_unit, CategoryTheory.ObjectProperty.strictMap_obj, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h_1 : P.IsCoseparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h : α.inverse.obj Y ⟶ Z
obtain :
  ∀ (h' : Y ⟶ α.symm.inverse.obj Z),
    Eq (α := α.inverse.obj X ⟶ Z)
      (α.inverse.map f ≫
        ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')
      (α.inverse.map g ≫
        ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')
⊢ α.inverse.map f ≫ h = α.inverse.map g ≫ h

Tactic:
obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective h

Premises used: CategoryTheory.Equivalence.toAdjunction, CategoryTheory.Adjunction.homEquiv, Equiv.surjective, Equiv.symm, CategoryTheory.Equivalence.symm, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h : P.IsCoseparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h' : Y ⟶ α.symm.inverse.obj Z
⊢ Eq (α := α.inverse.obj X ⟶ Z)
    (α.inverse.map f ≫
      ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')
    (α.inverse.map g ≫
      ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')

Tactic:
simp only [Equivalence.symm_inverse, Equivalence.symm_functor,
      Adjunction.homEquiv_counit, ← Functor.map_comp_assoc,
      H _ (P.strictMap_obj _ hZ) h']

Premises used: CategoryTheory.ObjectProperty.strictMap_obj, CategoryTheory.Functor.map_comp_assoc, CategoryTheory.Equivalence.symm_functor, CategoryTheory.Adjunction.homEquiv_counit, CategoryTheory.Equivalence.symm_inverse
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsSeparating.{v₁, u₁} P.op ↔ P.IsCoseparating

Tactic:
⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsSeparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h),
    f = g
refine_2 :
  ∀ (hP : P.IsCoseparating) (X Y : Cᵒᵖ) (f g : X ⟶ Y) (hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g), f = g
⊢ IsSeparating.{v₁, u₁} P.op ↔ P.IsCoseparating

Tactic:
refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsSeparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsSeparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : G ⟶ op Y), (h ≫ f.op).unop = (h ≫ g.op).unop
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsSeparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop

Tactic:
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
refine_2 : ∀ (G : C) (hG : P G) (h : unop X ⟶ G), (f.unop ≫ h).op = (g.unop ≫ h).op
⊢ f = g

Tactic:
refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : P G
h : unop X ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

Premises used: CategoryTheory.op_comp, Quiver.Hom.op_unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsCoseparating.{v₁, u₁} P.op ↔ P.IsSeparating

Tactic:
⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsCoseparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g),
    f = g
refine_2 :
  ∀ (hP : P.IsSeparating) (X Y : Cᵒᵖ) (f g : X ⟶ Y) (hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h), f = g
⊢ IsCoseparating.{v₁, u₁} P.op ↔ P.IsSeparating

Tactic:
refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCoseparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g

Tactic:
Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCoseparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
refine_1 :
  ∀ (G : Cᵒᵖ) (hG : P.op G) (h : op X ⟶ G),
    Eq (α := unop G ⟶ unop (op Y)) (Quiver.Hom.unop (f.op ≫ h)) (Quiver.Hom.unop (g.op ≫ h))
⊢ f = g

Tactic:
refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : IsCoseparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : P.op G
h : op X ⟶ G
⊢ Eq (α := unop G ⟶ unop (op Y)) (Quiver.Hom.unop (f.op ≫ h)) (Quiver.Hom.unop (g.op ≫ h))

Tactic:
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ hG _

Premises used: Quiver.Hom.unop_op, CategoryTheory.unop_comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g

Tactic:
Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
refine_2 : ∀ (G : C) (hG : P G) (h : G ⟶ unop Y), (h ≫ f.unop).op = (h ≫ g.unop).op
⊢ f = g

Tactic:
refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)

Premises used: Quiver.Hom.op_inj, Quiver.Hom.unop_inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : G ⟶ unop Y
⊢ (h ≫ f.unop).op = (h ≫ g.unop).op

Tactic:
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ hG _

Premises used: CategoryTheory.op_comp, Quiver.Hom.op_unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} Cᵒᵖ
⊢ P.unop.IsCoseparating ↔ IsSeparating.{v₁, u₁} P

Tactic:
P.unop.isSeparating_op_iff.symm

Premises used: CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.isSeparating_op_iff, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} Cᵒᵖ
⊢ P.unop.IsSeparating ↔ IsCoseparating.{v₁, u₁} P

Tactic:
P.unop.isCoseparating_op_iff.symm

Premises used: CategoryTheory.ObjectProperty.isCoseparating_op_iff, CategoryTheory.ObjectProperty.unop, CategoryTheory.ObjectProperty.op, Iff.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsDetecting.{v₁, u₁} P.op ↔ P.IsCodetecting

Tactic:
⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩

Premises used: Iff.intro