awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasProduct.{v₁, v₁, u₁} (C := C) fun (x : A ⟶ G) ↦ G
h : ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono.{v₁, u₁} (C := C) (X := Y) (Y := ∏ᶜ fun (f : Y ⟶ G) ↦ G) (Pi.lift fun (f : Y ⟶ G) ↦ f)
j : Discrete (Y ⟶ G)
⊢ Eq (α := X ⟶ Functor.obj (Discrete.functor fun (f : Y ⟶ G) ↦ G) j)
    (CategoryStruct.comp (Y := limit.{v₁, v₁, v₁, u₁} (J := Discrete (Y ⟶ G)) (Discrete.functor fun (f : Y ⟶ G) ↦ G))
      (f ≫ Pi.lift fun (f : Y ⟶ G) ↦ f) (limit.π (Discrete.functor fun (f : Y ⟶ G) ↦ G) j))
    (CategoryStruct.comp (Y := limit.{v₁, v₁, v₁, u₁} (J := Discrete (Y ⟶ G)) (Discrete.functor fun (f : Y ⟶ G) ↦ G))
      (g ≫ Pi.lift fun (f : Y ⟶ G) ↦ f) (limit.π (Discrete.functor fun (f : Y ⟶ G) ↦ G) j))

Tactic:
simpa using hh j.as

Premises used: CategoryTheory.Discrete.as
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
rw : ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g
⊢ IsSeparator.{v₁, u₁} c.pt

Tactic:
rw [isSeparator_def]

Premises used: CategoryTheory.isSeparator_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g

Tactic:
fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
refine :
  ∀ (x x_1 : C) (x_2 x_3 : x ⟶ x_1) (huv : ∀ (h : c.pt ⟶ x), h ≫ x_2 = h ≫ x_3) (x_4 : C)
    (h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4) (g : x_4 ⟶ x), g ≫ x_2 = g ≫ x_3
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g

Tactic:
refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : c.pt ⟶ x), h ≫ x_2 = h ≫ x_3
x_4 : C
h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4
g : x_4 ⟶ x
obtain : ∀ (b : β) (g : f b ⟶ x), g ≫ x_2 = g ≫ x_3
⊢ g ≫ x_2 = g ≫ x_3

Tactic:
obtain ⟨b⟩ := h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : c.pt ⟶ x), h ≫ x_2 = h ≫ x_3
b : β
g : f b ⟶ x
⊢ g ≫ x_2 = g ≫ x_3

Tactic:
simpa using c.inj b ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

Premises used: Pi.single, CategoryTheory.Limits.Cofan.inj, CategoryTheory.Limits.IsColimit.desc, CategoryTheory.Limits.Cofan.mk
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : c.pt ⟶ x), h ≫ x_2 = h ≫ x_3
b : β
g : f b ⟶ x
⊢ g ≫ x_2 = g ≫ x_3

Tactic:
classical simpa using c.inj b ≫= huv (hc.desc (Cofan.mk _ (Pi.single b g)))

Premises used: CategoryTheory.Limits.Cofan.inj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
⊢ IsSeparator.{v₁, u₁} c.pt ↔ ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩

Premises used: Iff.intro, CategoryTheory.isSeparator_of_isColimit_cofan
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
refine :
  ∀ (h : IsSeparator.{v₁, u₁} c.pt) (X Y : C) (u v : X ⟶ Y)
    (huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v), u = v
⊢ IsSeparator.{v₁, u₁} c.pt ↔ ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
h : IsSeparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v

Tactic:
h.def _ _ fun g => hc.hom_ext fun b => ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.IsSeparator.def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
h : IsSeparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
refine : ∀ (g : c.pt ⟶ X) (b : Discrete β), c.ι.app b ≫ g ≫ u = c.ι.app b ≫ g ≫ v
⊢ u = v

Tactic:
refine h.def _ _ fun g => hc.hom_ext fun b => ?_

Premises used: CategoryTheory.Limits.IsColimit.hom_ext, CategoryTheory.IsSeparator.def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
h : IsSeparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ ObjectProperty.ofObj.{v₁, u₁, w} f (f b.as)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Cofan.{w, v₁, u₁} f
hc : IsColimit c
h : IsSeparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : c.pt ⟶ X
b : Discrete β
⊢ c.ι.app b ≫ g ≫ u = c.ι.app b ≫ g ≫ v

Tactic:
simpa using huv (f b.as) (by simp) (c.inj _ ≫ g)

