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
P : ObjectProperty.{v₁, u₁} C
hP : IsCodetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : Cᵒᵖ
hG : P.op G
h : op Y ⟶ G
⊢ ∃! h' : op X ⟶ G, f.op ≫ h' = h
have refine_1 : ∀ (t : unop G ⟶ X) (ht : t ≫ f = h.unop)
  (ht' : ∀ (y : unop G ⟶ X), (fun (h' : unop G ⟶ X) ↦ h' ≫ f = h.unop) y → y = t), ∃! h' : op X ⟶ G, f.op ≫ h' = h
Tactic: obtain ⟨t, ht, ht'⟩ := hf (unop G) hG h.unop
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso f
have refine_2 : ∀ (G : C) (hG : P G) (h : G ⟶ unop X), ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
Tactic: refine (isIso_unop_iff _).1 (hP _ fun G hG h => ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
⊢ ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
have refine_2 : ∀ (t : Y ⟶ op G) (ht : f ≫ t = h.op) (ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t),
  ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
Tactic: obtain ⟨t, ht, ht'⟩ := hf (op G) hG h.op
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
hP : P.IsDetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : C
hG : P G
h : G ⟶ unop X
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y → y = t
⊢ ∃! h' : G ⟶ unop Y, h' ≫ f.unop = h
have refine_2 : ∀ (y : G ⟶ unop Y) (hy : (fun (h' : G ⟶ unop Y) ↦ h' ≫ f.unop = h) y), (fun (h' : Y ⟶ op G) ↦ f ≫ h' = h.op) y.op
Tactic: refine ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ ?_)⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f
have refine_1 : ∀ {Z : C} (g h : Z ⟶ X) (hgh : g ≫ f = h ≫ f) (G : C) (hG : P G) (i : G ⟶ Z), i ≫ g = i ≫ h
Tactic: refine
    (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
refine_1 : ∀ {Z : C} (g h : Z ⟶ X) (hgh : g ≫ f = h ≫ f) (G : C) (hG : P G) (i : G ⟶ Z), i ≫ g = i ≫ h
⊢ IsIso f
have refine_2 : ∀ {Z : C} (g h : Y ⟶ Z) (hgh : f ≫ g = f ≫ h), g = h
Tactic: refine
    (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => hP _ _ fun G hG i => ?_⟩, ⟨fun g h hgh => ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z
⊢ i ≫ g = i ≫ h
have refine_1 : ∀ (t : G ⟶ X) (ht : ∀ (y : G ⟶ X), (fun (h' : G ⟶ X) ↦ h' ≫ f = i ≫ g ≫ f) y → y = t), i ≫ g = i ≫ h
Tactic: obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun (h' : G ⟶ X) ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h
have refine_1 : t = i ≫ h
Tactic: rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Z ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : P G
i : G ⟶ Z
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun (h' : G ⟶ X) ↦ h' ≫ f = i ≫ g ≫ f) y → y = t
refine_1 : t = i ≫ h
⊢ i ≫ g = i ≫ h
have refine_1₁ : t = t
Tactic: rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
⊢ g = h
have refine_2 : ∀ (G : C) (hG : P G) (i : G ⟶ Y), i ≫ g = i ≫ h
Tactic: refine hP _ _ fun G hG i => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
i : G ⟶ Y
⊢ i ≫ g = i ≫ h
have refine_2 : ∀ (t : G ⟶ X), (t ≫ f) ≫ g = (t ≫ f) ≫ h
Tactic: obtain ⟨t, rfl, -⟩ := hf G hG i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h
have refine_2 : t ≫ f ≫ g = (t ≫ f) ≫ h
Tactic: rw [Category.assoc, hgh, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
refine_2 : t ≫ f ≫ g = (t ≫ f) ≫ h
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h
have refine_2₁ : t ≫ f ≫ h = (t ≫ f) ≫ h
Tactic: rw [Category.assoc, hgh, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
inst_1 : Balanced.{v₁, u₁} C
hP : P.IsSeparating
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
Z : C
g h : Y ⟶ Z
hgh : f ≫ g = f ≫ h
G : C
hG : P G
t : G ⟶ X
refine_2 : t ≫ f ≫ g = (t ≫ f) ≫ h
refine_2₁ : t ≫ f ≫ h = (t ≫ f) ≫ h
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h
have refine_2₂ : t ≫ f ≫ h = t ≫ f ≫ h
Tactic: rw [Category.assoc, hgh, Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ IsIso f ↔
    ∀ (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))
have mp : IsIso f →
  ∀ (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))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
mp :
  IsIso f →
    ∀ (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 ↔
    ∀ (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))
have mpr : (∀ (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: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
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 : IsIso f
⊢ ∀ (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))
have h₁ : ∀ (T : C), Function.Bijective (β := T ⟶ Y) fun (x : T ⟶ X) ↦ x ≫ f
Tactic: rw [isIso_iff_yoneda_map_bijective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
have mpr : ∀ (A : C) (hA : P A) (g : A ⟶ Y), ∃ (x : A ⟶ X), x ≫ f = g
Tactic: refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ IsIso f
have mpr₁ : ∀ (A : C) (hA : P A) (g : A ⟶ Y) (y₁ y₂ : A ⟶ X), y₁ ≫ f = g → y₂ ≫ f = g → y₁ = y₂
Tactic: refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ l₁ = l₂
have mpr : l₁ ≫ f = l₂ ≫ f
Tactic: rw [← cancel_mono f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ l₁ = l₂
have mpr₁ : g = l₂ ≫ f
Tactic: rw [← cancel_mono f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ l₁ = l₂
have mpr₂ : g = g
Tactic: rw [← cancel_mono f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ 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)))
have 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)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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)))
⊢ 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)))
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (hypothesis)
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
⊢ ∀ (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)))
have h₁ : ∀ (T : C), Function.Bijective (β := X ⟶ T) fun (x : Y ⟶ T) ↦ f ≫ x
Tactic: rw [isIso_iff_coyoneda_map_bijective] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
have mpr : ∀ (A : C) (hA : P A) (g : X ⟶ A), ∃ (x : Y ⟶ A), f ≫ x = g
Tactic: refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ IsIso f
have mpr₁ : ∀ (A : C) (hA : P A) (g : X ⟶ A) (y₁ y₂ : Y ⟶ A), f ≫ y₁ = g → f ≫ y₂ = g → y₁ = y₂
Tactic: refine hP _ (fun A hA g ↦ existsUnique_of_exists_of_unique ?_ ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ l₁ = l₂
have mpr : f ≫ l₁ = f ≫ l₂
Tactic: rw [← cancel_epi f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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₂
⊢ l₁ = l₂
have mpr₁ : g = f ≫ l₂
Tactic: rw [← cancel_epi f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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₂
⊢ l₁ = l₂
have mpr₂ : g = g
Tactic: rw [← cancel_epi f, h₁, h₂]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ f = g
have 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
Tactic: obtain ⟨ι, s, hs, c, hc, p, _⟩ := hP X
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ f = g
have rw : p ≫ f = p ≫ g
Tactic: rw [← cancel_epi p]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
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
⊢ f = g
have 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
Tactic: obtain ⟨ι, s, hs, c, hc, j, _⟩ := hP Y