no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ toList s₁ ~ toList s₂
classical
exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
  (Finset.ext <| by simp [*])
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ toList s₁ ~ toList s₂
exact List.perm_of_nodup_nodup_toFinset_eq s₁.toList_nodup s₂.toList_nodup
  (Finset.ext <| by simp [*])
no goals
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
h : ∀ (x : X), x ∈ s₁ ↔ x ∈ s₂
⊢ ∀ (a : X), a ∈ List.toFinset (toList s₁) ↔ a ∈ List.toFinset (toList s₂)
simp [*]