English
If s1 ≃ s2 and there is an Iso between their last elements, then snoc preserves equivalence.
Русский
Если s1 эквивалентна s2 и существует изоморфизм между их последними элементами, то добавление нового элемента через snoc сохраняет эквивалентность.
LaTeX
$$$\\forall s_1\\ s_2,\\; s_1.Equivalent s_2 \\rightarrow (\\text{Iso} (s_1.\\last, x_1) (s_2.\\last, x_2)) \\rightarrow s_1. snoc x_1 h_sat_1 \\ Equiv s_2. snoc x_2 h_sat_2.$$$
Lean4
protected theorem snoc {s₁ s₂ : CompositionSeries X} {x₁ x₂ : X} {hsat₁ : IsMaximal s₁.last x₁}
{hsat₂ : IsMaximal s₂.last x₂} (hequiv : Equivalent s₁ s₂) (hlast : Iso (s₁.last, x₁) (s₂.last, x₂)) :
Equivalent (s₁.snoc x₁ hsat₁) (s₂.snoc x₂ hsat₂) :=
let e : Fin s₁.length.succ ≃ Fin s₂.length.succ :=
calc
Fin (s₁.length + 1) ≃ Option (Fin s₁.length) := finSuccEquivLast
_ ≃ Option (Fin s₂.length) := (Functor.mapEquiv Option hequiv.choose)
_ ≃ Fin (s₂.length + 1) := finSuccEquivLast.symm
⟨e, fun i => by
refine Fin.lastCases ?_ ?_ i
· simpa [e, apply_last] using hlast
· intro i
simpa [e, ← Fin.castSucc_succ] using hequiv.choose_spec i⟩
