internlm/Lean-Github huggingface dataset:
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)
Theorem: List.uniqueAux_acc_append_filter
Proof 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₁]
Proof state after:
no goals
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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]
Theorem: List.uniqueAux_acc_append_filter
Proof 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₂]
Proof 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]
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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]
Theorem: List.uniqueAux_acc_append_filter
Proof 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
Proof 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]
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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]
Theorem: List.uniqueAux_acc_append_filter
Proof 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₃]
Proof 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))
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)
Theorem: List.uniqueAux_acc_append_filter
Proof 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]
Proof 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)