Module: Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

Goal state before:
pp: C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, 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
        { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
            X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
            g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.X₂ ↔
      { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
              X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
              g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.f =
          0 ∧
        { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
              X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
              g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.g =
          0
⊢ F.homologicalKernel (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)

Tactic:
have h₂ := fun n => F.homologySequence_mono_shift_map_mor₁_iff _ hT n _ rfl

Goal state after:
C : Type u_1
A : Type u_3
inst✝⁹ : Category.{v_1, u_1} C
inst✝⁸ : HasShift C ℤ
inst✝⁷ : Category.{v_3, 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
        { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
            X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
            g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.X₂ ↔
      { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
              X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
              g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.f =
          0 ∧
        { X₁ := (F.shift n).obj (Triangle.mk f g h).obj₂, X₂ := (F.shift n).obj (Triangle.mk f g h).obj₃,
              X₃ := (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁, f := (F.shift n).map (Triangle.mk f g h).mor₂,
              g := F.homologySequenceδ (Triangle.mk f g h) n (n + 1) ⋯, zero := ⋯ }.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 (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)