-- Mathlib/CategoryTheory/Abelian/Transfer.lean
theorem hasKernels [PreservesFiniteLimits G] (i : F ⋙ G ≅ 𝟭 C) : HasKernels C :=
  { has_limit := fun f => by
      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 : HasKernel (G.map (F.map f) ≫ i.hom.app _) := Limits.hasKernel_comp_mono _ _
      apply Limits.hasKernel_iso_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
inst✝ : 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
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

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
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasKernel 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
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasKernel 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
inst✝ : 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

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
inst✝ : 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

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
inst✝ : 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✝)

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
inst✝ : 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✝)

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

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
inst✝ : 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
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✝)

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
inst✝ : PreservesFiniteLimits G
i : F ⋙ G ≅ 𝟭 C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
this : i.inv.app X✝ ≫ (F ⋙ G).map f ≫ i.hom.app Y✝ = (𝟭 C).map f
⊢ HasKernel 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
inst✝ : 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