awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
h :
  ∀ (b : Subtype P),
    Eq (α :=
      Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
          Subobject.underlying ⊥ ⟶
        (↑b : C))
      ((CategoryStruct.comp (Y := equalizer f g) (Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥) ⋯)
            (equalizer.ι f g) ≫
          Subobject.arrow ⊥) ≫
        Pi.π (Subtype.val (p := P)) b)
      ((𝟙
            (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
              Subobject.underlying ⊥) ≫
          Subobject.arrow ⊥) ≫
        Pi.π (Subtype.val (p := P)) b)
⊢ CategoryStruct.comp (Y := equalizer f g) (Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥) ⋯)
      (equalizer.ι f g) =
    𝟙
      (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥)

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
b : Subtype P
⊢ Eq (α :=
    Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
        Subobject.underlying ⊥ ⟶
      (↑b : C))
    ((CategoryStruct.comp (Y := equalizer f g) (Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥) ⋯)
          (equalizer.ι f g) ≫
        Subobject.arrow ⊥) ≫
      Pi.π (Subtype.val (p := P)) b)
    ((𝟙
          (Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
            Subobject.underlying ⊥) ≫
        Subobject.arrow ⊥) ≫
      Pi.π (Subtype.val (p := P)) b)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} C
inst_2 : WellPowered.{w, v₁, u₁} C
inst_3 : HasLimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsCoseparating
this_1 : HasFiniteLimits.{v₁, u₁} C
this_2 : HasProductsOfShape.{u₁, u₁, v₁} (Subtype P) C
this_3 : ∀ (A : C), HasProductsOfShape (StructuredArrow A P.ι) C
this_4 : CompleteLattice (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P)))) :=
  completeLatticeOfCompleteSemilatticeInf
    (Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
this : ∀ (X : C) [inst_5 : HasProduct (P.productToFamily X)], Mono (Y := ∏ᶜ P.productToFamily X) (P.productTo X)
A : C
f g :
  Functor.obj (C := Subobject.{v₁, u₁} (C := C) (piObj.{u₁, v₁, u₁} (β := Subtype P) (Subtype.val (p := P))))
      Subobject.underlying ⊥ ⟶
    A
⊢ IsSplitEpi (X := equalizer f g) (equalizer.ι f g)

Tactic:
exact IsSplitEpi.mk' ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le, by
      ext
      simp⟩

Premises used: CategoryTheory.Subobject.arrow, CategoryTheory.Limits.equalizer.ι, CategoryTheory.SplitEpi.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Subobject.ofLEMk, bot_le, CategoryTheory.IsSplitEpi.mk'
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst_2 : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst_3 : HasColimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsSeparating
⊢ HasInitial.{v₁, u₁} Cᵒᵖ

Tactic:
haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating (P.isCoseparating_op_iff.2 hP)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst_2 : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst_3 : HasColimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsSeparating
this : HasInitial.{v₁, u₁} Cᵒᵖ
⊢ HasTerminal.{v₁, u₁} C

Tactic:
hasTerminal_of_hasInitial_op

Premises used: CategoryTheory.Limits.hasTerminal_of_hasInitial_op
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : LocallySmall.{w, v₁, u₁} Cᵒᵖ
inst_2 : WellPowered.{w, v₁, u₁} Cᵒᵖ
inst_3 : HasColimitsOfSize.{w, w, v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_4 : ObjectProperty.Small.{w, v₁, u₁} P
hP : P.IsSeparating
this : HasInitial.{v₁, u₁} Cᵒᵖ
⊢ HasTerminal.{v₁, u₁} C

Tactic:
exact hasTerminal_of_hasInitial_op

Premises used: CategoryTheory.Limits.hasTerminal_of_hasInitial_op
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ inv (P.ofLE Q h₁) ≫ P.arrow = Q.arrow

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
this : IsIso (P.ofLE Q h₁)
⊢ P = Q

Tactic:
exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))

Premises used: CategoryTheory.Subobject.le_of_comm, CategoryTheory.Subobject.ofLE, le_antisymm, CategoryTheory.inv
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
suffices : IsIso (P.ofLE Q h₁)
⊢ P = Q

Tactic:
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
⊢ IsIso (P.ofLE Q h₁)

Tactic:
h𝒢 _ fun G hG f => ?_
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
refine :
  ∀ (G : C) (hG : 𝒢 G) (f : G ⟶ Functor.obj underlying Q), ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f
⊢ IsIso (P.ofLE Q h₁)

Tactic:
refine h𝒢 _ fun G hG f => ?_
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
⊢ P.Factors (f ≫ Q.arrow)

Tactic:
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
⊢ ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f

Tactic:
⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩

