inrCompHomotopy — Mathlib

Lean4
/-- The composition `φ ≫ mappingCone.inr φ` is homotopic to `0`. -/
noncomputable def inrCompHomotopy (hc : ∀ j, ∃ i, c.Rel i j) : Homotopy (φ ≫ inr φ) 0
    where
  hom i j := if hij : c.Rel j i then inlX φ i j hij else 0
  zero _ _ hij := dif_neg hij
  comm
    j := by
    obtain ⟨i, hij⟩ := hc j
    rw [prevD_eq _ hij, dif_pos hij]
    by_cases hj : c.Rel j (c.next j)
    ·
      simp only [comp_f, homotopyCofiber_d, zero_f, add_zero, inlX_d φ i j _ hij hj, dNext_eq _ hj, dif_pos hj,
        add_neg_cancel_left, inr_f]
    · rw [dNext_eq_zero _ _ hj, zero_add, zero_f, add_zero, homotopyCofiber_d, inlX_d' _ _ _ _ hj, comp_f, inr_f]
Похожие утверждения