-- Lean 4 proof step from Mathlib.CategoryTheory.Triangulated.HomologicalFunctor (hypothesis)
Goal:
C : Type u_1
A : Type u_3
inst : Category.{v_1, u_1} C
inst_1 : HasShift.{v_1, u_1, 0} C ℤ
inst_2 : Category.{v_3, u_3} A
F : Functor.{v_1, v_3, u_1, u_3} C A
inst_3 : HasZeroObject.{v_1, u_1} C
inst_4 : Preadditive.{v_1, u_1} C
inst_5 : ∀ (n : ℤ), Additive.{v_1, u_1, v_1, u_1} (shiftFunctor C n)
inst_6 : Pretriangulated.{v_1, u_1} C
inst_7 : Abelian.{v_3, u_3} A
inst_8 : F.IsHomological
inst_9 : F.ShiftSequence ℤ
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
h : Z ⟶ obj.{v_1, v_1, u_1, u_1} (shiftFunctor C (A := ℤ) 1) X
hT :
  Membership.mem (γ := Set (Triangle.{v_1, u_1} C)) (@distinguishedTriangles _ _ inst_3 _ inst_4 inst_5 _)
    (Triangle.mk f g h)
h₁ :
  ∀ (n : ℤ),
    IsZero.{v_3, u_3}
        (ShortComplex.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 := ⋯ : ShortComplex.{v_3, u_3} A }) ↔
      Eq (α :=
          ShortComplex.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 := ⋯ : ShortComplex.{v_3, u_3} A } ⟶
            ShortComplex.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 := ⋯ })
          (ShortComplex.f
            { 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 := ⋯ })
          0 ∧
        Eq (α :=
          ShortComplex.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 := ⋯ : ShortComplex.{v_3, u_3} A } ⟶
            ShortComplex.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 := ⋯ })
          (ShortComplex.g
            { 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 := ⋯ })
          0
⊢ F.homologicalKernel (Triangle.mk f g h).obj₃ ↔ ∀ (n : ℤ), IsIso ((F.shift n).map f)
have h₂ : ∀ (n : ℤ),
  Mono ((F.shift (n + 1)).map (Triangle.mk f g h).mor₁) ↔
    Eq (α := (F.shift n).obj (Triangle.mk f g h).obj₃ ⟶ (F.shift (n + 1)).obj (Triangle.mk f g h).obj₁)
      (F.homologySequenceδ (Triangle.mk f g h) n (n + 1) sorry) 0
Tactic: have h₂ := fun n => F.homologySequence_mono_shift_map_mor₁_iff _ hT n _ rfl