awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Abelian.Subobject
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 (α := kernel (Y := cokernel f) (cokernel.π f) ⟶ X)
    (Iso.hom
        { hom := monoLift f (kernel.ι (cokernel.π f)) ⋯, inv := kernel.lift (cokernel.π f) f ⋯, hom_inv_id := ⋯,
          inv_hom_id := ⋯ } ≫
      f)
    (kernel.ι (cokernel.π f))

Tactic:
simp only [monoLift_comp]

Premises used: CategoryTheory.Abelian.monoLift_comp
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f

Tactic:
simpa using NatIso.naturality_1 i f

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
rw : HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
⊢ HasKernel f

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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 (G.map (F.map f) ≫ i.hom.app Y)

Tactic:
haveI : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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_1 : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
this : HasKernel (G.map (F.map f) ≫ i.hom.app Y)
⊢ HasKernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)

Tactic:
apply Limits.hasKernel_iso_comp

Premises used: CategoryTheory.Limits.hasKernel_iso_comp
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ PreservesColimits G

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f

Tactic:
simpa using NatIso.naturality_1 i f

Premises used: CategoryTheory.NatIso.naturality_1
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ 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
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
rw : HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)
⊢ HasCokernel f

Tactic:
rw [← this]
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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 (G.map (F.map f) ≫ i.hom.app Y)

Tactic:
haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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_2 : i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y = f
this : HasCokernel (G.map (F.map f) ≫ i.hom.app Y)
⊢ HasCokernel (i.inv.app X ≫ G.map (F.map f) ≫ i.hom.app Y)

Tactic:
apply Limits.hasCokernel_epi_comp

Premises used: CategoryTheory.Limits.hasCokernel_epi_comp
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ HasKernels.{v₁, u₁} C

Tactic:
haveI := hasKernels F G i
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
⊢ HasCokernels.{v₁, u₁} C

Tactic:
haveI := hasCokernels F G i adj
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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)
⊢ PreservesColimits G

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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))
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)))
⊢ IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)

Tactic:
rw [Arrow.isIso_iff_isIso_of_isIso iso.inv]

Premises used: CategoryTheory.Arrow.isIso_iff_isIso_of_isIso, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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 := G.obj (Abelian.coimage (F.map f))) (Y := G.obj (Abelian.image (F.map f)))
    (G.map (Abelian.coimageImageComparison (F.map f)))

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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), 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
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
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
this : ∀ {X Y : C} (f : X ⟶ Y), IsIso (X := Abelian.coimage f) (Y := Abelian.image f) (Abelian.coimageImageComparison f)
⊢ Abelian.{v₁, u₁} C

Tactic:
apply Abelian.ofCoimageImageComparisonIsIso

Premises used: CategoryTheory.Abelian.ofCoimageImageComparisonIsIso
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
⊢ Functor.Additive.{w, u_1, v_1, u_1} (inverse C)

Tactic:
(equivalence C).symm.fullyFaithfulFunctor.additive_ofFullyFaithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.ShrinkHoms.toShrinkHoms, CategoryTheory.ShrinkHoms.fromShrinkHoms, CategoryTheory.ShrinkHoms.inverse, CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Equivalence.symm
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
⊢ Functor.Additive.{v_1, u_1, w, u_1} (functor C)

Tactic:
(equivalence C).symm.additive_inverse_of_FullyFaithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.ShrinkHoms.toShrinkHoms, CategoryTheory.ShrinkHoms.functor, CategoryTheory.ShrinkHoms.fromShrinkHoms, CategoryTheory.ShrinkHoms.inverse, CategoryTheory.ShrinkHoms.equivalence, CategoryTheory.Equivalence.symm, CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
J : Type u_2
inst_3 : Category.{v_2, u_2} J
inst_4 : HasLimitsOfShape.{v_2, u_2, v_1, u_1} J C
⊢ HasLimitsOfShape.{v_2, u_2, w, u_1} J (ShrinkHoms.{u_1} C)

Tactic:
Adjunction.hasLimitsOfShape_of_equivalence (inverse C)