Premises used: CategoryTheory.Discrete.as, CategoryTheory.Limits.Cofan.inj, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
⊢ IsSeparator.{v₁, u₁} (sigmaObj.{w, v₁, u₁} f) ↔ ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
isSeparator_iff_of_isColimit_cofan (hc := colimit.isColimit _)

Premises used: CategoryTheory.Limits.colimit.isColimit, CategoryTheory.Limits.colimit, CategoryTheory.isSeparator_iff_of_isColimit_cofan
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ IsSeparator.{v₁, u₁} (coprod.{v₁, u₁} G H) ↔ ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
(isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.Limits.colimit, CategoryTheory.isSeparator_iff_of_isColimit_cofan, Iff.trans
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
refine :
  ObjectProperty.IsSeparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.pair G H)
⊢ IsSeparator.{v₁, u₁} (coprod.{v₁, u₁} G H) ↔ ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_

Premises used: CategoryTheory.Limits.coprodIsCoprod, CategoryTheory.isSeparator_iff_of_isColimit_cofan, Iff.trans
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ ObjectProperty.IsSeparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsSeparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
h :
  Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
⊢ ObjectProperty.IsSeparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsSeparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
h :
  ∀ (X : C),
    ObjectProperty.pair.{v₁, u₁} G H X ↔
      ObjectProperty.ofObj.{v₁, u₁, 0}
        (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X
⊢ Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)

Tactic:
ext X
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
⊢ ObjectProperty.pair.{v₁, u₁} G H X ↔
    ObjectProperty.ofObj.{v₁, u₁, 0}
      (fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) X

Tactic:
simp only [ObjectProperty.pair_iff, ObjectProperty.ofObj_iff]

Premises used: CategoryTheory.ObjectProperty.ofObj_iff, CategoryTheory.ObjectProperty.pair_iff
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
X : C
h : G = X ∨ H = X → ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X
h₁ : (∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X) → G = X ∨ H = X
⊢ G = X ∨ H = X ↔ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = X

Tactic:
constructor
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = G

Tactic:
⟨.left, rfl⟩

Premises used: Exists.intro, CategoryTheory.Limits.WalkingPair.left, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = H

Tactic:
⟨.right, rfl⟩

Premises used: CategoryTheory.Limits.WalkingPair.right, Exists.intro, rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
⊢ ∃ (i : WalkingPair), WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H i = G

Tactic:
exacts [⟨.left, rfl⟩, ⟨.right, rfl⟩]
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
h h₁ :
  ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left →
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.left

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
h h₁ h₂ h₃ h₄ :
  ¬G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right →
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right
⊢ G = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right ∨
    H = WalkingPair.rec (motive := fun (x : WalkingPair) ↦ C) G H WalkingPair.right

Tactic:
tauto
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
hG : IsSeparator.{v₁, u₁} G
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton G) (ObjectProperty.pair G H)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryCoproduct.{v₁, u₁} G H
hH : IsSeparator.{v₁, u₁} H
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton H) (ObjectProperty.pair G H)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
hS : IsSeparating.{v₁, u₁} (ofObj f)
⊢ IsSeparator.{v₁, u₁} (sigmaObj.{w, v₁, u₁} f)

Tactic:
(isSeparator_sigma _).2 hS

Premises used: Iff.mpr, CategoryTheory.isSeparator_sigma
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
inst_2 : HasCoproduct.{w, v₁, u₁} f
b : β
hb : IsSeparator.{v₁, u₁} (f b)
⊢ LE.le (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.singleton (f b)) (ObjectProperty.ofObj f)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
rw : ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g
⊢ IsCoseparator.{v₁, u₁} c.pt

Tactic:
rw [isCoseparator_def]

Premises used: CategoryTheory.isCoseparator_def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g

Tactic:
fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
refine :
  ∀ (x x_1 : C) (x_2 x_3 : x ⟶ x_1) (huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h) (x_4 : C)
    (h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4) (g : x_1 ⟶ x_4), x_2 ≫ g = x_3 ≫ g
⊢ ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : Y ⟶ c.pt), f_1 ≫ h = g ≫ h) → f_1 = g

Tactic:
refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h
x_4 : C
h : ObjectProperty.ofObj.{v₁, u₁, w} f x_4
g : x_1 ⟶ x_4
obtain : ∀ (b : β) (g : x_1 ⟶ f b), x_2 ≫ g = x_3 ≫ g
⊢ x_2 ≫ g = x_3 ≫ g

Tactic:
obtain ⟨b⟩ := h
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h
b : β
g : x_1 ⟶ f b
⊢ x_2 ≫ g = x_3 ≫ g

