-- Module: Mathlib.CategoryTheory.Functor.ReflectsIso.Exact
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
I : Type u_2
D : I → Type u_3
inst_1 : (i : I) → Category.{v_2, u_3} (D i)
F : (i : I) → Functor.{v_1, v_2, u_1, u_3} C (D i)
hP : JointlyReflectIsomorphisms (D := D) F
inst_2 : Abelian.{v_1, u_1} C
inst_3 : (i : I) → Abelian.{v_2, u_3} (D i)
inst_4 : CategoryWithHomology.{v_1, u_1} C
inst_5 : ∀ (i : I), PreservesFiniteLimits (F i)
inst_6 : ∀ (i : I), PreservesFiniteColimits (F i)
α : Type u_4
c : ComplexShape α
K L : HomologicalComplex.{v_1, u_1, u_4} C c
f : K ⟶ L
mp :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) →
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
mpr :
  (∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1) →
    ∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i
mp₁ mp₂ mp₃ :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) →
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
mpr₁ mpr₂ mpr₃ :
  (∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1) →
    ∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i
mp₄ mp₅ mp₆ :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) →
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
mpr₄ mpr₅ mpr₆ :
  (∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1) →
    ∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i
mp₇ mp₈ mp₉ :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) →
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
mpr₇ mpr₈ mpr₉ :
  (∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1) →
    ∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i
mp₁₀ mp₁₁ :
  (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) →
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1
mpr₁₀ mpr₁₁ :
  (∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1) →
    ∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i
⊢ (∀ (i : α) (i_1 : I),
      QuasiIsoAt (K := Functor.obj ((F i_1).mapHomologicalComplex c) K)
        (Functor.map ((F i_1).mapHomologicalComplex c) f) i) ↔
    ∀ (i : I) (i_1 : α),
      QuasiIsoAt (K := Functor.obj ((F i).mapHomologicalComplex c) K) (Functor.map ((F i).mapHomologicalComplex c) f)
        i_1

Tactic:
tauto