-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
lemma inrX_nullHomotopy_f (j : ι) :
    inrX K j ≫ (nullHomotopicMap K).f j = inrX K j ≫ (π K ≫ ι₀ K - 𝟙 _).f j

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
⊢ biprod.lift (𝟙 K) (-𝟙 K) ≫ biprod.snd = (biprod.inl - biprod.inr) ≫ biprod.snd

Tactic:
simp

Result:
no goals

Proof state:
case neg.h₀
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
simp

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ (K.biprodXIso K j).inv ≫
      biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (K.biprodXIso K j).inv ≫
      ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
ext

Result:
case neg.h₀
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inl ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

case neg.h₁
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Proof state:
case neg.h₁
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    biprod.inr ≫
      (K.biprodXIso K j).inv ≫
        ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)

Tactic:
simp [this]

Result:
no goals

Proof state:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ inrX K j ≫
      (Homotopy.nullHomotopicMap' fun i j hij =>
            homotopyCofiber.sndX (biprod.lift (𝟙 K) (-𝟙 K)) i ≫ biprod.snd.f i ≫ inlX K i j hij).f
        j =
    inrX K j ≫ ((π K).f j ≫ (ι₀ K).f j - 𝟙 (homotopyCofiber.X (biprod.lift (𝟙 K) (-𝟙 K)) j))

Tactic:
simp only [assoc, Homotopy.nullHomotopicMap'_f_of_not_rel_left hij hj, homotopyCofiber_X,
  homotopyCofiber_d, homotopyCofiber.inlX_d' _ _ _ _ (hj _), homotopyCofiber.inrX_sndX_assoc,
  comp_sub, inrX_π_assoc, comp_id, ι₀, comp_f, homotopyCofiber.inr_f]

Result:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j

Proof state:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j

Tactic:
rw [← cancel_epi (biprodXIso K K j).inv]

Result:
case neg
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
inst✝² : DecidableRel c.Rel
inst✝¹ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (K.X i)
inst✝ : HasHomotopyCofiber (biprod.lift (𝟙 K) (-𝟙 K))
hc : ∀ (j : ι), ∃ i, c.Rel i j
j : ι
this : biprod.lift (𝟙 K) (-𝟙 K) = biprod.inl - biprod.inr
i : ι
hij : c.Rel i j
hj : ∀ (x : ι), ¬c.Rel j x
⊢ (K.biprodXIso K j).inv ≫
      biprod.snd.f j ≫ (biprod.lift (𝟙 K) (-𝟙 K)).f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j =
    (K.biprodXIso K j).inv ≫
      ((biprod.desc (𝟙 K) (𝟙 K)).f j ≫ biprod.inl.f j ≫ homotopyCofiber.inrX (biprod.lift (𝟙 K) (-𝟙 K)) j - inrX K j)