awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
A : C
h_1 : P A
⊢ Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) X)) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op A)) f)) :
      (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj X)) →
        (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj Y))

Tactic:
(h A).2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
h : ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
A : C
h_1 : P A
⊢ Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) X)) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op A)) Y))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op A)) f)) :
      (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj X)) →
        (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op A)).obj Y))

Tactic:
exact (h A).2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
⊢ IsIso f

Tactic:
hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
mpr : ∀ (A : C) (hA : P A) (g : A ⟶ Y), ∃ (x : A ⟶ X), x ≫ f = g
mpr₁ : ∀ (A : C) (hA : P A) (g : A ⟶ Y) (y₁ y₂ : A ⟶ X), y₁ ≫ f = g → y₂ ≫ f = g → y₁ = y₂
⊢ IsIso f

Tactic:
refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
A : C
hA : P A
g : A ⟶ Y
⊢ ∃ (x : A ⟶ X), x ≫ f = g

Tactic:
hf A hA g
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
A : C
hA : P A
g : A ⟶ Y
⊢ ∃ (x : A ⟶ X), x ≫ f = g

Tactic:
exact hf A hA g
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : C
f : X ⟶ Y
inst_1 : Mono f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) X)) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj coyoneda (op G)) Y))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) f)) :
          (a : (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj X)) →
            (fun (X : Type v₁) ↦ X) ((coyoneda.obj (op G)).obj Y))
A : C
hA : P A
g : A ⟶ Y
l₁ l₂ : A ⟶ X
h₁ : l₁ ≫ f = g
h₂ : l₂ ≫ f = g
mpr : l₁ ≫ f = l₂ ≫ f
mpr₁ : g = l₂ ≫ f
mpr₂ mpr₃ : g = g
⊢ l₁ = l₂

Tactic:
rw [← cancel_mono f, h₁, h₂]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
mp :
  IsIso f →
    ∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
            (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
mpr :
  (∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
            (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))) →
    IsIso f
⊢ IsIso f ↔
    ∀ (G : C),
      P G →
        Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
          (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
          (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
            (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
              (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : IsIso f
⊢ ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x

Tactic:
rw [isIso_iff_coyoneda_map_bijective] at h

Premises used: CategoryTheory.isIso_iff_coyoneda_map_bijective
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
A : C
mp :
  P A →
    Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op Y))) (β :=
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op X)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda A) f.op)) :
        (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op X)))
⊢ P A →
    Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op Y))) (β :=
      (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op X)))
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda A) f.op)) :
        (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op X)))

Tactic:
_
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
A : C
h_1 : P A
⊢ Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op Y))) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op X)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda A) f.op)) :
      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op X)))

Tactic:
(h A).2

Premises used: Quiver.Hom.unop, And.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
h : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
A : C
h_1 : P A
⊢ Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op Y))) (β :=
    (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda A) (op X)))
    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda A) f.op)) :
      (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op Y))) → (fun (X : Type v₁) ↦ X) ((yoneda.obj A).obj (op X)))

Tactic:
exact (h A).2

Premises used: And.right
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
⊢ IsIso f

Tactic:
hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
mpr : ∀ (A : C) (hA : P A) (g : X ⟶ A), ∃ (x : Y ⟶ A), f ≫ x = g
mpr₁ : ∀ (A : C) (hA : P A) (g : X ⟶ A) (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂
⊢ IsIso f

Tactic:
refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)

Premises used: existsUnique_of_exists_of_unique
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
A : C
hA : P A
g : X ⟶ A
⊢ ∃ (x : Y ⟶ A), f ≫ x = g

Tactic:
hf A hA g

Premises used: Quiver.Hom.unop
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
A : C
hA : P A
g : X ⟶ A
⊢ ∃ (x : Y ⟶ A), f ≫ x = g

Tactic:
exact hf A hA g
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCodetecting
X Y : C
f : X ⟶ Y
inst_1 : Epi f
hf :
  ∀ (G : C),
    P G →
      Function.Surjective (α := (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op Y))) (β :=
        (fun (X : Type v₁) ↦ X) (Functor.obj (Functor.obj yoneda G) (op X)))
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) f.op)) :
          (a : (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op Y))) →
            (fun (X : Type v₁) ↦ X) ((yoneda.obj G).obj (op X)))
