-- 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
p q : ℤ
hpq : p + i = q
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (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 ⋯

Tactic:
simp only [Cochain.comp_zero_cochain_v] at h₂

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
p q : ℤ
hpq : p + i = q
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯
h₂ : γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q 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 (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 ⋯

Tactic:
replace h₂ := Cochain.congr_v h₂ p q hpq

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
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
⊢ γ₁.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
p q : ℤ
hpq : p + i = q
h₁ : (γ₁.comp (↑(fst φ)) hij).v p (q + 1) ⋯ = (γ₂.comp (↑(fst φ)) hij).v p (q + 1) ⋯
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
⊢ γ₁.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:
simp only [Cochain.comp_v _ _ _ p q (q + 1) hpq rfl] at h₁

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
p q : ℤ
hpq : p + i = q
h₂ : (γ₁.comp (snd φ) ⋯).v p q hpq = (γ₂.comp (snd φ) ⋯).v p q hpq
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (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:
case mpr.intro
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 φ) ⋯
⊢ γ₁ = γ₂

Tactic:
ext p q hpq

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 = γ₂.v p q hpq

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
h₁ : γ₁.comp (↑(fst φ)) hij = γ₂.comp (↑(fst φ)) hij
h₂ : γ₁.comp (snd φ) ⋯ = γ₂.comp (snd φ) ⋯
p q : ℤ
hpq : p + i = q
⊢ p + j = q + 1

Tactic:
omega

Result:
no goals

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
p q : ℤ
hpq : p + i = q
h₁ : γ₁.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯ = γ₂.v p q hpq ≫ (↑(fst φ)).v q (q + 1) ⋯
h₂ : γ₁.v p q hpq ≫ (snd φ).v q q ⋯ = γ₂.v p q hpq ≫ (snd φ).v q 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:
exact ⟨h₁, h₂⟩

Result:
no goals

Proof state:
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 φ) ⋯

Tactic:
rintro rfl

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 φ) ⋯

Proof state:
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 φ) ⋯ → γ₁ = γ₂

Tactic:
rintro ⟨h₁, h₂⟩

Result:
case mpr.intro
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 φ) ⋯
⊢ γ₁ = γ₂

Proof state:
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 φ) ⋯

Tactic:
tauto

Result:
no goals