English
If two lists are permutations of each other and are sorted with respect to a relation that is antisymmetric, then the lists are equal provided appropriate order constraints hold.
Русский
Если два списка перестановочно эквивалентны и упорядочены относительно антисимметричной связи, то при соблюдении соответствующих условий порядок их элементов совпадает и списки равны.
LaTeX
$$$ l_1 \\Perm l_2 \\to l_1.Sorted r \\to l_2.Sorted r \\to l_1 = l_2 $$$
Lean4
theorem eq_of_perm_of_sorted [IsAntisymm α r] {l₁ l₂ : List α} (hp : l₁ ~ l₂) (hs₁ : Sorted r l₁) (hs₂ : Sorted r l₂) :
l₁ = l₂ := by
induction hs₁ generalizing l₂ with
| nil => exact hp.nil_eq
| @cons a l₁ h₁ hs₁ IH =>
have : a ∈ l₂ := hp.subset mem_cons_self
rcases append_of_mem this with ⟨u₂, v₂, rfl⟩
have hp' := (perm_cons a).1 (hp.trans perm_middle)
obtain rfl := IH hp' (hs₂.sublist <| by simp)
change a :: u₂ ++ v₂ = u₂ ++ ([a] ++ v₂)
rw [← append_assoc]
congr
have : ∀ x ∈ u₂, x = a := fun x m => antisymm ((pairwise_append.1 hs₂).2.2 _ m a mem_cons_self) (h₁ _ (by simp [m]))
rw [(@eq_replicate_iff _ a (length u₂ + 1) (a :: u₂)).2, (@eq_replicate_iff _ a (length u₂ + 1) (u₂ ++ [a])).2] <;>
constructor <;>
simp [iff_true_intro this, or_comm]