A : C
hA : P A
g : X ⟶ A
l₁ l₂ : Y ⟶ A
h₁ : f ≫ l₁ = g
h₂ : f ≫ l₂ = g
mpr : f ≫ l₁ = f ≫ l₂
mpr₁ : g = f ≫ l₂
mpr₂ mpr₃ : g = g
⊢ l₁ = l₂

Tactic:
rw [← cancel_epi f, h₁, h₂]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
⊢ P.IsCoseparating → P.IsCodetecting

Tactic:
simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting

Premises used: CategoryTheory.ObjectProperty.isDetecting_op_iff, CategoryTheory.ObjectProperty.IsSeparating.isDetecting, CategoryTheory.ObjectProperty.isSeparating_op_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : HasEqualizers.{v₁, u₁} C
inst_2 : Balanced.{v₁, u₁} C
⊢ P.IsDetecting ↔ P.IsSeparating

Tactic:
⟨IsDetecting.isSeparating, IsSeparating.isDetecting⟩

Premises used: CategoryTheory.ObjectProperty.IsDetecting.isSeparating, CategoryTheory.ObjectProperty.IsSeparating.isDetecting, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : HasCoequalizers.{v₁, u₁} C
inst_2 : Balanced.{v₁, u₁} C
⊢ P.IsCodetecting ↔ P.IsCoseparating

Tactic:
⟨IsCodetecting.isCoseparating, IsCoseparating.isCodetecting⟩

Premises used: CategoryTheory.ObjectProperty.IsCodetecting.isCoseparating, CategoryTheory.ObjectProperty.IsCoseparating.isCodetecting, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsSeparating
Q : ObjectProperty.{v₁, u₁} C
h : P ≤ Q
⊢ Q.IsSeparating

Tactic:
fun _ _ _ _ hfg => hP _ _ fun _ hG _ => hfg _ (h _ hG) _

Premises used: CategoryTheory.ObjectProperty.IsSeparating
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsCoseparating
Q : ObjectProperty.{v₁, u₁} C
h : P ≤ Q
⊢ Q.IsCoseparating

Tactic:
fun _ _ _ _ hfg => hP _ _ fun _ hG _ => hfg _ (h _ hG) _

Premises used: CategoryTheory.ObjectProperty.IsCoseparating
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
Q : ObjectProperty.{v₁, u₁} C
h : P ≤ Q
⊢ Q.IsDetecting

Tactic:
fun _ _ _ hf => hP _ fun _ hG _ => hf _ (h _ hG) _

Premises used: CategoryTheory.ObjectProperty.IsDetecting
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h𝒢 : P.IsCodetecting
Q : ObjectProperty.{v₁, u₁} C
h : P ≤ Q
⊢ Q.IsCodetecting

Tactic:
fun _ _ _ hf => h𝒢 _ fun _ hG _ => hf _ (h _ hG) _

Premises used: CategoryTheory.ObjectProperty.IsCodetecting
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : IsSeparating.{v₁, u₁} (C := C) ⊥
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ x), h ≫ x_2 = h ≫ x_3

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Quiver.IsThin.{u₁, v₁} C
⊢ IsSeparating.{v₁, u₁} (C := C) ⊥

Tactic:
fun _ _ _ _ _ ↦ Subsingleton.elim _ _

Premises used: CategoryTheory.ObjectProperty.IsSeparating, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : IsCoseparating.{v₁, u₁} (C := C) ⊥
x x_1 : C
x_2 x_3 : x ⟶ x_1
⊢ ∀ (G : C), ⊥ G → ∀ (h : x_1 ⟶ G), x_2 ≫ h = x_3 ≫ h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Quiver.IsThin.{u₁, v₁} C
⊢ IsCoseparating.{v₁, u₁} (C := C) ⊥

Tactic:
fun _ _ _ _ _ ↦ Subsingleton.elim _ _

Premises used: CategoryTheory.ObjectProperty.IsCoseparating, Subsingleton.elim
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : IsDetecting.{v₁, u₁} (C := C) ⊥
X Y : C
f : X ⟶ Y
⊢ ∀ (G : C), ⊥ G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsGroupoid.{v₁, u₁} C
⊢ IsDetecting.{v₁, u₁} (C := C) ⊥

