English
Two formPerm permutations are equal iff their underlying lists are rotation-equivalent (IsRotated).
Русский
Две перестановки formPerm равны тогда и только тогда, когда соответствующие списки являются вращениями друг друга (IsRotated).
LaTeX
$$$\forall {\alpha}\, [\DecidableEq\alpha],\forall (x y x' y' : \alpha)\{l l' : List \alpha\},\ hd : Nodup (x :: y :: l),\ hd' : Nodup (x' :: y' :: l'):\ formPerm (x :: y :: l) = formPerm (x' :: y' :: l') \\text{IsRotated}\ (x' :: y' :: l')$$$
Lean4
theorem formPerm_ext_iff {x y x' y' : α} {l l' : List α} (hd : Nodup (x :: y :: l)) (hd' : Nodup (x' :: y' :: l')) :
formPerm (x :: y :: l) = formPerm (x' :: y' :: l') ↔ (x :: y :: l) ~r (x' :: y' :: l') :=
by
refine ⟨fun h => ?_, fun hr => formPerm_eq_of_isRotated hd hr⟩
rw [Equiv.Perm.ext_iff] at h
have hx : x' ∈ x :: y :: l :=
by
have : x' ∈ {z | formPerm (x :: y :: l) z ≠ z} :=
by
rw [Set.mem_setOf_eq, h x', formPerm_apply_head _ _ _ hd']
simp only [mem_cons, nodup_cons] at hd'
push_neg at hd'
exact hd'.left.left.symm
simpa using support_formPerm_le' _ this
obtain ⟨⟨n, hn⟩, hx'⟩ := get_of_mem hx
have hl : (x :: y :: l).length = (x' :: y' :: l').length :=
by
rw [← dedup_eq_self.mpr hd, ← dedup_eq_self.mpr hd', ← card_toFinset, ← card_toFinset]
refine congr_arg Finset.card ?_
rw [← Finset.coe_inj, ← support_formPerm_of_nodup' _ hd (by simp), ← support_formPerm_of_nodup' _ hd' (by simp)]
simp only [h]
use n
apply List.ext_getElem
· rw [length_rotate, hl]
· intro k hk hk'
rw [getElem_rotate]
induction k with
| zero =>
refine Eq.trans ?_ hx'
congr
simpa using hn
| succ k IH =>
conv => congr <;> · arg 2; (rw [← Nat.mod_eq_of_lt hk'])
rw [← formPerm_apply_getElem _ hd' k (k.lt_succ_self.trans hk'), ← IH (k.lt_succ_self.trans hk), ← h,
formPerm_apply_getElem _ hd]
congr 1
rw [hl, Nat.mod_eq_of_lt hk', add_right_comm]
apply Nat.add_mod
