-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
lemma eq_add_nullHomotopic (h : Homotopy φ₁ φ₂) :
    φ₁ = φ₂ + nullHomotopic _ _ h.h₀ h.h₀_f h.h₁ h.h₂ h.h₃ h.g_h₃

Proof state:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Tactic:
rw [h.comm₃]

Result:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁ = φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯

Tactic:
ext

Result:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁

case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂

case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃

Proof state:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ h.h₃ + h.h₂ ≫ S₂.g + φ₂.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Tactic:
abel

Result:
no goals

Proof state:
case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₂

Tactic:
dsimp

Result:
case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Proof state:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
rw [h.comm₁]

Result:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Proof state:
case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Tactic:
abel

Result:
no goals

Proof state:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₃

Tactic:
dsimp

Result:
case h₃
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₃ = φ₂.τ₃ + (h.h₂ ≫ S₂.g + h.h₃)

Proof state:
case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Tactic:
rw [h.comm₂]

Result:
case h₂
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.g ≫ h.h₂ + h.h₁ ≫ S₂.f + φ₂.τ₂ = φ₂.τ₂ + (h.h₁ ≫ S₂.f + S₁.g ≫ h.h₂)

Proof state:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = (φ₂ + S₁.nullHomotopic S₂ h.h₀ ⋯ h.h₁ h.h₂ h.h₃ ⋯).τ₁

Tactic:
dsimp

Result:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ φ₁.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Proof state:
case h₁
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ₁ φ₂ : S₁ ⟶ S₂
h : Homotopy φ₁ φ₂
⊢ S₁.f ≫ h.h₁ + h.h₀ + φ₂.τ₁ = φ₂.τ₁ + (h.h₀ + S₁.f ≫ h.h₁)

Tactic:
abel

Result:
no goals