awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)
⊢ IsSeparator.{v₁, u₁} (unop G) ↔ IsCoseparator.{v₁, u₁} G
have rw₂ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
  IsSeparating.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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))
⊢ IsSeparator.{v₁, u₁} (unop G) ↔ IsCoseparator.{v₁, u₁} G
have rw₃ : IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsSeparating.{v₁, u₁} (ObjectProperty.singleton (unop G))
Tactic: rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsDetector.{v₁, u₁} (op G) ↔ IsCodetector.{v₁, u₁} G
have rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetector.{v₁, u₁} G
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetector.{v₁, u₁} G
⊢ IsDetector.{v₁, u₁} (op G) ↔ IsCodetector.{v₁, u₁} G
have rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)
⊢ IsDetector.{v₁, u₁} (op G) ↔ IsCodetector.{v₁, u₁} G
have rw₂ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
  IsDetecting.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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))
⊢ IsDetector.{v₁, u₁} (op G) ↔ IsCodetector.{v₁, u₁} G
have rw₃ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton (op G))
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
⊢ IsCodetector.{v₁, u₁} (op G) ↔ IsDetector.{v₁, u₁} G
have rw : IsCodetector.{v₁, u₁} (op G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCodetector.{v₁, u₁} (op G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCodetector.{v₁, u₁} (op G) ↔ IsDetector.{v₁, u₁} G
have rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCodetector.{v₁, u₁} (op G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCodetector.{v₁, u₁} (op G) ↔ IsDetector.{v₁, u₁} G
have rw₂ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
  IsCodetecting.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
rw : IsCodetector.{v₁, u₁} (op G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔
    IsCodetecting.{v₁, u₁} (ObjectProperty.op (ObjectProperty.singleton G))
⊢ IsCodetector.{v₁, u₁} (op G) ↔ IsDetector.{v₁, u₁} G
have rw₃ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (op G))
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, op_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsCodetector.{v₁, u₁} (unop G) ↔ IsDetector.{v₁, u₁} G
have rw : IsCodetector.{v₁, u₁} (unop G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCodetector.{v₁, u₁} (unop G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCodetector.{v₁, u₁} (unop G) ↔ IsDetector.{v₁, u₁} G
have rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCodetector.{v₁, u₁} (unop G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsCodetector.{v₁, u₁} (unop G) ↔ IsDetector.{v₁, u₁} G
have rw₂ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
  IsCodetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsCodetector.{v₁, u₁} (unop G) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₁ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsCodetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
⊢ IsCodetector.{v₁, u₁} (unop G) ↔ IsDetector.{v₁, u₁} G
have rw₃ : IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton (unop G))
Tactic: rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
⊢ IsDetector.{v₁, u₁} (unop G) ↔ IsCodetector.{v₁, u₁} G
have rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetector.{v₁, u₁} G
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetector.{v₁, u₁} G
⊢ IsDetector.{v₁, u₁} (unop G) ↔ IsCodetector.{v₁, u₁} G
have rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetector.{v₁, u₁} G
rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
⊢ IsDetector.{v₁, u₁} (unop G) ↔ IsCodetector.{v₁, u₁} G
have rw₂ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
  IsDetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : Cᵒᵖ
rw : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetector.{v₁, u₁} G
rw₁ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsCodetecting.{v₁, u₁} (ObjectProperty.singleton G)
rw₂ :
  IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔
    IsDetecting.{v₁, u₁} (ObjectProperty.unop (ObjectProperty.singleton G))
⊢ IsDetector.{v₁, u₁} (unop G) ↔ IsCodetector.{v₁, u₁} G
have rw₃ : IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G)) ↔ IsDetecting.{v₁, u₁} (ObjectProperty.singleton (unop G))
Tactic: rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, unop_singleton]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsSeparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : H ⟶ X
⊢ h ≫ f = h ≫ g
have obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : G ⟶ X), h ≫ f = h ≫ g
Tactic: obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
Cleared hypotheses: H, hH, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCoseparator.{v₁, u₁} G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : Y ⟶ H
⊢ f ≫ h = g ≫ h
have obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : Y ⟶ G), f ≫ h = g ≫ h
Tactic: obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
Cleared hypotheses: H, hH, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsDetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : H ⟶ Y
⊢ ∃! h' : H ⟶ X, h' ≫ f = h
have obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Tactic: obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
Cleared hypotheses: H, hH, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
hG : IsCodetector.{v₁, u₁} G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
H : C
hH : ObjectProperty.singleton.{v₁, u₁} G H
h : X ⟶ H
⊢ ∃! h' : Y ⟶ H, f ≫ h' = h
have obtain : ∀ (hH : ObjectProperty.singleton.{v₁, u₁} G G) (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
Tactic: obtain rfl := (ObjectProperty.singleton_iff _ _).1 hH
Cleared hypotheses: H, hH, h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj coyoneda (op G))
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : G ⟶ x), h ≫ x_2 = h ≫ x_3
⊢ Eq (α := Functor.obj (Functor.obj coyoneda (op G)) x ⟶ Functor.obj (Functor.obj coyoneda (op G)) x_1)
    (Functor.map (Functor.obj coyoneda (op G)) x_2) (Functor.map (Functor.obj coyoneda (op G)) x_3)
have h : ∀ (x_4 : Functor.obj (Functor.obj coyoneda (op G)) x),
  TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_2)) x_4 =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj coyoneda (op G)) x_3)) x_4
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
h : Functor.Faithful.{v₁, v₁, u₁, v₁ + 1} (Functor.obj yoneda G)
x x_1 : C
x_2 x_3 : x ⟶ x_1
hfg : ∀ (h : x_1 ⟶ G), x_2 ≫ h = x_3 ≫ h
⊢ Eq (α := Functor.obj (Functor.obj yoneda G) (op x_1) ⟶ Functor.obj (Functor.obj yoneda G) (op x))
    (Functor.map (Functor.obj yoneda G) x_2.op) (Functor.map (Functor.obj yoneda G) x_3.op)
