no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : top s₁ = bot s₂
i : Fin s₁.length
⊢ series (append s₁ s₂ h) (Fin.succ (↑(Fin.castAdd s₂.length) i)) = series s₁ (Fin.succ i)
rw [coe_append, append_succ_castAdd_aux _ _ _ h]