-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma mem_homologicalKernel_W_iff {X Y : C} (f : X ⟶ Y) :
    F.homologicalKernel.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Proof state:
case intro.intro.intro
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero
        (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂)
            (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).X₂ ↔
      (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯)
              ⋯).f =
          0 ∧
        (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂)
              (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).g =
          0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map (Triangle.mk f g h).mor₁) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
⊢ F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
have h₃ := fun n => F.homologySequence_epi_shift_map_mor₁_iff _ hT n

Result:
case intro.intro.intro
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero
        (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂)
            (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).X₂ ↔
      (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂) (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯)
              ⋯).f =
          0 ∧
        (ShortComplex.mk ((F.shift n).map (Triangle.mk f g h).mor₂)
              (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯) ⋯).g =
          0
h₂ :
  ∀ (n : ℤ),
    Mono ((F.shift (n + 1)).map (Triangle.mk f g h).mor₁) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map (Triangle.mk f g h).mor₁) ↔ (F.shift n).map (Triangle.mk f g h).mor₂ = 0
⊢ F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Proof state:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
⊢ F.homologicalKernel.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
obtain ⟨Z, g, h, hT⟩ := distinguished_cocone_triangle f

Result:
case intro.intro.intro
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
⊢ F.homologicalKernel.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Proof state:
case intro.intro.intro.mpr
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
a✝ : ∀ (n : ℤ), IsIso ((F.shift n).map f)
n✝ : ℤ
⊢ Epi ((F.shift n✝).map f) ∧ Mono ((F.shift (n✝ + 1)).map f)

Tactic:
constructor <;> infer_instance

Result:
no goals

Proof state:
case intro.intro.intro
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ F.homologicalKernel.P Z ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
simp only [mem_homologicalKernel_iff, h₁, ← h₂, ← h₃]

Result:
case intro.intro.intro
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁶ : HasZeroObject C
inst✝⁵ : Preadditive C
inst✝⁴ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝³ : Pretriangulated C
inst✝² : Abelian A
inst✝¹ : F.IsHomological
inst✝ : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ (shiftFunctor C 1).obj X
hT : Triangle.mk f g h ∈ distinguishedTriangles
h₁ :
  ∀ (n : ℤ),
    IsZero ((F.shift n).obj Z) ↔ (F.shift n).map g = 0 ∧ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₂ : ∀ (n : ℤ), Mono ((F.shift (n + 1)).map f) ↔ F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯ = 0
h₃ : ∀ (n : ℤ), Epi ((F.shift n).map f) ↔ (F.shift n).map g = 0
⊢ (∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)) ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)