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

State before:
α : Type u_1
inst✝ : DecidableEq α
acc : List α
⊢ uniqueAux [] acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) [])
Tactic:
simp [uniqueAux, reverse, reverseAux, unique]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
⊢ uniqueAux (x :: xs) acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) (x :: xs))
Tactic:
simp only [uniqueAux, filter]
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
⊢ (if x ∈ acc then uniqueAux xs acc else uniqueAux xs (x :: acc)) =
    reverse acc ++
      unique
        (match decide ¬x ∈ acc with
        | true => x :: filter (fun x => decide ¬x ∈ acc) xs
        | false => filter (fun x => decide ¬x ∈ acc) xs)

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
⊢ (if x ∈ acc then uniqueAux xs acc else uniqueAux xs (x :: acc)) =
    reverse acc ++
      unique
        (match decide ¬x ∈ acc with
        | true => x :: filter (fun x => decide ¬x ∈ acc) xs
        | false => filter (fun x => decide ¬x ∈ acc) xs)
Tactic:
cases Decidable.em (x ∈ acc) with
| inl hin =>
  simp only [hin, ite_true, not_true_eq_false, decide_False]
  rw [ih₁]
| inr hout =>
  simp only [hout, ite_false, not_false_eq_true, decide_True]
  simp only [reverse_singleton, singleton_append, unique,
             uniqueAux, List.not_mem_nil, ite_false]
  rw [ih₂]
  simp only [reverse_cons, append_assoc, singleton_append]
  apply congrArg
  simp only [unique]
  rw [ih₃]
  rw [reverse_singleton, singleton_append, filter_filter]
  have : (λ x_1 => decide (
          (decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)
         ) = (λ x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) := by
    apply funext
    intro x_1
    simp only [decide_not, Bool.not_eq_true']
    cases Decidable.em (x_1 ∈ acc) with
    | inl hmem =>
      simp only [hmem, decide_True, not_true_eq_false, false_and]
    | inr hnmem =>
      simp only [hnmem, decide_False, not_false_eq_true, true_and,
                 decide_not]
      cases Decidable.em (x_1 ∈ [x]) with
      | inl hmem' => simp only [hmem', decide_True, decide_False, not]
      | inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
  rw [this, ←unique]
  apply congrArg
  apply congrArg
  have h_mem_iff := mem_cons_iff_mem_singleton_or_tail x acc
  have h_mem_iff_neg := (λ x => Iff.not_iff_not_of_iff $ h_mem_iff x)
  apply congr _ rfl
  apply congr rfl
  apply funext
  intros a
  apply Decidable.prop_eq_of_decide_eq
  rw [h_mem_iff_neg, not_or_distrib, And.comm]
State after:
no goals

State before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hin : x ∈ acc
⊢ (if x ∈ acc then uniqueAux xs acc else uniqueAux xs (x :: acc)) =
    reverse acc ++
      unique
        (match decide ¬x ∈ acc with
        | true => x :: filter (fun x => decide ¬x ∈ acc) xs
        | false => filter (fun x => decide ¬x ∈ acc) xs)
Tactic:
simp only [hin, ite_true, not_true_eq_false, decide_False]
State after:
case inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hin : x ∈ acc
⊢ uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)

State before:
case inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hin : x ∈ acc
⊢ uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
Tactic:
rw [ih₁]
State after:
no goals

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ (if x ∈ acc then uniqueAux xs acc else uniqueAux xs (x :: acc)) =
    reverse acc ++
      unique
        (match decide ¬x ∈ acc with
        | true => x :: filter (fun x => decide ¬x ∈ acc) xs
        | false => filter (fun x => decide ¬x ∈ acc) xs)
