awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
⊢ ∃ (G : C), Injective.{v, u} G ∧ IsCoseparator.{v, u} G
have this : WellPowered.{v, v, u} C
Tactic: haveI : WellPowered.{v} C := wellPowered_of_isDetector G hG.isDetector
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this : WellPowered.{v, v, u} C
⊢ ∃ (G : C), Injective.{v, u} G ∧ IsCoseparator.{v, u} G
have this₁ : HasProductsOfShape (Subobject.{v, u} (op G)) C
Tactic: haveI : HasProductsOfShape (Subobject (op G)) C := hasProductsOfShape_of_small.{v} _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
⊢ ∃ (G : C), Injective.{v, u} G ∧ IsCoseparator.{v, u} G
have refine : ∀ (X Y : C) (f : X ⟶ Y) (hf : ∀ (h : Y ⟶ T), f ≫ h = 0), f = 0
Tactic: refine ⟨T, inferInstance, (Preadditive.isCoseparator_iff _).2 fun X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
⊢ f = 0
have refine : ∀ (h : G ⟶ X), h ≫ f = 0
Tactic: refine (Preadditive.isSeparator_iff _).1 hG _ fun h => ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
⊢ h ≫ f = 0
have rw : CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f)) (Limits.image.ι (h ≫ f)) = 0
Tactic: rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
rw : CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f)) (Limits.image.ι (h ≫ f)) = 0
⊢ h ≫ f = 0
have rw₁ : Eq (α := G ⟶ Y) (CategoryStruct.comp (Y := image (h ≫ f)) 0 (Limits.image.ι (h ≫ f))) 0
Tactic: rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
hh : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
rw : CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f)) (Limits.image.ι (h ≫ f)) = 0
rw₁ : Eq (α := G ⟶ Y) (CategoryStruct.comp (Y := image (h ≫ f)) 0 (Limits.image.ι (h ≫ f))) 0
⊢ h ≫ f = 0
have rw₂ : Eq.{v + 1} (α := G ⟶ Y) 0 0
Tactic: rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
⊢ h ≫ f = 0
have suffices : Eq (α := G ⟶ image (h ≫ f)) (factorThruImage (h ≫ f)) 0
Tactic: suffices hh : factorThruImage (h ≫ f) = 0 by
    rw [← Limits.image.fac (h ≫ f), hh, zero_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
⊢ factorThruImage (h ≫ f) ≫ q = 0
have rw : CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
    (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
  0
Tactic: rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
rw :
  CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
      (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
    0
⊢ factorThruImage (h ≫ f) ≫ q = 0
have rw₁ : (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
Tactic: rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
rw :
  CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
      (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
    0
rw₁ : (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
⊢ factorThruImage (h ≫ f) ≫ q = 0
have rw₂ : h ≫ f ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
Tactic: rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
rw :
  CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
      (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
    0
rw₁ : (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
rw₂ : h ≫ f ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
⊢ factorThruImage (h ≫ f) ≫ q = 0
have rw₃ : Eq (α := G ⟶ T) (h ≫ 0) 0
Tactic: rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasLimits.{v, u} C
inst_3 : EnoughInjectives.{v, u} C
G : C
hG : IsSeparator.{v, u} G
this_1 : WellPowered.{v, v, u} C
this : HasProductsOfShape (Subobject.{v, u} (op G)) C
T : C := Injective.under.{v, u} (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
X Y : C
f : X ⟶ Y
hf : ∀ (h : Y ⟶ T), f ≫ h = 0
h : G ⟶ X
R : Subobject.{v, u} (op G) := Subobject.mk (A := op (image (h ≫ f))) (Quiver.Hom.op (factorThruImage (h ≫ f)))
q₁ : image (h ≫ f) ⟶ unop (Functor.obj Subobject.underlying R) :=
  Iso.hom (Iso.unop (Subobject.underlyingIso (Quiver.Hom.op (factorThruImage (h ≫ f)))))
q₂ : unop (Functor.obj Subobject.underlying R) ⟶
  ∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P) :=
  section_ (Pi.π (fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P)) R)
q : image (h ≫ f) ⟶ T :=
  q₁ ≫ q₂ ≫ Injective.ι (∏ᶜ fun (P : Subobject.{v, u} (op G)) ↦ unop (Functor.obj Subobject.underlying P))
rw :
  CategoryStruct.comp (Y := image (h ≫ f)) (factorThruImage (h ≫ f))
      (Limits.image.ι (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f))) =
    0
rw₁ : (h ≫ f) ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
rw₂ : h ≫ f ≫ Injective.factorThru q (Limits.image.ι (h ≫ f)) = 0
rw₃ : Eq (α := G ⟶ T) (h ≫ 0) 0
⊢ factorThruImage (h ≫ f) ≫ q = 0
have rw₄ : Eq.{v + 1} (α := G ⟶ T) 0 0
Tactic: rw [← Injective.comp_factorThru q (Limits.image.ι (h ≫ f)), Limits.image.fac_assoc,
      Category.assoc, hf, comp_zero]
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Abelian (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
inst_2 : HasColimits.{v, u} C
inst_3 : EnoughProjectives.{v, u} C
G : C
hG : IsCoseparator.{v, u} G
⊢ ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G
have obtain : ∀ (T : Cᵒᵖ) (hT₁ : Injective.{v, u} T) (hT₂ : IsCoseparator.{v, u} T),
  ∃ (G : C), Projective.{v, u} G ∧ IsSeparator.{v, u} G
Tactic: obtain ⟨T, hT₁, hT₂⟩ := has_injective_coseparator (op G) ((isSeparator_op_iff _).2 hG)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
h_1 : P.IsSeparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
Z : C
hZ : P Z
h : Z ⟶ α.inverse.obj X
⊢ h ≫ α.inverse.map f = h ≫ α.inverse.map g
have obtain : ∀ (h' : α.functor.obj Z ⟶ X),
  Eq.{v₁ + 1} (α := Z ⟶ α.inverse.obj Y)
    ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map f :
      Z ⟶ α.inverse.obj Y)
    ((α.toAdjunction.homEquiv Z X : (a : α.functor.obj Z ⟶ X) → Z ⟶ α.inverse.obj X) h' ≫ α.inverse.map g :
      Z ⟶ α.inverse.obj Y)
Tactic: obtain ⟨h', rfl⟩ := (α.toAdjunction.homEquiv _ _).surjective 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
h_1 : P.IsCoseparating
D : Type u_1
inst_1 : Category.{v_1, u_1} D
α : Equivalence.{v₁, v_1, u₁, u_1} C D
X Y : D
f g : X ⟶ Y
H : ∀ (G : D), P.strictMap α.functor G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
Z : C
hZ : P Z
h : α.inverse.obj Y ⟶ Z
⊢ α.inverse.map f ≫ h = α.inverse.map g ≫ h
have obtain : ∀ (h' : Y ⟶ α.symm.inverse.obj Z),
  Eq (α := α.inverse.obj X ⟶ Z)
    (α.inverse.map f ≫
      ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')
    (α.inverse.map g ≫
      ((α.symm.toAdjunction.homEquiv Y Z).symm : (a : Y ⟶ α.symm.inverse.obj Z) → α.symm.functor.obj Y ⟶ Z) h')
Tactic: obtain ⟨h', rfl⟩ := (α.symm.toAdjunction.homEquiv _ _).symm.surjective 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
⊢ IsSeparating.{v₁, u₁} P.op ↔ P.IsCoseparating
have refine_1 : ∀ (hP : IsSeparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h), f = g
Tactic: refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsSeparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h),
    f = g
⊢ IsSeparating.{v₁, u₁} P.op ↔ P.IsCoseparating
have refine_2 : ∀ (hP : P.IsCoseparating) (X Y : Cᵒᵖ) (f g : X ⟶ Y) (hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g), f = g
Tactic: refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- 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 : IsSeparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
have refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : G ⟶ op Y), (h ≫ f.op).unop = (h ≫ g.op).unop
Tactic: refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
-- 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.IsCoseparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
have refine_2 : ∀ (G : C) (hG : P G) (h : unop X ⟶ G), (f.unop ≫ h).op = (g.unop ≫ h).op
Tactic: refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsCoseparating.{v₁, u₁} P.op ↔ P.IsSeparating
have refine_1 : ∀ (hP : IsCoseparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g),
  f = g
Tactic: refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsCoseparating.{v₁, u₁} P.op) (X Y : C) (f g : X ⟶ Y) (hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g),
    f = g
⊢ IsCoseparating.{v₁, u₁} P.op ↔ P.IsSeparating
have refine_2 : ∀ (hP : P.IsSeparating) (X Y : Cᵒᵖ) (f g : X ⟶ Y) (hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h), f = g
Tactic: refine ⟨fun hP X Y f g hfg => ?_, fun hP X Y f g hfg => ?_⟩
-- 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 : IsCoseparating.{v₁, u₁} P.op
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), P G → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
have refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : op X ⟶ G),
  Eq (α := unop G ⟶ unop (op Y)) (Quiver.Hom.unop (f.op ≫ h)) (Quiver.Hom.unop (g.op ≫ h))
Tactic: refine Quiver.Hom.op_inj (hP _ _ fun G hG h => Quiver.Hom.unop_inj ?_)
-- 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.IsSeparating
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
have refine_2 : ∀ (G : C) (hG : P G) (h : G ⟶ unop Y), (h ≫ f.unop).op = (h ≫ g.unop).op
Tactic: refine Quiver.Hom.unop_inj (hP _ _ fun G hG h => Quiver.Hom.op_inj ?_)
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
⊢ IsDetecting.{v₁, u₁} P.op ↔ P.IsCodetecting
have refine_1 : ∀ (hP : IsDetecting.{v₁, u₁} P.op) (X Y : C) (f : X ⟶ Y)
  (hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h), IsIso f
Tactic: refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (hP : IsDetecting.{v₁, u₁} P.op) (X Y : C) (f : X ⟶ Y)
    (hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h), IsIso f
⊢ IsDetecting.{v₁, u₁} P.op ↔ P.IsCodetecting
have refine_2 : ∀ (hP : P.IsCodetecting) (X Y : Cᵒᵖ) (f : X ⟶ Y) (hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h),
  IsIso f
Tactic: refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- 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 : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
⊢ IsIso f
have refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : G ⟶ op X), ∃! h' : G ⟶ op Y, h' ≫ f.op = h
Tactic: refine (isIso_op_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 : IsDetecting.{v₁, u₁} P.op
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), P G → ∀ (h : X ⟶ G), ∃! h' : Y ⟶ G, f ≫ h' = h
G : Cᵒᵖ
hG : P.op G
h : G ⟶ op X
⊢ ∃! h' : G ⟶ op Y, h' ≫ f.op = h
have refine_1 : ∀ (t : Y ⟶ unop G) (ht : f ≫ t = h.unop)
  (ht' : ∀ (y : Y ⟶ unop G), (fun (h' : Y ⟶ unop G) ↦ f ≫ h' = h.unop) y → y = t), ∃! h' : G ⟶ op Y, h' ≫ f.op = 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.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
⊢ IsIso f
have refine_2 : ∀ (G : C) (hG : P G) (h : unop Y ⟶ G), ∃! h' : unop X ⟶ G, f.unop ≫ h' = 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.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
⊢ ∃! h' : unop X ⟶ G, f.unop ≫ h' = h
have refine_2 : ∀ (t : op G ⟶ X) (ht : t ≫ f = h.op) (ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t),
  ∃! h' : unop X ⟶ G, f.unop ≫ h' = 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.IsCodetecting
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), P.op G → ∀ (h : G ⟶ Y), ∃! h' : G ⟶ X, h' ≫ f = h
G : C
hG : P G
h : unop Y ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun (h' : op G ⟶ X) ↦ h' ≫ f = h.op) y → y = t
⊢ ∃! h' : unop X ⟶ G, f.unop ≫ h' = h
have refine_2 : ∀ (y : unop X ⟶ G) (hy : (fun (h' : unop X ⟶ G) ↦ f.unop ≫ h' = h) y), (fun (h' : op G ⟶ X) ↦ h' ≫ f = 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
⊢ IsCodetecting.{v₁, u₁} P.op ↔ P.IsDetecting
have refine_1 : ∀ (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), IsIso f
Tactic: refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Generator.Basic (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
P : ObjectProperty.{v₁, u₁} C
refine_1 :
  ∀ (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), IsIso f
⊢ IsCodetecting.{v₁, u₁} P.op ↔ P.IsDetecting
have refine_2 : ∀ (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
Tactic: refine ⟨fun hP X Y f hf => ?_, fun hP X Y f hf => ?_⟩
-- 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
⊢ IsIso f
have refine_1 : ∀ (G : Cᵒᵖ) (hG : P.op G) (h : op Y ⟶ G), ∃! h' : op X ⟶ G, f.op ≫ h' = h
Tactic: refine (isIso_op_iff _).1 (hP _ fun G hG h => ?_)