-- Module: Mathlib.Algebra.Homology.Functor
Goal:
T : Type u_1
inst : Category.{v_1, u_1} T
V : Type u_2
inst_1 : Category.{v_2, u_2} V
inst_2 : Abelian.{v_2, u_2} V
ι : Type u_3
c : ComplexShape ι
K₁ K₂ : HomologicalComplex (CategoryTheory.Functor.{v_1, v_2, u_1, u_2} T V) c
f : K₁ ⟶ K₂
mp :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mpr :
  (∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mp₁ mp₂ mp₃ :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mpr₁ mpr₂ mpr₃ :
  (∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mp₄ mp₅ mp₆ :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mpr₄ mpr₅ mpr₆ :
  (∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mp₇ mp₈ mp₉ :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mpr₇ mpr₈ mpr₉ :
  (∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mp₁₀ mp₁₁ :
  (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
mpr₁₀ mpr₁₁ :
  (∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) →
    ∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i
⊢ (∀ (i : ι) (t : T),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i) ↔
    ∀ (t : T) (i : ι),
      QuasiIsoAt (K := Functor.obj (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) K₁)
        (CategoryTheory.Functor.map (Functor.mapHomologicalComplex (Functor.obj (evaluation T V) t) c) f) i

Tactic:
tauto