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.natAdd s₁.length) i)) = series s₂ (Fin.succ i)
rw [coe_append, append_succ_natAdd_aux _ _ i]