Tactic:
simp only [hout, ite_false, not_false_eq_true, decide_True]
State after:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ uniqueAux xs (x :: acc) = reverse acc ++ unique (x :: filter (fun x => decide ¬x ∈ acc) xs)

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ uniqueAux xs (x :: acc) = reverse acc ++ unique (x :: filter (fun x => decide ¬x ∈ acc) xs)
Tactic:
simp only [reverse_singleton, singleton_append, unique,
           uniqueAux, List.not_mem_nil, ite_false]
State after:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ uniqueAux xs (x :: acc) = reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ uniqueAux xs (x :: acc) = reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]
Tactic:
rw [ih₂]
State after:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]
Tactic:
simp only [reverse_cons, append_assoc, singleton_append]
State after:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ reverse acc ++ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]

State before:
case inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ reverse acc ++ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    reverse acc ++ uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]
Tactic:
apply congrArg
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) = uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) = uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]
Tactic:
simp only [unique]
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    uniqueAux (filter (fun x => decide ¬x ∈ acc) xs) [x]
Tactic:
rw [ih₃]
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
Tactic:
rw [reverse_singleton, singleton_append, filter_filter]
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    x :: unique (filter (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) xs)

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    x :: unique (filter (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) xs)
Tactic:
have : (λ x_1 => decide (
        (decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)
       ) = (λ x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) := by
  apply funext
  intro x_1
  simp only [decide_not, Bool.not_eq_true']
  cases Decidable.em (x_1 ∈ acc) with
  | inl hmem =>
    simp only [hmem, decide_True, not_true_eq_false, false_and]
  | inr hnmem =>
    simp only [hnmem, decide_False, not_false_eq_true, true_and,
               decide_not]
    cases Decidable.em (x_1 ∈ [x]) with
    | inl hmem' => simp only [hmem', decide_True, decide_False, not]
    | inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    x :: unique (filter (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) xs)

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ x :: uniqueAux (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) [] =
    x :: unique (filter (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) xs)
Tactic:
rw [this, ←unique]
State after:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    x :: unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)

State before:
case inr.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ x :: unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    x :: unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)
Tactic:
apply congrArg
State after:
case inr.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)

State before:
case inr.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs) =
    unique (filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs)
Tactic:
apply congrArg
State after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs

State before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
have h_mem_iff := mem_cons_iff_mem_singleton_or_tail x acc
State after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs

State before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
have h_mem_iff_neg := (λ x => Iff.not_iff_not_of_iff $ h_mem_iff x)
State after:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs

State before:
case inr.h.h.h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs = filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
apply congr _ rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (filter fun x_1 => decide ¬x_1 ∈ x :: acc) = fun xs => filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (filter fun x_1 => decide ¬x_1 ∈ x :: acc) = fun xs => filter (fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])) xs
Tactic:
apply congr rfl
State after:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (fun x_1 => decide ¬x_1 ∈ x :: acc) = fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ (fun x_1 => decide ¬x_1 ∈ x :: acc) = fun x_1 => decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
apply funext
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ ∀ (x_1 : α), (decide ¬x_1 ∈ x :: acc) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
⊢ ∀ (x_1 : α), (decide ¬x_1 ∈ x :: acc) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
intros a
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (decide ¬a ∈ x :: acc) = decide (¬a ∈ acc ∧ ¬a ∈ [x])

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (decide ¬a ∈ x :: acc) = decide (¬a ∈ acc ∧ ¬a ∈ [x])
Tactic:
apply Decidable.prop_eq_of_decide_eq
State after:
case h.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (¬a ∈ x :: acc) = (¬a ∈ acc ∧ ¬a ∈ [x])

State before:
case h.a
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
this :
  (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
h_mem_iff : ∀ (x_1 : α), x_1 ∈ x :: acc ↔ x_1 ∈ [x] ∨ x_1 ∈ acc
h_mem_iff_neg : ∀ (x_1 : α), ¬x_1 ∈ x :: acc ↔ ¬(x_1 ∈ [x] ∨ x_1 ∈ acc)
a : α
⊢ (¬a ∈ x :: acc) = (¬a ∈ acc ∧ ¬a ∈ [x])
Tactic:
rw [h_mem_iff_neg, not_or_distrib, And.comm]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ (fun x_1 => decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true)) = fun x_1 =>
    decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
