desc — Mathlib

Lean4
/-- The morphism `homotopyCofiber φ ⟶ K` that is induced by a morphism `α : G ⟶ K`
and a homotopy `hα : Homotopy (φ ≫ α) 0`. -/
noncomputable def desc : homotopyCofiber φ ⟶ K
    where
  f j := if hj : c.Rel j (c.next j) then fstX φ j _ hj ≫ hα.hom _ j + sndX φ j ≫ α.f j else sndX φ j ≫ α.f j
  comm' j k
    hjk := by
    obtain rfl := c.next_eq' hjk
    simp [dif_pos hjk]
    have H := hα.comm (c.next j)
    simp only [comp_f, zero_f, add_zero, prevD_eq _ hjk] at H
    split_ifs with hj
    · simp only [comp_add, d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, d_fstX_assoc _ _ _ _ hjk, neg_comp, dNext,
        AddMonoidHom.mk'_apply]
      abel
    · simp only [d_sndX_assoc _ _ _ hjk, add_comp, assoc, H, dNext_eq_zero _ _ hj, zero_add]
Похожие утверждения