-- Mathlib/Data/List/Perm/Lattice.lean
theorem Perm.drop_inter {xs ys : List α} (n : ℕ) (h : xs ~ ys) (h' : ys.Nodup) :
    xs.drop n ~ ys.inter (xs.drop n)

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
let n' := xs.length - n

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ drop n xs ~ ys.inter (drop n xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ xs ~ ys

Tactic:
assumption

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ (take n' xs.reverse).reverse ~ ys.inter (take n' xs.reverse).reverse

Tactic:
apply (reverse_perm _).trans

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ take n' xs.reverse ~ ys.inter (take n' xs.reverse).reverse

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
have : drop n xs = [] := by
  apply eq_nil_of_length_eq_zero
  rw [length_drop, Nat.sub_eq_zero_iff_le]
  apply le_of_not_ge h''

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
this : drop n xs = []
⊢ drop n xs ~ ys.inter (drop n xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ xs.reverse ~ ys

Tactic:
apply (reverse_perm _).trans

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ xs ~ ys

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ take n' xs.reverse ~ ys.inter (take n' xs.reverse).reverse

Tactic:
rw [inter_reverse]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ take n' xs.reverse ~ ys.inter (take n' xs.reverse)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ n = xs.length - n'

Tactic:
rwa [Nat.sub_sub_self]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
have h₁ : xs.drop n = (xs.reverse.take n').reverse := by
  rw [take_reverse, h₀, reverse_reverse]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ drop n xs ~ ys.inter (drop n xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ drop n xs = []

Tactic:
apply eq_nil_of_length_eq_zero

Result:
case x
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ (drop n xs).length = 0

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
have h₀ : n = xs.length - n' := by rwa [Nat.sub_sub_self]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ drop n xs ~ ys.inter (drop n xs)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
by_cases h'' : n ≤ xs.length

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
⊢ drop n xs ~ ys.inter (drop n xs)

case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ drop n xs ~ ys.inter (drop n xs)

Proof state:
case x
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ (drop n xs).length = 0

Tactic:
rw [length_drop, Nat.sub_eq_zero_iff_le]

Result:
case x
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ xs.length ≤ n

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
this : drop n xs = []
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
simp [this, List.inter]

Result:
no goals

Proof state:
case x
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : ¬n ≤ xs.length
⊢ xs.length ≤ n

Tactic:
apply le_of_not_ge h''

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
⊢ drop n xs = (take n' xs.reverse).reverse

Tactic:
rw [take_reverse, h₀, reverse_reverse]

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ take n' xs.reverse ~ ys.inter (take n' xs.reverse)

Tactic:
apply Perm.take_inter _ _ h'

Result:
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ xs.reverse ~ ys

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ drop n xs ~ ys.inter (drop n xs)

Tactic:
rw [h₁]

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
xs ys : List α
n : ℕ
h : xs ~ ys
h' : ys.Nodup
h'' : n ≤ xs.length
n' : ℕ := xs.length - n
h₀ : n = xs.length - n'
h₁ : drop n xs = (take n' xs.reverse).reverse
⊢ (take n' xs.reverse).reverse ~ ys.inter (take n' xs.reverse).reverse