apply funext
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ ∀ (x_1 : α), decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_1 => decide ¬x_1 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_1 => decide ¬x_1 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
⊢ ∀ (x_1 : α), decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
intro x_1
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide ((decide ¬x_1 ∈ acc) = true ∧ (decide ¬x_1 ∈ [x]) = true) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [decide_not, Bool.not_eq_true']
State after:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])

State before:
case h
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
cases Decidable.em (x_1 ∈ acc) with
| inl hmem =>
  simp only [hmem, decide_True, not_true_eq_false, false_and]
| inr hnmem =>
  simp only [hnmem, decide_False, not_false_eq_true, true_and,
             decide_not]
  cases Decidable.em (x_1 ∈ [x]) with
  | inl hmem' => simp only [hmem', decide_True, decide_False, not]
  | inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
State after:
no goals

State before:
case h.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hmem : x_1 ∈ acc
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [hmem, decide_True, not_true_eq_false, false_and]
State after:
no goals

State before:
case h.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ acc) = false ∧ decide (x_1 ∈ [x]) = false) = decide (¬x_1 ∈ acc ∧ ¬x_1 ∈ [x])
Tactic:
simp only [hnmem, decide_False, not_false_eq_true, true_and,
           decide_not]
State after:
case h.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])

State before:
case h.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hnmem : ¬x_1 ∈ acc
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
cases Decidable.em (x_1 ∈ [x]) with
| inl hmem' => simp only [hmem', decide_True, decide_False, not]
| inr hnmem' => simp only [hnmem', decide_True, decide_False, not]
State after:
no goals

State before:
case h.inr.inl
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hnmem : ¬x_1 ∈ acc
hmem' : x_1 ∈ [x]
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
simp only [hmem', decide_True, decide_False, not]
State after:
no goals

State before:
case h.inr.inr
α : Type u_1
inst✝ : DecidableEq α
x : α
xs acc : List α
hterm : length (filter (fun a => decide ¬a ∈ acc) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
ih₁ : uniqueAux xs acc = reverse acc ++ unique (filter (fun x => decide ¬x ∈ acc) xs)
ih₂ : uniqueAux xs (x :: acc) = reverse (x :: acc) ++ unique (filter (fun x_2 => decide ¬x_2 ∈ x :: acc) xs)
ih₃ :
  uniqueAux (filter (fun a => decide ¬a ∈ acc) xs) [x] =
    reverse [x] ++ unique (filter (fun x_2 => decide ¬x_2 ∈ [x]) (filter (fun a => decide ¬a ∈ acc) xs))
hout : ¬x ∈ acc
x_1 : α
hnmem : ¬x_1 ∈ acc
hnmem' : ¬x_1 ∈ [x]
⊢ decide (decide (x_1 ∈ [x]) = false) = !decide (x_1 ∈ [x])
Tactic:
simp only [hnmem', decide_True, decide_False, not]
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
_x✝ : (_ : List α) ×' List α
a✝¹ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y _x✝ →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x✝² x✝¹ : List α
a✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x✝², snd := x✝¹ } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
x : α
xs ys : List α
x✝ :
  ∀ (y : (_ : List α) ×' List α),
    (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 y
        { fst := x :: xs, snd := ys } →
      uniqueAux y.1 y.2 = reverse y.2 ++ unique (filter (fun x => decide ¬x ∈ y.2) y.1)
hterm : length (filter (fun a => decide ¬a ∈ ys) xs) < Nat.succ (length xs)
hterm' : length xs < Nat.succ (length xs)
⊢ (invImage (fun a => PSigma.casesOn a fun xs snd => length xs) instWellFoundedRelation).1 { fst := xs, snd := ys }
    { fst := x :: xs, snd := ys }
Tactic:
assumption
State after:
no goals