Theorem: List.uniqueAux_acc_append (Table/BuiltinExtensions.lean)

State before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ uniqueAux xs acc = reverse acc ++ unique xs
Tactic:
have : filter (fun a => decide ¬a ∈ acc) xs = xs := by
  induction xs with
  | nil => simp [filter]
  | cons x xs ih =>
    simp only [filter]
    have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
    rw [this]
    simp only
    rw [ih]
    . intros x hx
      apply h x (Mem.tail _ hx)
State after:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ uniqueAux xs acc = reverse acc ++ unique xs

State before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ uniqueAux xs acc = reverse acc ++ unique xs
Tactic:
rw [uniqueAux_acc_append_filter]
State after:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs) = reverse acc ++ unique xs

State before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) xs = xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs) = reverse acc ++ unique xs
Tactic:
cases xs with
| nil => apply congrArg; simp [filter]
| cons x xs =>
  apply congrArg
  rw [this]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
xs acc : List α
h : ∀ (x : α), x ∈ xs → ¬x ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) xs = xs
Tactic:
induction xs with
| nil => simp [filter]
| cons x xs ih =>
  simp only [filter]
  have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
  rw [this]
  simp only
  rw [ih]
  . intros x hx
    apply h x (Mem.tail _ hx)
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) [] = []
Tactic:
simp [filter]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
Tactic:
simp only [filter]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
have : decide (¬x ∈ acc) = true := by simp [h x (Mem.head _)]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match decide ¬x ∈ acc with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
rw [this]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match true with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ (match true with
    | true => x :: filter (fun a => decide ¬a ∈ acc) xs
    | false => filter (fun a => decide ¬a ∈ acc) xs) =
    x :: xs
Tactic:
simp only
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ x :: filter (fun a => decide ¬a ∈ acc) xs = x :: xs

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ x :: filter (fun a => decide ¬a ∈ acc) xs = x :: xs
Tactic:
rw [ih]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc
Tactic:
. intros x hx
  apply h x (Mem.tail _ hx)
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
⊢ (decide ¬x ∈ acc) = true
Tactic:
simp [h x (Mem.head _)]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : (decide ¬x ∈ acc) = true
⊢ ∀ (x : α), x ∈ xs → ¬x ∈ acc
Tactic:
intros x hx
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x✝ : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x : α), x ∈ x✝ :: xs → ¬x ∈ acc
this : (decide ¬x✝ ∈ acc) = true
x : α
hx : x ∈ xs
⊢ ¬x ∈ acc

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x✝ : α
xs : List α
ih : (∀ (x : α), x ∈ xs → ¬x ∈ acc) → filter (fun a => decide ¬a ∈ acc) xs = xs
h : ∀ (x : α), x ∈ x✝ :: xs → ¬x ∈ acc
this : (decide ¬x✝ ∈ acc) = true
x : α
hx : x ∈ xs
⊢ ¬x ∈ acc
Tactic:
apply h x (Mem.tail _ hx)
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) []) = reverse acc ++ unique []
Tactic:
apply congrArg
State after:
case nil.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ unique (filter (fun x => decide ¬x ∈ acc) []) = unique []

State before:
case nil.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
h : ∀ (x : α), x ∈ [] → ¬x ∈ acc
this : filter (fun a => decide ¬a ∈ acc) [] = []
⊢ unique (filter (fun x => decide ¬x ∈ acc) []) = unique []
Tactic:
simp [filter]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = reverse acc ++ unique (x :: xs)
Tactic:
apply congrArg
State after:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = unique (x :: xs)

State before:
case cons.h
α : Type u_1
inst✝ : DecidableEq α
acc : List α
x : α
xs : List α
h : ∀ (x_1 : α), x_1 ∈ x :: xs → ¬x_1 ∈ acc
this : filter (fun a => decide ¬a ∈ acc) (x :: xs) = x :: xs
⊢ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs)) = unique (x :: xs)
Tactic:
rw [this]
State after:
no goals