no goals
α : Type u_1
m n : Nat
x✝¹ : Nodup []
x✝ : m ≤ n
⊢ Disjoint (take m []) (drop n [])
simp
case succ.zero
α : Type u_1
x : α
xs : List α
hl : Nodup (x :: xs)
n✝ : Nat
h : succ n✝ ≤ zero
⊢ False

case succ.succ
α : Type u_1
x : α
xs : List α
hl : Nodup (x :: xs)
n✝¹ n✝ : Nat
h : succ n✝¹ ≤ succ n✝
⊢ ¬x ∈ drop n✝ xs ∧ Disjoint (take n✝¹ xs) (drop n✝ xs)
α : Type u_1
m n : Nat
x : α
xs : List α
hl : Nodup (x :: xs)
h : m ≤ n
⊢ Disjoint (take m (x :: xs)) (drop n (x :: xs))
cases m <;> cases n <;> simp only [disjoint_cons_left, mem_cons, disjoint_cons_right,
  drop, true_or, eq_self_iff_true, not_true, false_and, not_mem_nil, disjoint_nil_left, take]
no goals
case succ.zero
α : Type u_1
x : α
xs : List α
hl : Nodup (x :: xs)
n✝ : Nat
h : succ n✝ ≤ zero
⊢ False
case succ.zero => cases h
no goals
α : Type u_1
x : α
xs : List α
hl : Nodup (x :: xs)
n✝ : Nat
h : succ n✝ ≤ zero
⊢ False
cases h
no goals
case succ.succ
α : Type u_1
x : α
xs : List α
hl : Nodup (x :: xs)
n✝¹ n✝ : Nat
h : succ n✝¹ ≤ succ n✝
⊢ ¬x ∈ drop n✝ xs ∧ Disjoint (take n✝¹ xs) (drop n✝ xs)
cases hl with | cons h₀ h₁ =>
refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : succ n✝¹ ≤ succ n✝
h₁ : Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ Disjoint (take n✝¹ xs) (drop n✝ xs)
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : succ n✝¹ ≤ succ n✝
h₁ : Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ ¬x ∈ drop n✝ xs ∧ Disjoint (take n✝¹ xs) (drop n✝ xs)
refine ⟨fun h => h₀ _ (mem_of_mem_drop h) rfl, ?_⟩
no goals
case succ.succ.cons
α : Type u_1
x : α
xs : List α
n✝¹ n✝ : Nat
h : succ n✝¹ ≤ succ n✝
h₁ : Pairwise (fun x x_1 => x ≠ x_1) xs
h₀ : ∀ (a' : α), a' ∈ xs → x ≠ a'
⊢ Disjoint (take n✝¹ xs) (drop n✝ xs)
exact disjoint_take_drop h₁ (Nat.le_of_succ_le_succ h)