Tactic:
simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Limits.Fan.mk, Pi.single, CategoryTheory.Limits.IsLimit.lift
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
hf : ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
x x_1 : C
x_2 x_3 : x ⟶ x_1
huv : ∀ (h : x_1 ⟶ c.pt), x_2 ≫ h = x_3 ≫ h
b : β
g : x_1 ⟶ f b
⊢ x_2 ≫ g = x_3 ≫ g

Tactic:
classical simpa using huv (hc.lift (Fan.mk _ (Pi.single b g))) =≫ c.proj b

Premises used: CategoryTheory.Limits.Fan.proj
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
⊢ IsCoseparator.{v₁, u₁} c.pt ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
⟨fun h X Y u v huv => ?_, fun h => isCoseparator_of_isLimit_fan h hc⟩

Premises used: CategoryTheory.isCoseparator_of_isLimit_fan, Iff.intro
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
refine :
  ∀ (h : IsCoseparator.{v₁, u₁} c.pt) (X Y : C) (u v : X ⟶ Y)
    (huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h), u = v
⊢ IsCoseparator.{v₁, u₁} c.pt ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
refine ⟨fun h X Y u v huv => ?_, fun h => isCoseparator_of_isLimit_fan h hc⟩
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
h : IsCoseparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v

Tactic:
h.def _ _ fun g => hc.hom_ext fun b => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.IsCoseparator.def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
h : IsCoseparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
refine : ∀ (g : Y ⟶ c.pt) (b : Discrete β), (u ≫ g) ≫ c.π.app b = (v ≫ g) ≫ c.π.app b
⊢ u = v

Tactic:
refine h.def _ _ fun g => hc.hom_ext fun b => ?_

Premises used: CategoryTheory.Limits.IsLimit.hom_ext, CategoryTheory.IsCoseparator.def
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
h : IsCoseparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ ObjectProperty.ofObj.{v₁, u₁, w} f (f b.as)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
c : Fan.{w, v₁, u₁} f
hc : IsLimit c
h : IsCoseparator.{v₁, u₁} c.pt
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), ObjectProperty.ofObj.{v₁, u₁, w} f G → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ c.pt
b : Discrete β
⊢ (u ≫ g) ≫ c.π.app b = (v ≫ g) ≫ c.π.app b

Tactic:
simpa using huv (f b.as) (by simp) (g ≫ c.proj _)

Premises used: CategoryTheory.Limits.Fan.proj, CategoryTheory.Discrete.as, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
β : Type w
f : β → C
inst_2 : HasProduct.{w, v₁, u₁} f
⊢ IsCoseparator.{v₁, u₁} (piObj.{w, v₁, u₁} f) ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.ofObj f)

Tactic:
isCoseparator_iff_of_isLimit_fan (hc := limit.isLimit _)

Premises used: CategoryTheory.Limits.limit.isLimit, CategoryTheory.Limits.limit, CategoryTheory.isCoseparator_iff_of_isLimit_fan
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ IsCoseparator.{v₁, u₁} (Limits.prod.{v₁, u₁} G H) ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
(isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_

Premises used: CategoryTheory.Limits.limit, CategoryTheory.Limits.prodIsProd, Iff.trans, CategoryTheory.isCoseparator_iff_of_isLimit_fan
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
refine :
  ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)
⊢ IsCoseparator.{v₁, u₁} (Limits.prod.{v₁, u₁} G H) ↔ ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
refine (isCoseparator_iff_of_isLimit_fan (prodIsProd G H)).trans ?_

Premises used: CategoryTheory.Limits.prodIsProd, Iff.trans, CategoryTheory.isCoseparator_iff_of_isLimit_fan
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
⊢ ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.CategoryTheory.Generator.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : HasZeroMorphisms.{v₁, u₁} C
G H : C
inst_2 : HasBinaryProduct.{v₁, u₁} G H
h :
  Eq (α := ObjectProperty.{v₁, u₁} C) (ObjectProperty.pair G H)
    (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H)
⊢ ObjectProperty.IsCoseparating.{v₁, u₁} (C := C)
      (ObjectProperty.ofObj fun (j : WalkingPair) ↦ WalkingPair.casesOn (motive := fun (x : WalkingPair) ↦ C) j G H) ↔
    ObjectProperty.IsCoseparating.{v₁, u₁} (ObjectProperty.pair G H)

Tactic:
convert! Iff.rfl

Premises used: Iff.rfl