-- Mathlib/Data/List/Dedup.lean
theorem Disjoint.union_eq {xs ys : List α} (h : Disjoint xs ys) :
    xs ∪ ys = xs.dedup ++ ys

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [disjoint_cons_left] at h

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_mem hx, insert_of_mem (mem_union_left hx _), ih h.2]

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ x ∉ xs ∧ x ∉ ys

Tactic:
exact ⟨hx, h.1⟩

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ x ∉ xs ∪ ys

Tactic:
rw [mem_union_iff, not_or]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ x ∉ xs ∧ x ∉ ys

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
rw [dedup_cons_of_not_mem hx, insert_of_not_mem, ih h.2, cons_append]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ x ∉ xs ∪ ys

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
ys : List α
h : [].Disjoint ys
⊢ [] ∪ ys = [].dedup ++ ys

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Tactic:
by_cases hx : x ∈ xs

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∈ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

case neg
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : x ∉ ys ∧ xs.Disjoint ys
hx : x ∉ xs
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ x :: xs ∪ ys = (x :: xs).dedup ++ ys

Tactic:
rw [cons_union]

Result:
case cons
α : Type u_1
inst✝ : DecidableEq α
ys : List α
x : α
xs : List α
ih : xs.Disjoint ys → xs ∪ ys = xs.dedup ++ ys
h : (x :: xs).Disjoint ys
⊢ List.insert x (xs ∪ ys) = (x :: xs).dedup ++ ys