English
If xs ∼ ys and ys Nodup, then the tail xs.drop n is a permutation of the intersection ys ∩ (xs.drop n).
Русский
Если xs ∼ ys и ys Nodup, то хвост xs.drop n перестановочно эквивалентен ys ∩ (xs.drop n).
LaTeX
$$$\forall n,\; xs \sim ys \land ys.Nodup \Rightarrow (xs.drop n) \sim (ys \cap (xs.drop n))$$$
Lean4
theorem drop_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) : xs.drop n ~ ys.inter (xs.drop n) :=
by
by_cases h'' : n ≤ xs.length
· let n' := xs.length - n
have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]
have h₁ : xs.drop n = (xs.reverse.take n').reverse := by rw [take_reverse, h₀, reverse_reverse]
rw [h₁]
apply (reverse_perm _).trans
rw [inter_reverse]
apply Perm.take_inter _ _ h'
apply (reverse_perm _).trans; assumption
· have : xs.drop n = [] := by
apply eq_nil_of_length_eq_zero
rw [length_drop, Nat.sub_eq_zero_iff_le]
apply le_of_not_ge h''
simp [this, List.inter]
