case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ∩ (t₁ ++ t₂) ~ tail✝ ∩ t₁ ++ tail✝ ∩ t₂
⊢ (head✝ :: tail✝) ∩ (t₁ ++ t₂) ~ (head✝ :: tail✝) ∩ t₁ ++ (head✝ :: tail✝) ∩ t₂
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
l t₁ t₂ : List α
h : Disjoint t₁ t₂
⊢ l ∩ (t₁ ++ t₂) ~ l ∩ t₁ ++ l ∩ t₂
induction l
case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ∩ (t₁ ++ t₂) ~ tail✝ ∩ t₁ ++ tail✝ ∩ t₂
⊢ (head✝ :: tail✝) ∩ (t₁ ++ t₂) ~ (head✝ :: tail✝) ∩ t₁ ++ (head✝ :: tail✝) ∩ t₂
case nil
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂

case cons
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
head✝ : α
tail✝ : List α
tail_ih✝ : tail✝ ∩ (t₁ ++ t₂) ~ tail✝ ∩ t₁ ++ tail✝ ∩ t₂
⊢ (head✝ :: tail✝) ∩ (t₁ ++ t₂) ~ (head✝ :: tail✝) ∩ t₁ ++ (head✝ :: tail✝) ∩ t₂
case nil => simp
no goals
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
⊢ [] ∩ (t₁ ++ t₂) ~ [] ∩ t₁ ++ [] ∩ t₂
simp
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
by_cases h₁ : x ∈ t₁
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂

case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
by_cases h₂ : x ∈ t₂
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
have h₂ : x ∉ t₂ := h h₁
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
simp [*]
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ x :: xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
simp only [*, inter_cons_of_not_mem, false_or_iff, mem_append, inter_cons_of_mem,
  not_false_iff]
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ x :: (xs ∩ t₁ ++ xs ∩ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ x :: xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
refine' Perm.trans (Perm.cons _ l_ih) _
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ ([x] ++ xs ∩ t₂)
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ x :: (xs ∩ t₁ ++ xs ∩ t₂) ~ xs ∩ t₁ ++ x :: xs ∩ t₂
change [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ ([x] ++ xs ∩ t₂)
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ [x] ++ xs ∩ t₂
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ ([x] ++ xs ∩ t₂)
rw [← List.append_assoc]
no goals
case pos
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : x ∈ t₂
⊢ [x] ++ xs ∩ t₁ ++ xs ∩ t₂ ~ xs ∩ t₁ ++ [x] ++ xs ∩ t₂
solve_by_elim [Perm.append_right, perm_append_comm]
no goals
case neg
α : Type uu
β : Type vv
l₁ l₂ : List α
inst✝ : DecidableEq α
t₁ t₂ : List α
h : Disjoint t₁ t₂
x : α
xs : List α
l_ih : xs ∩ (t₁ ++ t₂) ~ xs ∩ t₁ ++ xs ∩ t₂
h₁ : ¬x ∈ t₁
h₂ : ¬x ∈ t₂
⊢ (x :: xs) ∩ (t₁ ++ t₂) ~ (x :: xs) ∩ t₁ ++ (x :: xs) ∩ t₂
simp [*]