English
For xs ∼ ys and ys Nodup, the dropSlice n m of xs is a permutation of ys ∩ dropSlice n m xs.
Русский
Для xs ∼ ys и ys Nodup, List.dropSlice n m xs перестановочно эквивалентна ys ∩ List.dropSlice n m xs.
LaTeX
$$$\forall n\, m\, (xs \sim ys) \land ys.Nodup \Rightarrow (List.dropSlice\ n\ m\ xs) \sim (ys \cap List.dropSlice\ n\ m\ xs)$$$
Lean4
theorem dropSlice_inter {xs ys : List α} (n m : ℕ) (h : xs ~ ys) (h' : ys.Nodup) :
List.dropSlice n m xs ~ ys ∩ List.dropSlice n m xs :=
by
simp only [dropSlice_eq]
have : n ≤ n + m := Nat.le_add_right _ _
have h₂ := h.nodup_iff.2 h'
apply Perm.trans _ (Perm.inter_append _).symm
· exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
· exact disjoint_take_drop h₂ this
