case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)

case neg
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
⊢ drop n xs ~ List.inter ys (drop n xs)
by_cases h'' : n ≤ xs.length
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
⊢ drop n xs ~ List.inter ys (drop n xs)
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)
let n' := xs.length - n
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
⊢ drop n xs ~ List.inter ys (drop n xs)
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
⊢ drop n xs ~ List.inter ys (drop n xs)
have h₀ : n = xs.length - n' := by
  rwa [tsub_tsub_cancel_of_le]
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
⊢ drop n xs ~ List.inter ys (drop n xs)
have h₁ : n' ≤ xs.length := by apply tsub_le_self
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ drop n xs ~ List.inter ys (drop n xs)
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)
have h₂ : xs.drop n = (xs.reverse.take n').reverse := by
  rw [reverse_take _ h₁, h₀, reverse_reverse]
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ reverse (take n' (reverse xs)) ~ List.inter ys (reverse (take n' (reverse xs)))
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ drop n xs ~ List.inter ys (drop n xs)
rw [h₂]
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ take n' (reverse xs) ~ List.inter ys (reverse (take n' (reverse xs)))
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ reverse (take n' (reverse xs)) ~ List.inter ys (reverse (take n' (reverse xs)))
apply (reverse_perm _).trans
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ take n' (reverse xs) ~ List.inter ys (take n' (reverse xs))
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ take n' (reverse xs) ~ List.inter ys (reverse (take n' (reverse xs)))
rw [inter_reverse]
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ reverse xs ~ ys
case pos
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ take n' (reverse xs) ~ List.inter ys (take n' (reverse xs))
apply Perm.take_inter _ _ h'
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ xs ~ ys
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ reverse xs ~ ys
apply (reverse_perm _).trans
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
h₂ : drop n xs = reverse (take n' (reverse xs))
⊢ xs ~ ys
assumption
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
⊢ n = length xs - n'
rwa [tsub_tsub_cancel_of_le]
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
⊢ n' ≤ length xs
apply tsub_le_self
no goals
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : n ≤ length xs
n' : ℕ := length xs - n
h₀ : n = length xs - n'
h₁ : n' ≤ length xs
⊢ drop n xs = reverse (take n' (reverse xs))
rw [reverse_take _ h₁, h₀, reverse_reverse]
case neg
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
this : drop n xs = []
⊢ drop n xs ~ List.inter ys (drop n xs)
case neg
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ drop n xs ~ List.inter ys (drop n xs)
have : drop n xs = [] := by
  apply eq_nil_of_length_eq_zero
  rw [length_drop, tsub_eq_zero_iff_le]
  apply le_of_not_ge h''
no goals
case neg
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
this : drop n xs = []
⊢ drop n xs ~ List.inter ys (drop n xs)
simp [this, List.inter]
case x
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ length (drop n xs) = 0
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ drop n xs = []
apply eq_nil_of_length_eq_zero
case x
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ length xs ≤ n
case x
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ length (drop n xs) = 0
rw [length_drop, tsub_eq_zero_iff_le]
no goals
case x
α✝ : Type uu
β : Type vv
l₁ l₂ : List α✝
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : Nodup ys
h'' : ¬n ≤ length xs
⊢ length xs ≤ n
apply le_of_not_ge h''