Premises used: CategoryTheory.Subobject.factorThru, ExistsUnique, And.intro, Exists.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
refine_1 : (fun (h' : G ⟶ Functor.obj underlying P) ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)
refine_2 : ∀ (g : G ⟶ Functor.obj underlying P) (hg : g ≫ P.ofLE Q h₁ = f), g = P.factorThru (f ≫ Q.arrow) this
⊢ ∃! h' : G ⟶ Functor.obj underlying P, h' ≫ P.ofLE Q h₁ = f

Tactic:
refine ⟨factorThru _ _ this, ?_, fun g (hg : g ≫ _ = f) => ?_⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
⊢ (fun (h' : G ⟶ Functor.obj underlying P) ↦ h' ≫ P.ofLE Q h₁ = f) (P.factorThru (f ≫ Q.arrow) this)

Tactic:
simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Category.assoc, CategoryTheory.Subobject.arrow, CategoryTheory.cancel_mono, CategoryTheory.Subobject.factorThru_arrow
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h₁ : P ≤ Q
h₂ : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, Q.Factors f → P.Factors f
G : C
hG : 𝒢 G
f : G ⟶ Functor.obj underlying Q
this : P.Factors (f ≫ Q.arrow)
g : G ⟶ Functor.obj underlying P
hg : g ≫ P.ofLE Q h₁ = f
⊢ g = P.factorThru (f ≫ Q.arrow) this

Tactic:
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc,
      ofLE_arrow, factorThru_arrow]

Premises used: CategoryTheory.Subobject.ofLE_arrow, CategoryTheory.Category.assoc, CategoryTheory.Subobject.arrow, CategoryTheory.Subobject.ofLE, CategoryTheory.cancel_mono, CategoryTheory.Subobject.factorThru_arrow
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f → Q.Factors f
⊢ P ⊓ Q = P

Tactic:
eq_of_le_of_isDetecting h𝒢 _ _ _root_.inf_le_left
    fun _ hG _ hf => (inf_factors _).2 ⟨hf, h _ hG hf⟩

Premises used: Iff.mpr, CategoryTheory.Subobject.eq_of_le_of_isDetecting, CategoryTheory.Subobject.inf_factors, And.intro, inf_le_left
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h : ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f
⊢ P = Q

Tactic:
calc
    P = P ⊓ Q := Eq.symm <| inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).1 hf
    _ = Q ⊓ P := inf_comm ..
    _ = Q := inf_eq_of_isDetecting h𝒢 _ _ fun G hG _ hf => (h G hG).2 hf

Premises used: Iff.mpr, Trans.trans, CategoryTheory.Subobject.inf_eq_of_isDetecting, inf_comm, Iff.mp, Eq.symm
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasPullbacks.{v₁, u₁} C
𝒢 : ObjectProperty.{v₁, u₁} C
inst_2 : ObjectProperty.Small.{w, v₁, u₁} 𝒢
inst_3 : LocallySmall.{w, v₁, u₁} C
h𝒢 : 𝒢.IsDetecting
X : C
P Q : Subobject.{v₁, u₁} X
h :
  Eq (α := Set ((G : Subtype 𝒢) × ((↑G : C) ⟶ X)))
    ((fun (P : Subobject.{v₁, u₁} X) ↦
        ({f : (G : Subtype 𝒢) × ((↑G : C) ⟶ X) | P.Factors (f.snd (β := fun (G : Subtype 𝒢) ↦ (↑G : C) ⟶ X))} :
          Set ((G : Subtype 𝒢) × ((↑G : C) ⟶ X))))
      P)
    ((fun (P : Subobject.{v₁, u₁} X) ↦
        ({f : (G : Subtype 𝒢) × ((↑G : C) ⟶ X) | P.Factors (f.snd (β := fun (G : Subtype 𝒢) ↦ (↑G : C) ⟶ X))} :
          Set ((G : Subtype 𝒢) × ((↑G : C) ⟶ X))))
      Q)
⊢ ∀ (G : C), 𝒢 G → ∀ {f : G ⟶ X}, P.Factors f ↔ Q.Factors f

Tactic:
simpa [Set.ext_iff, Sigma.forall] using h

Premises used: Sigma.forall, Set.ext_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
⊢ (P.inverseImage (proj S T)).IsCoseparating

Tactic:
fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)

Premises used: CategoryTheory.StructuredArrow.ext, CategoryTheory.ObjectProperty.IsCoseparating, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
refine :
  ∀ (X Y : StructuredArrow S T) (f g : X ⟶ Y)
    (hfg : ∀ (G : StructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h) (G : C) (hG : P G)
    (h : Y.right ⟶ G), Hom.right f ≫ h = Hom.right g ≫ h
⊢ (P.inverseImage (proj S T)).IsCoseparating

Tactic:
refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)

Premises used: CategoryTheory.StructuredArrow.ext, CategoryTheory.StructuredArrow.Hom.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : StructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : Y.right ⟶ G
⊢ Hom.right f ≫ h = Hom.right g ≫ h

