-- Module: Mathlib.Algebra.Homology.Double
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : HasZeroMorphisms.{v_1, u_1} C
inst_2 : HasZeroObject.{v_1, u_1} C
X₀ X₁ : C
f : X₀ ⟶ X₁
ι : Type u_2
c : ComplexShape ι
i₀ : ι
K : HomologicalComplex.{v_1, u_1, u_2} C c
φ₀ : X₀ ⟶ K.X i₀
k₀ k₁ : ι
hk : c.Rel k₀ k₁
h₀ : ¬k₀ = i₀
hi₀₁ : c.Rel i₀ k₀
h : i₀ ≠ k₀
φ₁ : X₁ ⟶ K.X k₀
comm : φ₀ ≫ K.d i₀ k₀ = f ≫ φ₁
hφ : ∀ (k : ι), c.Rel k₀ k → φ₁ ≫ K.d k₀ k = 0
pos :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀)) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₁ :
  (𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0
pos₂ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) ((Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁) ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₃ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ K.d k₀ k₁)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₄ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) (Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ 0)
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₅ :
  Eq (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
    (d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0)
pos₆ :
  Eq.{v_1 + 1} (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0
    (CategoryStruct.comp (Y := X (double f hi₀₁) k₁) 0
      (if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0))
pos₇ pos₈ : Eq.{v_1 + 1} (α := X (double f hi₀₁) k₀ ⟶ K.X k₁) 0 0
⊢ (if k₀ = k₀ then 𝟙 (X (double f hi₀₁) k₀) ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ 𝟙 (K.X k₀) else 0) ≫ K.d k₀ k₁ =
    d (double f hi₀₁) k₀ k₁ ≫
      if hk₀ : k₁ = i₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₀ f hi₀₁) ≫ φ₀ ≫ eqToHom ⋯
      else if hk₁ : k₁ = k₀ then eqToHom ⋯ ≫ Iso.hom (doubleXIso₁ f hi₀₁ h) ≫ φ₁ ≫ eqToHom ⋯ else 0

Tactic:
rw [if_pos rfl, comp_id, id_comp, assoc, hφ k₁ hk, comp_zero,
          double_d_eq_zero₀ _ _ _ _ h.symm, zero_comp]

Premises used: HomologicalComplex.double_d_eq_zero₀, CategoryTheory.Category.assoc, CategoryTheory.Limits.comp_zero, Ne.symm, CategoryTheory.Category.comp_id, if_pos, CategoryTheory.Limits.zero_comp, rfl, CategoryTheory.Category.id_comp