α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ dropSlice n m xs ~ ys ∩ dropSlice n m xs
simp only [dropSlice_eq]
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
have : n ≤ n + m := Nat.le_add_right _ _
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
have h₂ := h.nodup_iff.2 h'
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs

α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ Disjoint (take n xs) (drop (n + m) xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ (take n xs ++ drop (n + m) xs)
apply Perm.trans _ (Perm.inter_append _).symm
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ Disjoint (take n xs) (drop (n + m) xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs

α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ Disjoint (take n xs) (drop (n + m) xs)
. exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ Disjoint (take n xs) (drop (n + m) xs)
. exact disjoint_take_drop h₂ this
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ take n xs ++ drop (n + m) xs ~ ys ∩ take n xs ++ ys ∩ drop (n + m) xs
exact Perm.append (Perm.take_inter _ h h') (Perm.drop_inter _ h h')
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n m : ℕ
h : xs ~ ys
h' : Nodup ys
this : n ≤ n + m
h₂ : Nodup xs
⊢ Disjoint (take n xs) (drop (n + m) xs)
exact disjoint_take_drop h₂ this