awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
refine_1 : op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ A
refine_1₁ : A ⟶ op (cokernel (X := kernel f.unop) (kernel.ι f.unop))
refine_1₂ :
  Eq.{v + 1} (α :=
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
      unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯)))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))
refine_1₃ :
  Eq.{v + 1} (α := unop A ⟶ unop A)
    (Quiver.Hom.unop
      (CategoryStruct.comp (Y := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
        (Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯))
        (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯))))
    (Quiver.Hom.unop (𝟙 A))
⊢ Subobject.mk (A := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))
      (Quiver.Hom.op (cokernel.π (kernel.ι f.unop))) =
    Subobject.mk f
have refine_1₄ : Eq (α := op (cokernel (X := kernel f.unop) (kernel.ι f.unop)) ⟶ op X)
  (Iso.hom
      { hom := Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) sorry),
        inv := Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop sorry), hom_inv_id := sorry, inv_hom_id := sorry } ≫
    f)
  (Quiver.Hom.op (cokernel.π (kernel.ι f.unop)))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _
        ⟨?_, ?_, Quiver.Hom.unop_inj ?_, Quiver.Hom.unop_inj ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
A : Cᵒᵖ
f : A ⟶ op X
hf : Mono f
⊢ Eq.{v + 1} (α :=
    unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))) ⟶
      unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) ⋯) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop ⋯)))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop)))))
have refine_1 : Eq (α := unop (op X) ⟶ unop (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))
  (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
    (Quiver.Hom.unop
      (Quiver.Hom.op (epiDesc f.unop (cokernel.π (kernel.ι f.unop)) sorry) ≫
        Quiver.Hom.op (cokernel.desc (kernel.ι f.unop) f.unop sorry))))
  (CategoryStruct.comp (Y := cokernel (X := kernel f.unop) (kernel.ι f.unop)) (cokernel.π (kernel.ι f.unop))
    (Quiver.Hom.unop (𝟙 (op (cokernel (X := kernel f.unop) (kernel.ι f.unop))))))
Tactic: rw [← cancel_epi (cokernel.π (kernel.ι f.unop))]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X : C
⊢ Eq (α := Subobject.{v, u} X →o Subobject.{v, u} X) (OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X)) OrderHom.id
have refine_2 : ∀ ⦃A : C⦄ (f : A ⟶ X) [inst_2 : Mono f],
  Eq (α := Subobject.{v, u} X)
    ((OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) : (a : Subobject X) → Subobject X) (Subobject.mk f) :
      Subobject.{v, u} X)
    ((OrderHom.id : (a : Subobject X) → Subobject X) (Subobject.mk f) : Subobject.{v, u} X)
Tactic: refine OrderHom.ext _ _ (funext (Subobject.ind _ ?_))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ Eq (α := Subobject.{v, u} X)
    ((OrderHom.comp (kernelOrderHom X) (cokernelOrderHom X) : (a : Subobject X) → Subobject X) (Subobject.mk f) :
      Subobject.{v, u} X)
    ((OrderHom.id : (a : Subobject X) → Subobject X) (Subobject.mk f) : Subobject.{v, u} X)
have refine_2 : Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
Tactic: dsimp only [OrderHom.comp_coe, Function.comp_apply, cokernelOrderHom_coe, Subobject.lift_mk,
      kernelOrderHom_coe, OrderHom.id_coe, id, unop_op, Quiver.Hom.unop_op]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
have refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
have refine_2₁ : A ⟶ kernel (Y := cokernel f) (cokernel.π f)
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
refine_2₁ : A ⟶ kernel (Y := cokernel f) (cokernel.π f)
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
have refine_2₂ : monoLift f (kernel.ι (cokernel.π f)) sorry ≫ kernel.lift (cokernel.π f) f sorry = 𝟙 (kernel (Y := cokernel f) (cokernel.π f))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
refine_2₁ : A ⟶ kernel (Y := cokernel f) (cokernel.π f)
refine_2₂ :
  monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (Y := cokernel f) (cokernel.π f))
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
have refine_2₃ : CategoryStruct.comp (Y := kernel (Y := cokernel f) (cokernel.π f)) (kernel.lift (cokernel.π f) f sorry)
    (monoLift f (kernel.ι (cokernel.π f)) sorry) =
  𝟙 A
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Subobject (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
X A : C
f : A ⟶ X
hf : Mono f
refine_2 : kernel (Y := cokernel f) (cokernel.π f) ⟶ A
refine_2₁ : A ⟶ kernel (Y := cokernel f) (cokernel.π f)
refine_2₂ :
  monoLift f (kernel.ι (cokernel.π f)) ⋯ ≫ kernel.lift (cokernel.π f) f ⋯ = 𝟙 (kernel (Y := cokernel f) (cokernel.π f))
refine_2₃ :
  CategoryStruct.comp (Y := kernel (Y := cokernel f) (cokernel.π f)) (kernel.lift (cokernel.π f) f ⋯)
      (monoLift f (kernel.ι (cokernel.π f)) ⋯) =
    𝟙 A
⊢ Subobject.mk (A := kernel (Y := cokernel f) (cokernel.π f)) (kernel.ι (cokernel.π f)) = Subobject.mk f
have refine_2₄ : Eq (α := kernel (Y := cokernel f) (cokernel.π f) ⟶ X)
  (Iso.hom
      { hom := monoLift f (kernel.ι (cokernel.π f)) sorry, inv := kernel.lift (cokernel.π f) f sorry, hom_inv_id := sorry,
        inv_hom_id := sorry } ≫
    f)
  (kernel.ι (cokernel.π f))
Tactic: refine Subobject.mk_eq_mk_of_comm _ _ ⟨?_, ?_, ?_, ?_⟩ ?_
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
⊢ HasKernel f
have this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
Tactic: have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by
        simpa using NatIso.naturality_1 i f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel f
have rw : HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
inst_5 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X Y : C
f : X ⟶ Y
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
have this₁ : HasKernel (G.map (F.map f) ≫ i.hom.app Y)
Tactic: haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
⊢ HasCokernel f
have this : PreservesColimits G
Tactic: have : PreservesColimits G := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this : PreservesColimits G
⊢ HasCokernel f
have this₁ : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
Tactic: have : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f := by
        simpa using NatIso.naturality_1 i f
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this_1 : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel f
have rw : HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
D : Type u₂
inst_2 : Category.{v₂, u₂} D
inst_3 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_4 : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X Y : C
f : X ⟶ Y
this_1 : PreservesColimits G
this : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
⊢ HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
have this₁ : HasCokernel (G.map (F.map f) ≫ i.hom.app Y)
Tactic: haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
inst_2 : HasFiniteProducts.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_5 : G.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
⊢ Abelian.{v₁, u₁} C
have this : HasKernels.{v₁, u₁} C
Tactic: haveI := hasKernels F G i
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
inst_2 : HasFiniteProducts.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_5 : G.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this : HasKernels.{v₁, u₁} C
⊢ Abelian.{v₁, u₁} C
have this₁ : HasCokernels.{v₁, u₁} C
Tactic: haveI := hasCokernels F G i adj
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
inst_2 : HasFiniteProducts.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_5 : G.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this_1 : HasKernels.{v₁, u₁} C
this : HasCokernels.{v₁, u₁} C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f :=
  Iso.app (Functor.mapIso (Functor.mapArrowFunctor C C) i) (Arrow.mk f)
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)
have this₁ : PreservesColimits G
Tactic: have : PreservesColimits G := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
inst_2 : HasFiniteProducts.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_5 : G.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this_1 : HasKernels.{v₁, u₁} C
this_2 : HasCokernels.{v₁, u₁} C
X Y : C
f : X ⟶ Y
arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f :=
  Iso.app (Functor.mapIso (Functor.mapArrowFunctor C C) i) (Arrow.mk f)
this : PreservesColimits G
iso : Arrow.mk (X := G.obj (Abelian.coimage (F.map f))) (Y := G.obj (Abelian.image (F.map f)))
    (G.map (Abelian.coimageImageComparison (F.map f))) ≅
  Arrow.mk (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f) :=
  Iso.trans (Y :=
    Arrow.mk (X := Abelian.coimage (G.map (F.map f))) (Y := Abelian.image (G.map (F.map f)))
      (Abelian.coimageImageComparison (G.map (F.map f))))
    (Abelian.PreservesCoimageImageComparison.iso G (F.map f) :
      Arrow.mk (X := G.obj (Abelian.coimage (F.map f))) (Y := G.obj (Abelian.image (F.map f)))
          (G.map (Abelian.coimageImageComparison (F.map f))) ≅
        Arrow.mk (X := Abelian.coimage (G.map (F.map f))) (Y := Abelian.image (G.map (F.map f)))
          (Abelian.coimageImageComparison (G.map (F.map f))))
    (Functor.mapIso Abelian.coimageImageComparisonFunctor arrowIso :
      Functor.obj Abelian.coimageImageComparisonFunctor (Arrow.mk (G.map (F.map f))) ≅
        Functor.obj Abelian.coimageImageComparisonFunctor (Arrow.mk f))
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)
have rw : IsIso (X := G.obj (Abelian.coimage (F.map f))) (Y := G.obj (Abelian.image (F.map f)))
  (G.map (Abelian.coimageImageComparison (F.map f)))
