-- 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
⊢ F.homologicalKernel.P (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
have h₁ := fun n => (F.homologySequence_exact₃ _ hT n _ rfl).isZero_X₂_iff

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
⊢ 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
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
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ n = n - 1 + 1

Tactic:
simp

Result:
no goals

Proof state:
case intro.intro.intro.mp
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)

Tactic:
intro h n

Result:
case intro.intro.intro.mp
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
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
n : ℤ
⊢ IsIso ((F.shift n).map f)

Proof state:
case intro.intro.intro.mp.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
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
this : Epi ((F.shift (m + 1)).map f)
⊢ IsIso ((F.shift (m + 1)).map f)

Tactic:
have := (h m).2

Result:
case intro.intro.intro.mp.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
h : ∀ (n : ℤ), Epi ((F.shift n).map f) ∧ Mono ((F.shift (n + 1)).map f)
m : ℤ
this✝ : Epi ((F.shift (m + 1)).map f)
this : Mono ((F.shift (m + 1)).map f)
⊢ IsIso ((F.shift (m + 1)).map f)