English
If x is not the last element and x ∈ s, then x ∈ s.eraseLast.
Русский
Если x не равен последнему элементу и x принадлежит серии, то x принадлежит eraseLast.
LaTeX
$$$\\forall {X} [\\mathrm{Lattice}\\ X] [\\mathrm{JordanHolderLattice}\\ X],\\ {s : \\mathrm{CompositionSeries}\\ X},\\ {x : X},\\ x \\neq \\mathrm{RelSeries}.last\\ s \\to \\mathrm{RelSeries}.membership.mem s x \\to \\mathrm{RelSeries}.membership.mem (\\mathrmRelSeries.eraseLast s) x.$$$
Lean4
theorem mem_eraseLast_of_ne_of_mem {s : CompositionSeries X} {x : X} (hx : x ≠ s.last) (hxs : x ∈ s) :
x ∈ s.eraseLast := by
rcases hxs with ⟨i, rfl⟩
have hi : (i : ℕ) < (s.length - 1).succ :=
by
conv_rhs => rw [← Nat.succ_sub (length_pos_of_nontrivial ⟨_, ⟨i, rfl⟩, _, s.last_mem, hx⟩), Nat.add_one_sub_one]
exact lt_of_le_of_ne (Nat.le_of_lt_succ i.2) (by simpa [last, s.inj, Fin.ext_iff] using hx)
exact ⟨⟨↑i, hi⟩, by simp⟩