Tactic: rw [Arrow.isIso_iff_isIso_of_isIso iso.inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Transfer (hypothesis)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : Preadditive.{v₁, u₁} C
inst_2 : HasFiniteProducts.{v₁, u₁} C
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : Abelian.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
G : Functor.{v₂, v₁, u₂, u₁} D C
inst_5 : G.PreservesZeroMorphisms
inst_6 : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
this_1 : HasKernels.{v₁, u₁} C
this : HasCokernels.{v₁, u₁} C
⊢ Abelian.{v₁, u₁} C
have this₁ : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)
Tactic: have : ∀ {X Y : C} (f : X ⟶ Y), IsIso (Abelian.coimageImageComparison f) := by
    intro X Y f
    let arrowIso : Arrow.mk (G.map (F.map f)) ≅ Arrow.mk f :=
      ((Functor.mapArrowFunctor _ _).mapIso i).app (Arrow.mk f)
    have : PreservesColimits G := adj.leftAdjoint_preservesColimits
    let iso : Arrow.mk (G.map (Abelian.coimageImageComparison (F.map f))) ≅
        Arrow.mk (Abelian.coimageImageComparison f) :=
      Abelian.PreservesCoimageImageComparison.iso G (F.map f) ≪≫
        Abelian.coimageImageComparisonFunctor.mapIso arrowIso
    rw [Arrow.isIso_iff_isIso_of_isIso iso.inv]
    infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
⊢ Function.Surjective.{v + 1, v + 1} (α := X ⟶ Y) (β :=
    Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
      (Functor.obj (preadditiveCoyonedaObj G) Y))
    (Functor.map (preadditiveCoyonedaObj G))
have rw : Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
  AddCommGrpCat.of
    (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
      (Functor.obj (preadditiveCoyonedaObj G) Y)))
  (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
Tactic: rw [← Functor.coe_mapAddHom, ← AddCommGrpCat.hom_ofHom (preadditiveCoyonedaObj G).mapAddHom,
    ← AddCommGrpCat.epi_iff_surjective]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have exact : cm.Exact
Tactic: have exact : cm.Exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel _)
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
⊢ Mono cm.op.f
have dsimp : Mono.{v, u} (C := Cᵒᵖ) (X := op X) (Y := op G) p.op
Tactic: dsimp [cm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have mono : Mono cm.op.f
Tactic: have mono : Mono cm.op.f := by dsimp [cm]; infer_instance
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have faithful : φ.Faithful
Tactic: have faithful : φ.Faithful := by rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
faithful : φ.Faithful
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have hR₁ : ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))
Tactic: apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
faithful : φ.Faithful
hR₁ : ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have hR₂' : Mono (X :=
  ShortComplex.X₁
    (cm.op.map
      (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
        (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
  (ShortComplex.f
    (cm.op.map
      (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
        (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
Tactic: apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))
-- Lean 4 proof step from Mathlib.CategoryTheory.Abelian.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Abelian.{v, u} C
G : C
inst_2 : Projective.{v, u} G
hG : IsSeparator.{v, u} G
X : C
p : G ⟶ X
inst_3 : Epi p
Y : C
cm : ShortComplex.{v, u} C := ShortComplex.mk (X₁ := kernel p) (kernel.ι p) p ⋯
exact : cm.Exact
mono : Mono cm.op.f
φ : Functor.{v, v, u, v + 1} C (ModuleCat (End G)ᵐᵒᵖ) := preadditiveCoyonedaObj G
faithful : φ.Faithful
hR₁ : ShortComplex.Exact (cm.op.map (Functor.obj preadditiveYoneda Y))
hR₂' :
  Mono (X :=
    ShortComplex.X₁
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
    (ShortComplex.f
      (cm.op.map
        (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
          (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
⊢ Epi.{v, v + 1} (X := AddCommGrpCat.of (X ⟶ Y)) (Y :=
    AddCommGrpCat.of
      (Quiver.Hom (V := ModuleCat (End G)ᵐᵒᵖ) (Functor.obj (preadditiveCoyonedaObj G) X)
        (Functor.obj (preadditiveCoyonedaObj G) Y)))
    (AddCommGrpCat.ofHom (Functor.mapAddHom (preadditiveCoyonedaObj G)))
have h₀ : Epi (X := ShortComplex.X₂ (cm.op.map (Functor.obj preadditiveYoneda Y))) (Y :=
  ShortComplex.X₂
    (cm.op.map
      (Functor.comp (D := (ModuleCat (End G)ᵐᵒᵖ)ᵒᵖ) (Functor.op (preadditiveCoyonedaObj G))
        (Functor.obj preadditiveYoneda (Functor.obj (preadditiveCoyonedaObj G) Y)))))
  (ShortComplex.Hom.τ₂ (cm.op.mapNatTrans (preadditiveYonedaMap (preadditiveCoyonedaObj G) Y)))
Tactic: apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))