-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma ext_cochain_from_iff (i j : ℤ) (hij : i + 1 = j)
    {K : CochainComplex C ℤ} {γ₁ γ₂ : Cochain (mappingCone φ) K j} :
    γ₁ = γ₂ ↔
      (inl φ).comp γ₁ (show _ = i by omega) = (inl φ).comp γ₂ (by omega) ∧
        (Cochain.ofHom (inr φ)).comp γ₁ (zero_add j) =
          (Cochain.ofHom (inr φ)).comp γ₂ (zero_add j)

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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
h₂ : (inr φ).f p ≫ γ₁.v p q ⋯ = (inr φ).f p ≫ γ₂.v p q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq

Tactic:
exact ⟨h₁, h₂⟩

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 (mappingCone φ) K j
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
p q : ℤ
hpq : p + j = q
h₁ : ((inl φ).comp γ₁ ⋯).v (p + 1) q ⋯ = ((inl φ).comp γ₂ ⋯).v (p + 1) q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq

Tactic:
replace h₂ := Cochain.congr_v h₂ p q (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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : ((inl φ).comp γ₁ ⋯).v (p + 1) q ⋯ = ((inl φ).comp γ₂ ⋯).v (p + 1) q ⋯
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.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 (mappingCone φ) K j
h₁ : (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
p q : ℤ
hpq : p + j = q
⊢ p + 1 + i = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{?u.77145, u_1} C
inst✝³ : Category.{?u.77149, u_2} D
inst✝² : Preadditive C
inst✝¹ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j : ℤ
hij : i + 1 = j
K : CochainComplex C ℤ
γ₁ γ₂ : Cochain (mappingCone φ) K j
⊢ -1 + j = i

Tactic:
omega

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 (mappingCone φ) K j
⊢ (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₁ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₁ ⋯

Tactic:
tauto

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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.v p q hpq

Tactic:
simp only [Cochain.zero_cochain_comp_v, Cochain.ofHom_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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq
h₂ : (inr φ).f p ≫ γ₁.v p q ⋯ = (inr φ).f p ≫ γ₂.v p q ⋯
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.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 (mappingCone φ) K j
⊢ γ₁ = γ₂ ↔
    (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯

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 (mappingCone φ) K j
⊢ γ₁ = γ₂ →
    (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯

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 (mappingCone φ) K j
⊢ (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯ ∧ (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯ →
    γ₁ = γ₂

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 (mappingCone φ) K j
p q : ℤ
hpq : p + j = q
h₁ : ((inl φ).comp γ₁ ⋯).v (p + 1) q ⋯ = ((inl φ).comp γ₂ ⋯).v (p + 1) q ⋯
h₂ : ((Cochain.ofHom (inr φ)).comp γ₁ ⋯).v p q ⋯ = ((Cochain.ofHom (inr φ)).comp γ₂ ⋯).v p q ⋯
⊢ p + 1 + -1 = p

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 (mappingCone φ) K j
h₁ : (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
p q : ℤ
hpq : p + j = q
⊢ γ₁.v p q hpq = γ₂.v p q hpq

Tactic:
rw [ext_from_iff φ (p + 1) p 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 (mappingCone φ) K j
h₁ : (inl φ).comp γ₁ ⋯ = (inl φ).comp γ₂ ⋯
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
p q : ℤ
hpq : p + j = q
⊢ (inl φ).v (p + 1) p ⋯ ≫ γ₁.v p q hpq = (inl φ).v (p + 1) p ⋯ ≫ γ₂.v p q hpq ∧
    (inr φ).f p ≫ γ₁.v p q hpq = (inr φ).f p ≫ γ₂.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 (mappingCone φ) K j
h₂ : (Cochain.ofHom (inr φ)).comp γ₁ ⋯ = (Cochain.ofHom (inr φ)).comp γ₂ ⋯
p q : ℤ
hpq : p + j = q
h₁ : ((inl φ).comp γ₁ ⋯).v (p + 1) q ⋯ = ((inl φ).comp γ₂ ⋯).v (p + 1) q ⋯
⊢ p + j = q

Tactic:
omega

Result:
no goals