have h : ∀ (x_4 : Functor.obj (Functor.obj yoneda G) (op x_1)),
  TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_2.op)) x_4 =
    TypeCat.Fun.toFun (hom (FC := TypeCat.Fun) (Functor.map (Functor.obj yoneda G) x_3.op)) x_4
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
⊢ IsSeparator.{v₁, u₁} G ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
have rw : (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
  ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
Tactic: rw [isSeparator_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
have refine_1 : ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) (A : C) {Z : C} (u v : A ⟶ Z)
  (huv :
    Eq (α := (∐ fun (f : G ⟶ A) ↦ G) ⟶ Z) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ u) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ v))
  (i : G ⟶ A), i ≫ u = i ≫ v
Tactic: refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
refine_1 :
  ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) (A : C) {Z : C} (u v : A ⟶ Z)
    (huv :
      Eq (α := (∐ fun (f : G ⟶ A) ↦ G) ⟶ Z) ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ u)
        ((Sigma.desc fun (f : G ⟶ A) ↦ f) ≫ v))
    (i : G ⟶ A), i ≫ u = i ≫ v
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔
    ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
have refine_2 : ∀ (h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f))
  (X Y : C) (f g : X ⟶ Y) (hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g), f = g
Tactic: refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
have this : Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)
Tactic: haveI := h X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
G : C
inst_1 : ∀ (A : C), HasCoproduct.{v₁, v₁, u₁} (C := C) fun (x : G ⟶ A) ↦ G
h : ∀ (A : C), Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ A) ↦ G) (Y := A) (Sigma.desc fun (f : G ⟶ A) ↦ f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi.{v₁, u₁} (C := C) (X := ∐ fun (f : G ⟶ X) ↦ G) (Y := X) (Sigma.desc fun (f : G ⟶ X) ↦ f)
⊢ f = g
have refine_2 : ∀ (j : Discrete (G ⟶ X)),
  Eq (α := Functor.obj (Discrete.functor fun (f : G ⟶ X) ↦ G) j ⟶ Y)
    (CategoryStruct.comp (Y := colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
      (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ f))
    (CategoryStruct.comp (Y := colimit.{v₁, v₁, v₁, u₁} (J := Discrete (G ⟶ X)) (Discrete.functor fun (f : G ⟶ X) ↦ G))
      (colimit.ι (Discrete.functor fun (f : G ⟶ X) ↦ G) j) ((Sigma.desc fun (f : G ⟶ X) ↦ f) ≫ g))
Tactic: refine (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ IsCoseparator.{v₁, u₁} G ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
have rw : (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
  ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
Tactic: rw [isCoseparator_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
have refine_1 : ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) (A : C) {Z : C} (u v : Z ⟶ A)
  (huv : Eq (α := Z ⟶ ∏ᶜ fun (f : A ⟶ G) ↦ G) (u ≫ Pi.lift fun (f : A ⟶ G) ↦ f) (v ≫ Pi.lift fun (f : A ⟶ G) ↦ f))
  (i : A ⟶ G), u ≫ i = v ≫ i
Tactic: refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
refine_1 :
  ∀ (h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) (A : C) {Z : C} (u v : Z ⟶ A)
    (huv : Eq (α := Z ⟶ ∏ᶜ fun (f : A ⟶ G) ↦ G) (u ≫ Pi.lift fun (f : A ⟶ G) ↦ f) (v ≫ Pi.lift fun (f : A ⟶ G) ↦ f))
    (i : A ⟶ G), u ≫ i = v ≫ i
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔
    ∀ (A : C), Mono.{v₁, u₁} (C := C) (X := A) (Y := ∏ᶜ fun (f : A ⟶ G) ↦ G) (Pi.lift fun (f : A ⟶ G) ↦ f)
have refine_2 : ∀ (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), f = g
Tactic: refine ⟨fun h A => ⟨fun u v huv => h _ _ fun i => ?_⟩, fun h X Y f g hh => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
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
⊢ f = g
have this : Mono.{v₁, u₁} (C := C) (X := Y) (Y := ∏ᶜ fun (f : Y ⟶ G) ↦ G) (Pi.lift fun (f : Y ⟶ G) ↦ f)
Tactic: haveI := h Y
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)
⊢ f = g
have refine_2 : ∀ (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: refine (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ IsSeparator.{v₁, u₁} c.pt
have rw : ∀ ⦃X Y : C⦄ (f_1 g : X ⟶ Y), (∀ (h : c.pt ⟶ X), h ≫ f_1 = h ≫ g) → f_1 = g
Tactic: rw [isSeparator_def]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
have 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
Tactic: refine fun _ _ _ _ huv ↦ hf _ _ (fun _ h g ↦ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ g ≫ x_2 = g ≫ x_3
have obtain : ∀ (b : β) (g : f b ⟶ x), g ≫ x_2 = g ≫ x_3
Tactic: obtain ⟨b⟩ := h
Cleared hypotheses: x_4, h, g
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)
have 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
Tactic: refine ⟨fun h X Y u v huv => ?_, fun h => isSeparator_of_isColimit_cofan h hc⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
have refine : ∀ (g : c.pt ⟶ X) (b : Discrete β), c.ι.app b ≫ g ≫ u = c.ι.app b ≫ g ≫ v
Tactic: refine h.def _ _ fun g => hc.hom_ext fun b => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)
have 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)
Tactic: refine (isSeparator_iff_of_isColimit_cofan (coprodIsCoprod G H)).trans ?_