no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : Equivalent s₁ s₂
i : Fin s₂.length
⊢ Iso (series s₁ (↑Fin.castSucc (↑(Exists.choose h).symm i)), series s₁ (Fin.succ (↑(Exists.choose h).symm i)))
    (series s₂ (↑Fin.castSucc i), series s₂ (Fin.succ i))
simpa using h.choose_spec (h.choose.symm i)