-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[reassoc]
lemma inl_v_d (i j k : ℤ) (hij : i + (-1) = j) (hik : k + (-1) = i) :
    (inl φ).v i j hij ≫ (mappingCone φ).d j i =
      φ.f i ≫ (inr φ).f i - F.d i k ≫ (inl φ).v _ _ hik

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ j + 1 = i

Tactic:
omega

Result:
no goals

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel j i

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ j + 1 = i

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ homotopyCofiber.inlX φ i j ⋯ ≫ homotopyCofiber.d φ j i =
    φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯

Tactic:
rw [homotopyCofiber.inlX_d φ j i k (by dsimp; omega) (by dsimp; omega)]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ -F.d i k ≫ homotopyCofiber.inlX φ k i ⋯ + φ.f i ≫ homotopyCofiber.inrX φ i =
    φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ -F.d i k ≫ homotopyCofiber.inlX φ k i ⋯ + φ.f i ≫ homotopyCofiber.inrX φ i =
    φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯

Tactic:
abel

Result:
no goals

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (inl φ).v i j hij ≫ (mappingCone φ).d j i = φ.f i ≫ (inr φ).f i - F.d i k ≫ (inl φ).v k i hik

Tactic:
dsimp [mappingCone, inl, inr]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ homotopyCofiber.inlX φ i j ⋯ ≫ homotopyCofiber.d φ j i =
    φ.f i ≫ homotopyCofiber.inrX φ i - F.d i k ≫ homotopyCofiber.inlX φ k i ⋯

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ i + 1 = k

Tactic:
omega

Result:
no goals

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 k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ (ComplexShape.up ℤ).Rel i k

Tactic:
dsimp

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
i j k : ℤ
hij : i + -1 = j
hik : k + -1 = i
⊢ i + 1 = k