Tactic:
congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, congr_arg, CategoryTheory.CommaMorphism.right, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : D
T : Functor.{v₁, v₂, u₁, u₂} C D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : StructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : P G
h : Y.right ⟶ G
⊢ Hom.right f ≫ h = Hom.right g ≫ h

Tactic:
exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))

Premises used: CategoryTheory.StructuredArrow.homMk, CategoryTheory.StructuredArrow.hom, CategoryTheory.Functor.map, congr_arg, CategoryTheory.CommaMorphism.right, CategoryTheory.CategoryStruct.comp, CategoryTheory.StructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
⊢ (P.inverseImage (proj S T)).IsSeparating

Tactic:
fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)

Premises used: CategoryTheory.CostructuredArrow.ext, CategoryTheory.CommaMorphism.left, CategoryTheory.ObjectProperty.IsSeparating
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
refine :
  ∀ (X Y : CostructuredArrow S T) (f g : X ⟶ Y)
    (hfg : ∀ (G : CostructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g) (G : C) (hG : P G)
    (h : G ⟶ X.left), h ≫ f.left = h ≫ g.left
⊢ (P.inverseImage (proj S T)).IsSeparating

Tactic:
refine fun X Y f g hfg => ext _ _ (hP _ _ fun G hG h => ?_)

Premises used: CategoryTheory.CostructuredArrow.ext, CategoryTheory.CommaMorphism.left
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : CostructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : P G
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left

Tactic:
congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Functor.map, congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CategoryStruct.comp, CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
S : Functor.{v₁, v₂, u₁, u₂} C D
T : D
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : CostructuredArrow S T), P.inverseImage (proj S T) G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : P G
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left

Tactic:
exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))

Premises used: CategoryTheory.CostructuredArrow.hom, CategoryTheory.CostructuredArrow.homMk, CategoryTheory.Functor.map, congr_arg, CategoryTheory.CommaMorphism.left, CategoryTheory.CategoryStruct.comp, CategoryTheory.CostructuredArrow.mk, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : C
h : IsSeparator.{v₁, u₁} G
α : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ IsSeparator.{v₂, u₂} (α.functor.obj G)

Tactic:
simpa using ObjectProperty.IsSeparating.of_equivalence h α

Premises used: CategoryTheory.ObjectProperty.IsSeparating.of_equivalence
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
G : C
h : IsCoseparator.{v₁, u₁} G
α : Equivalence.{v₁, v₂, u₁, u₂} C D
⊢ IsCoseparator.{v₂, u₂} (α.functor.obj G)

Tactic:
simpa using ObjectProperty.IsCoseparating.of_equivalence h α

Premises used: CategoryTheory.ObjectProperty.IsCoseparating.of_equivalence
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparator.{v₁, u₁} G
rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsSeparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton (op G))
⊢ IsSeparator.{v₁, u₁} (op G) ↔ IsCoseparator.{v₁, u₁} G

Tactic:
rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, op_singleton]

Premises used: CategoryTheory.ObjectProperty.op_singleton, CategoryTheory.IsSeparator, CategoryTheory.IsCoseparator, CategoryTheory.ObjectProperty.isSeparating_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsCoseparating.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (op G))
⊢ IsCoseparator.{v₁, u₁} (op G) ↔ IsSeparator.{v₁, u₁} G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, op_singleton]

Premises used: CategoryTheory.ObjectProperty.isCoseparating_op_iff, CategoryTheory.ObjectProperty.op_singleton, CategoryTheory.IsSeparator, CategoryTheory.IsCoseparator
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCoseparating.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCoseparating.{v₁, u₁} (ObjectProperty.singleton (unop G))
⊢ IsCoseparator.{v₁, u₁} (unop G) ↔ IsSeparator.{v₁, u₁} G

Tactic:
rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, unop_singleton]

Premises used: CategoryTheory.IsSeparator, CategoryTheory.ObjectProperty.isCoseparating_unop_iff, CategoryTheory.IsCoseparator, CategoryTheory.ObjectProperty.unop_singleton
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCoseparator.{v₁, u₁} G
rw₁ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCoseparating.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsSeparating.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G))
⊢ IsSeparator.{v₁, u₁} (unop G) ↔ IsCoseparator.{v₁, u₁} G

Tactic:
rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]

Premises used: CategoryTheory.ObjectProperty.isSeparating_unop_iff, CategoryTheory.IsSeparator, CategoryTheory.IsCoseparator, CategoryTheory.ObjectProperty.unop_singleton
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetector.{v₁, u₁} G
rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsDetecting.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
rw₃ rw₄ :
  IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G))
⊢ IsDetector.{v₁, u₁} (op G) ↔ IsCodetector.{v₁, u₁} G

Tactic:
rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]

Premises used: CategoryTheory.ObjectProperty.isDetecting_op_iff, CategoryTheory.ObjectProperty.op_singleton, CategoryTheory.IsCodetector, CategoryTheory.IsDetector