-- 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.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)

Tactic:
obtain ⟨m, rfl⟩ : ∃ (m : ℤ), n = m + 1 := ⟨n - 1, by simp⟩

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 : ℤ
⊢ IsIso ((F.shift (m + 1)).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
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)

Tactic:
dsimp at 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
⊢ F.homologicalKernel.P Z ↔ ∀ (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 : ℤ
⊢ IsIso ((F.shift (m + 1)).map f)

Tactic:
have := (h (m + 1)).1

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)
⊢ IsIso ((F.shift (m + 1)).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.W f ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
apply (F.homologicalKernel.mem_W_iff_of_distinguished _ hT).trans

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