Premises used: CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence, CategoryTheory.ShrinkHoms.inverse
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : LocallySmall.{w, v_1, u_1} C
inst_2 : Preadditive.{v_1, u_1} C
inst_3 : HasFiniteLimits.{v_1, u_1} C
⊢ HasFiniteLimits.{w, u_1} (ShrinkHoms.{u_1} C)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Functor.Additive (C := AsSmall.{u_1, v, u} C) down

Tactic:
equiv.symm.fullyFaithfulFunctor.additive_ofFullyFaithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulFunctor, CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.AsSmall.equiv, CategoryTheory.Functor.FullyFaithful.additive_ofFullyFaithful, CategoryTheory.Equivalence.symm, CategoryTheory.AsSmall.down
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
⊢ Functor.Additive (C := C) (D := AsSmall.{u_1, v, u} C) up

Tactic:
equiv.symm.additive_inverse_of_FullyFaithful

Premises used: CategoryTheory.Equivalence.fullyFaithfulInverse, CategoryTheory.AsSmall.equiv, CategoryTheory.AsSmall.up, CategoryTheory.Equivalence.symm, CategoryTheory.AsSmall.down, CategoryTheory.Equivalence.additive_inverse_of_FullyFaithful
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
J : Type u_1
inst_2 : Category.{v_1, u_1} J
inst_3 : HasLimitsOfShape.{v_1, u_1, v, u} J C
⊢ HasLimitsOfShape J (AsSmall.{w, v, u} C)

Tactic:
Adjunction.hasLimitsOfShape_of_equivalence equiv.inverse

Premises used: CategoryTheory.Adjunction.hasLimitsOfShape_of_equivalence, CategoryTheory.AsSmall.equiv, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.CategoryTheory.Abelian.Transfer
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteLimits.{v, u} C
⊢ HasFiniteLimits (AsSmall.{w, v, u} C)

Tactic:
⟨fun _ => inferInstance⟩

Premises used: inferInstance, CategoryTheory.Limits.HasFiniteLimits.mk
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
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)))
⊢ 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))

Tactic:
rw [← Functor.coe_mapAddHom, ← AddCommGrpCat.hom_ofHom (preadditiveCoyonedaObj G).mapAddHom,
    ← AddCommGrpCat.epi_iff_surjective]

Premises used: AddCommGrpCat.hom_ofHom, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.Functor.coe_mapAddHom, AddCommGrpCat.epi_iff_surjective, CategoryTheory.Functor.mapAddHom
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
⊢ Eq (α := kernel p ⟶ X) (kernel.ι p ≫ p) 0

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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 ⋯
⊢ cm.Exact

Tactic:
have exact : cm.Exact := ShortComplex.exact_of_f_is_kernel _ (kernelIsKernel _)
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
dsimp : Mono.{v, u} (C := Cᵒᵖ) (X := op X) (Y := op G) p.op
⊢ Mono cm.op.f

Tactic:
dsimp [cm]
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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.{v, u} (C := Cᵒᵖ) (X := op X) (Y := op G) p.op

Tactic:
infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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

Tactic:
have mono : Mono cm.op.f := by dsimp [cm]; infer_instance
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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
rwa rwa₁ rwa₂ rwa₃ : IsSeparator.{v, u} G
⊢ φ.Faithful

Tactic:
rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]

Premises used: CategoryTheory.isSeparator_iff_faithful_preadditiveCoyonedaObj
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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

Tactic:
have faithful : φ.Faithful := by rwa [← isSeparator_iff_faithful_preadditiveCoyonedaObj]
-- Module: Mathlib.CategoryTheory.Abelian.Yoneda
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)))))
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)))
h₁ :
  Mono (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)))
⊢ 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:
apply ShortComplex.epi_of_mono_of_epi_of_mono (cm.op.mapNatTrans (preadditiveYonedaMap _ _))

Premises used: CategoryTheory.ShortComplex.mapNatTrans, CategoryTheory.preadditiveYonedaMap, CategoryTheory.ShortComplex.op, CategoryTheory.ShortComplex.epi_of_mono_of_epi_of_mono