Tactic:
fun _ _ _ _ ↦ inferInstance

Premises used: inferInstance, CategoryTheory.ObjectProperty.IsDetecting
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
h : IsCodetecting.{v₁, u₁} (C := C) ⊥
X Y : C
f : X ⟶ Y
⊢ ∀ (G : C), ⊥ G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : IsGroupoid.{v₁, u₁} C
⊢ IsCodetecting.{v₁, u₁} (C := C) ⊥

Tactic:
fun _ _ _ _ ↦ inferInstance

Premises used: CategoryTheory.ObjectProperty.IsCodetecting, inferInstance
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (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
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
obtain :
  ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Cofan.{w, v₁, u₁} s) (hc : IsColimit c) (p : c.pt ⟶ X),
    Epi p → f = g
⊢ f = g

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

Premises used: CategoryTheory.ObjectProperty.ι
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (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
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v₁, u₁} s
hc : IsColimit c
p : c.pt ⟶ X
h_1 : Epi p
rw : p ≫ f = p ≫ g
⊢ f = g

Tactic:
rw [← cancel_epi p]

Premises used: CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (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
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v₁, u₁} s
hc : IsColimit c
p : c.pt ⟶ X
h_1 : Epi p
i : ι
⊢ c.inj i ≫ p ≫ f = c.inj i ≫ p ≫ g

Tactic:
simpa using h _ (hs i) (c.inj i ≫ p)

Premises used: CategoryTheory.Limits.Cofan.inj, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (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
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Cofan.{w, v₁, u₁} s
hc : IsColimit c
p : c.pt ⟶ X
h_1 : Epi p
⊢ p ≫ f = p ≫ g

Tactic:
exact Cofan.IsColimit.hom_ext hc _ _
    (fun i ↦ by simpa using h _ (hs i) (c.inj i ≫ p))

Premises used: CategoryTheory.Limits.Cofan.IsColimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (x : IsLimit c) (j : X ⟶ c.pt), Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
obtain :
  ∀ (ι : Type w) (s : ι → C) (hs : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (hc : IsLimit c) (j : Y ⟶ c.pt),
    Mono j → f = g
⊢ f = g

Tactic:
obtain ⟨ι, s, hs, c, hc, j, _⟩ := hP Y

Premises used: CategoryTheory.ObjectProperty.ι
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (x : IsLimit c) (j : X ⟶ c.pt), Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan.{w, v₁, u₁} s
hc : IsLimit c
j : Y ⟶ c.pt
h_1 : Mono j
rw : f ≫ j = g ≫ j
⊢ f = g

Tactic:
rw [← cancel_mono j]

Premises used: CategoryTheory.cancel_mono
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (x : IsLimit c) (j : X ⟶ c.pt), Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan.{w, v₁, u₁} s
hc : IsLimit c
j : Y ⟶ c.pt
h_1 : Mono j
i : ι
⊢ (f ≫ j) ≫ c.proj i = (g ≫ j) ≫ c.proj i

Tactic:
simpa using h _ (hs i) (j ≫ c.proj i)

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP :
  ∀ (X : C),
    ∃ (ι : Type w) (s : ι → C) (_ : ∀ (i : ι), P (s i)) (c : Fan.{w, v₁, u₁} s) (x : IsLimit c) (j : X ⟶ c.pt), Mono j
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
ι : Type w
s : ι → C
hs : ∀ (i : ι), P (s i)
c : Fan.{w, v₁, u₁} s
hc : IsLimit c
j : Y ⟶ c.pt
h_1 : Mono j
⊢ f ≫ j = g ≫ j

Tactic:
exact Fan.IsLimit.hom_ext hc _ _
    (fun i ↦ by simpa using h _ (hs i) (j ≫ c.proj i))

Premises used: CategoryTheory.Limits.Fan.IsLimit.hom_ext
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : ∀ (X : C), ∃ (J : Type w) (x : Category.{w', w} J), colimitsOfShape.{w', w, v₁, u₁} P J X
X Y : C
f g : X ⟶ Y
h : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
obtain : ∀ (J : Type w) (w : Category.{w', w} J) (p : ColimitOfShape.{w', w, v₁, u₁} P J X), f = g
⊢ f = g

Tactic:
obtain ⟨J, _, ⟨p⟩⟩ := hP X