-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma ext_cochain_to_iff (i j : ℤ) (hij : i + 1 = j)
    {K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain K (mappingCone φ) i} :
    γ₁ = γ₂ ↔ γ₁.comp (fst φ).1 hij = γ₂.comp (fst φ).1 hij ∧
      γ₁.comp (snd φ) (add_zero i) = γ₂.comp (snd φ) (add_zero i)

Proof state:
case mpr.intro.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq = γ₂.v p q hpq

Tactic:
rw [ext_to_iff φ q (q + 1) rfl]

Result:
case mpr.intro.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Proof state:
case mpr.intro.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Tactic:
replace h₁ := Cochain.congr_v h₁ p (q + 1) (by omega)

Result:
case mpr.intro.h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
⊢ γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ ∧
    γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q q ⋯

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
⊢ γ₁ = γ₂ ↔ γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
⊢ γ₁ = γ₂ → γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain K (mappingCone φ) i
⊢ γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij ∧ γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯ → γ₁ = γ₂