-- Mathlib/CategoryTheory/Abelian/Transfer.lean
theorem hasCokernels (i : F ⋙ G ≅ 𝟭 C) (adj : G ⊣ F) : HasCokernels C :=
  { has_colimit := fun f => by
      have : PreservesColimits G := adj.leftAdjoint_preservesColimits
      have := NatIso.naturality_1 i f
      simp? at this says
        simp only [Functor.id_obj, Functor.comp_obj, Functor.comp_map, Functor.id_map] at this
      rw [← this]
      haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _
      apply Limits.hasCokernel_epi_comp }

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝¹ : PreservesColimits G
this✝ : 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

Result:
no goals

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel f

Tactic:
rw [← this]

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : 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✝)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasCokernel f

Tactic:
simp? at this says
  simp only [Functor.id_obj, Functor.comp_obj, Functor.comp_map, Functor.id_map] at this

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel f

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : PreservesColimits G
⊢ HasCokernel f

Tactic:
have := NatIso.naturality_1 i f

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasCokernel f

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasCokernel f

Tactic:
have : PreservesColimits G := adj.leftAdjoint_preservesColimits

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : PreservesColimits G
⊢ HasCokernel f

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : 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✝)

Tactic:
haveI : HasCokernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasCokernel_comp_iso _ _

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝¹ : PreservesColimits G
this✝ : 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✝)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasCokernel f

Tactic:
simp only [Functor.id_obj, Functor.comp_obj, Functor.comp_map, Functor.id_map] at this

Result:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Preadditive C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : Abelian D
F : C ⥤ D
G : D ⥤ C
inst✝ : G.PreservesZeroMorphisms
i : F ⋙ G ≅ 𝟭 C
adj : G ⊣ F
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this✝ : PreservesColimits G
this : i.inv.app X✝ ≫ G.map (F.map f) ≫ i.hom.app Y✝ = f
⊢ HasCokernel f