English
If rij and rij' relate i to j, then the composition involving eqToHom from congr_arg C.X along c.prev_eq equals the appropriate differential: eqToHom(congr_arg C.X (c.prev_eq rij rij')) ≫ C.d i' j = C.d i j.
Русский
Если rij и rij' связывают i с j, то композиция с eqToHom от congr_arg C.X вдоль c.prev_eq равна дифференциалу: eqToHom(congr_arg C.X (c.prev_eq rij rij')) ≫ C.d i' j = C.d i j.
LaTeX
$$$\\\\eqToHom (congrArg C.X (c.prev_eq rij rij')) \\\\circ C.d i' j = C.d i j$$$
Lean4
/-- If `C.d i j` and `C.d i' j` are both allowed, then we must have `i = i'`,
and so the differentials only differ by an `eqToHom`.
-/
@[simp]
theorem eqToHom_comp_d {i i' j : ι} (rij : c.Rel i j) (rij' : c.Rel i' j) :
eqToHom (congr_arg C.X (c.prev_eq rij rij')) ≫ C.d i' j = C.d i j :=
by
obtain rfl := c.prev_eq rij rij'
simp only [eqToHom_refl, id_comp]
