English
If j = i.succ.castSucc, then mkOfSucc i ≫ δ_j equals the interval edge from i to i+2.
Русский
Если j = i.succ.castSucc, то mkOfSucc i ∘ δ_j равняется интервалу ребра от i до i+2.
LaTeX
$$$\\text{If } j = i.\\succ.castSucc, \\ mkOfSucc i \\circ δ_j = intervalEdge i 2$$$
Lean4
/-- If `i + 1 = j`, `mkOfSucc i ≫ δ j` is the morphism `⦋1⦌ ⟶ ⦋n⦌` that
sends `0` and `1` to `i` and `i + 2`, respectively. -/
theorem mkOfSucc_δ_eq {n : ℕ} {i : Fin n} {j : Fin (n + 2)} (h : j = i.succ.castSucc) :
mkOfSucc i ≫ δ j = intervalEdge i 2 (by cutsat) := by
ext x
fin_cases x
· subst h
simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.zero_eta, OrderHom.comp_coe,
OrderEmbedding.toOrderHom_coe, Function.comp_apply, mkOfSucc_homToOrderHom_zero, Fin.succAboveOrderEmb_apply,
Fin.castSucc_succAbove_castSucc, Fin.succAbove_succ_self]
rfl
· simp only [δ, len_mk, Nat.reduceAdd, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, Fin.mk_one, OrderHom.comp_coe,
OrderEmbedding.toOrderHom_coe, Function.comp_apply, mkOfSucc_homToOrderHom_one, Fin.succAboveOrderEmb_apply]
subst h
rw [Fin.succAbove_castSucc_self]
rfl
