no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s : CompositionSeries X
x : X
hsat : IsMaximal (top s) x
⊢ bot (snoc s x hsat) = bot s
rw [bot, bot, ← snoc_castSucc s _ _ 0, Fin.castSucc_zero]