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

State before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
as xs cs : List α
⊢ length (uniqueAux xs (cs ++ x :: (as ++ [y]))) = length (uniqueAux xs (cs ++ y :: x :: as))
Tactic:
induction xs generalizing cs with
| nil =>
  simp [uniqueAux]
  rw [←Nat.add_one,
      Nat.add_assoc,
      Nat.add_comm (length cs),
      ←Nat.add_assoc]
| cons z zs ih =>
  have rearrange_mem :
    (z ∈ cs ++ x :: (as ++ [y])) ↔ (z ∈ cs ++ y :: x :: as) := by
    apply Iff.intro
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        rw [←cons_append] at hcons
        cases mem_append_iff.mpr hcons with
        | inl hxas => exact List.Mem.tail _ hxas
        | inr hy =>
          cases hy with
          | tail _ _ => contradiction
          | head _ => exact List.Mem.head _
    . intros h
      cases mem_append_iff.mpr h with
      | inl hcs => exact List.mem_append_front _ _ _ hcs
      | inr hcons =>
        apply List.mem_append_back
        cases hcons with
        | head _ =>
          apply List.Mem.tail
          apply List.mem_append_back
          apply (List.mem_singleton_iff y y).mpr rfl
        | tail _ hcons' =>
          rw [←cons_append]
          exact List.mem_append_front _ _ _ hcons'
  simp only [uniqueAux]
  cases Decidable.em (z ∈ cs ++ x :: (as ++ [y])) with
  | inl hin =>
    simp only [hin, rearrange_mem.mp hin, ite_true]
    apply ih
  | inr hout =>
    simp only [hout, rearrange_mem.not_iff_not_of_iff.mp hout, ite_false]
    have rw_help (stuff) : (z :: (cs ++ stuff)) = ((z :: cs) ++ stuff) := rfl
    rw [rw_help, rw_help]
    apply ih
State after:
no goals

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ length (uniqueAux [] (cs ++ x :: (as ++ [y]))) = length (uniqueAux [] (cs ++ y :: x :: as))
Tactic:
simp [uniqueAux]
State after:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ Nat.succ (length as + Nat.succ 0 + length cs) = length as + Nat.succ 0 + Nat.succ 0 + length cs

State before:
case nil
α : Type u_1
inst✝ : DecidableEq α
x y : α
as cs : List α
⊢ Nat.succ (length as + Nat.succ 0 + length cs) = length as + Nat.succ 0 + Nat.succ 0 + length cs
Tactic:
rw [←Nat.add_one,
    Nat.add_assoc,
    Nat.add_comm (length cs),
    ←Nat.add_assoc]
State after:
no goals

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ length (uniqueAux (z :: zs) (cs ++ x :: (as ++ [y]))) = length (uniqueAux (z :: zs) (cs ++ y :: x :: as))
Tactic:
have rearrange_mem :
  (z ∈ cs ++ x :: (as ++ [y])) ↔ (z ∈ cs ++ y :: x :: as) := by
  apply Iff.intro
  . intros h
    cases mem_append_iff.mpr h with
    | inl hcs => exact List.mem_append_front _ _ _ hcs
    | inr hcons =>
      apply List.mem_append_back
      rw [←cons_append] at hcons
      cases mem_append_iff.mpr hcons with
      | inl hxas => exact List.Mem.tail _ hxas
      | inr hy =>
        cases hy with
        | tail _ _ => contradiction
        | head _ => exact List.Mem.head _
  . intros h
    cases mem_append_iff.mpr h with
    | inl hcs => exact List.mem_append_front _ _ _ hcs
    | inr hcons =>
      apply List.mem_append_back
      cases hcons with
      | head _ =>
        apply List.Mem.tail
        apply List.mem_append_back
        apply (List.mem_singleton_iff y y).mpr rfl
      | tail _ hcons' =>
        rw [←cons_append]
        exact List.mem_append_front _ _ _ hcons'
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length (uniqueAux (z :: zs) (cs ++ x :: (as ++ [y]))) = length (uniqueAux (z :: zs) (cs ++ y :: x :: as))

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length (uniqueAux (z :: zs) (cs ++ x :: (as ++ [y]))) = length (uniqueAux (z :: zs) (cs ++ y :: x :: as))
Tactic:
simp only [uniqueAux]
State after:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length
      (if z ∈ cs ++ x :: (as ++ [y]) then uniqueAux zs (cs ++ x :: (as ++ [y]))
      else uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) =
    length
      (if z ∈ cs ++ y :: x :: as then uniqueAux zs (cs ++ y :: x :: as) else uniqueAux zs (z :: (cs ++ y :: x :: as)))

State before:
case cons
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
⊢ length
      (if z ∈ cs ++ x :: (as ++ [y]) then uniqueAux zs (cs ++ x :: (as ++ [y]))
      else uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) =
    length
      (if z ∈ cs ++ y :: x :: as then uniqueAux zs (cs ++ y :: x :: as) else uniqueAux zs (z :: (cs ++ y :: x :: as)))
Tactic:
cases Decidable.em (z ∈ cs ++ x :: (as ++ [y])) with
| inl hin =>
  simp only [hin, rearrange_mem.mp hin, ite_true]
  apply ih
| inr hout =>
  simp only [hout, rearrange_mem.not_iff_not_of_iff.mp hout, ite_false]
  have rw_help (stuff) : (z :: (cs ++ stuff)) = ((z :: cs) ++ stuff) := rfl
  rw [rw_help, rw_help]
  apply ih
State after:
no goals

State before:
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
Tactic:
apply Iff.intro
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ x :: (as ++ [y]) → z ∈ cs ++ y :: x :: as

case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ x :: (as ++ [y]) → z ∈ cs ++ y :: x :: as

case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])
Tactic:
. intros h
  cases mem_append_iff.mpr h with
  | inl hcs => exact List.mem_append_front _ _ _ hcs
  | inr hcons =>
    apply List.mem_append_back
    rw [←cons_append] at hcons
    cases mem_append_iff.mpr hcons with
    | inl hxas => exact List.Mem.tail _ hxas
    | inr hy =>
      cases hy with
      | tail _ _ => contradiction
      | head _ => exact List.Mem.head _
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])
Tactic:
. intros h
  cases mem_append_iff.mpr h with
  | inl hcs => exact List.mem_append_front _ _ _ hcs
  | inr hcons =>
    apply List.mem_append_back
    cases hcons with
    | head _ =>
      apply List.Mem.tail
      apply List.mem_append_back
      apply (List.mem_singleton_iff y y).mpr rfl
    | tail _ hcons' =>
      rw [←cons_append]
      exact List.mem_append_front _ _ _ hcons'
State after:
no goals

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ x :: (as ++ [y]) → z ∈ cs ++ y :: x :: as
Tactic:
intros h
State after:
case mp
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
⊢ z ∈ cs ++ y :: x :: as

State before:
case mp
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
⊢ z ∈ cs ++ y :: x :: as
Tactic:
cases mem_append_iff.mpr h with
| inl hcs => exact List.mem_append_front _ _ _ hcs
| inr hcons =>
  apply List.mem_append_back
  rw [←cons_append] at hcons
  cases mem_append_iff.mpr hcons with
  | inl hxas => exact List.Mem.tail _ hxas
  | inr hy =>
    cases hy with
    | tail _ _ => contradiction
    | head _ => exact List.Mem.head _
State after:
no goals

State before:
case mp.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcs : z ∈ cs
⊢ z ∈ cs ++ y :: x :: as
Tactic:
exact List.mem_append_front _ _ _ hcs
State after:
no goals

State before:
case mp.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: (as ++ [y])
⊢ z ∈ cs ++ y :: x :: as
Tactic:
apply List.mem_append_back
State after:
case mp.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: (as ++ [y])
⊢ z ∈ y :: x :: as

State before:
case mp.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: (as ++ [y])
⊢ z ∈ y :: x :: as
Tactic:
rw [←cons_append] at hcons
State after:
case mp.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
⊢ z ∈ y :: x :: as

State before:
case mp.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
⊢ z ∈ y :: x :: as
Tactic:
cases mem_append_iff.mpr hcons with
| inl hxas => exact List.Mem.tail _ hxas
| inr hy =>
  cases hy with
  | tail _ _ => contradiction
  | head _ => exact List.Mem.head _
State after:
no goals

State before:
case mp.inr.a.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
hxas : z ∈ x :: as
⊢ z ∈ y :: x :: as
Tactic:
exact List.Mem.tail _ hxas
State after:
no goals

State before:
case mp.inr.a.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
hy : z ∈ [y]
⊢ z ∈ y :: x :: as
Tactic:
cases hy with
| tail _ _ => contradiction
| head _ => exact List.Mem.head _
State after:
no goals

State before:
case mp.inr.a.inr.tail
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ x :: (as ++ [y])
hcons : z ∈ x :: as ++ [y]
a✝ : Mem z []
⊢ z ∈ y :: x :: as
Tactic:
contradiction
State after:
no goals

State before:
case mp.inr.a.inr.head
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ x :: (as ++ [y])
hcons : y ∈ x :: as ++ [y]
⊢ y ∈ y :: x :: as
Tactic:
exact List.Mem.head _
State after:
no goals

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
⊢ z ∈ cs ++ y :: x :: as → z ∈ cs ++ x :: (as ++ [y])
Tactic:
intros h
State after:
case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
⊢ z ∈ cs ++ x :: (as ++ [y])

State before:
case mpr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
⊢ z ∈ cs ++ x :: (as ++ [y])
Tactic:
cases mem_append_iff.mpr h with
| inl hcs => exact List.mem_append_front _ _ _ hcs
| inr hcons =>
  apply List.mem_append_back
  cases hcons with
  | head _ =>
    apply List.Mem.tail
    apply List.mem_append_back
    apply (List.mem_singleton_iff y y).mpr rfl
  | tail _ hcons' =>
    rw [←cons_append]
    exact List.mem_append_front _ _ _ hcons'
State after:
no goals

State before:
case mpr.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcs : z ∈ cs
⊢ z ∈ cs ++ x :: (as ++ [y])
Tactic:
exact List.mem_append_front _ _ _ hcs
State after:
no goals

State before:
case mpr.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons : z ∈ y :: x :: as
⊢ z ∈ cs ++ x :: (as ++ [y])
Tactic:
apply List.mem_append_back
State after:
case mpr.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons : z ∈ y :: x :: as
⊢ z ∈ x :: (as ++ [y])

State before:
case mpr.inr.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons : z ∈ y :: x :: as
⊢ z ∈ x :: (as ++ [y])
Tactic:
cases hcons with
| head _ =>
  apply List.Mem.tail
  apply List.mem_append_back
  apply (List.mem_singleton_iff y y).mpr rfl
| tail _ hcons' =>
  rw [←cons_append]
  exact List.mem_append_front _ _ _ hcons'
State after:
no goals

State before:
case mpr.inr.a.head
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ y :: x :: as
⊢ y ∈ x :: (as ++ [y])
Tactic:
apply List.Mem.tail
State after:
case mpr.inr.a.head.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ y :: x :: as
⊢ Mem y (as ++ [y])

State before:
case mpr.inr.a.head.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ y :: x :: as
⊢ Mem y (as ++ [y])
Tactic:
apply List.mem_append_back
State after:
case mpr.inr.a.head.a.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ y :: x :: as
⊢ y ∈ [y]

State before:
case mpr.inr.a.head.a.a
α : Type u_1
inst✝ : DecidableEq α
x y : α
as zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : y ∈ cs ++ y :: x :: as
⊢ y ∈ [y]
Tactic:
apply (List.mem_singleton_iff y y).mpr rfl
State after:
no goals

State before:
case mpr.inr.a.tail
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons' : Mem z (x :: as)
⊢ z ∈ x :: (as ++ [y])
Tactic:
rw [←cons_append]
State after:
case mpr.inr.a.tail
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons' : Mem z (x :: as)
⊢ z ∈ x :: as ++ [y]

State before:
case mpr.inr.a.tail
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
h : z ∈ cs ++ y :: x :: as
hcons' : Mem z (x :: as)
⊢ z ∈ x :: as ++ [y]
Tactic:
exact List.mem_append_front _ _ _ hcons'
State after:
no goals

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hin : z ∈ cs ++ x :: (as ++ [y])
⊢ length
      (if z ∈ cs ++ x :: (as ++ [y]) then uniqueAux zs (cs ++ x :: (as ++ [y]))
      else uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) =
    length
      (if z ∈ cs ++ y :: x :: as then uniqueAux zs (cs ++ y :: x :: as) else uniqueAux zs (z :: (cs ++ y :: x :: as)))
Tactic:
simp only [hin, rearrange_mem.mp hin, ite_true]
State after:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hin : z ∈ cs ++ x :: (as ++ [y])
⊢ length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))

State before:
case cons.inl
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hin : z ∈ cs ++ x :: (as ++ [y])
⊢ length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
Tactic:
apply ih
State after:
no goals

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
⊢ length
      (if z ∈ cs ++ x :: (as ++ [y]) then uniqueAux zs (cs ++ x :: (as ++ [y]))
      else uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) =
    length
      (if z ∈ cs ++ y :: x :: as then uniqueAux zs (cs ++ y :: x :: as) else uniqueAux zs (z :: (cs ++ y :: x :: as)))
Tactic:
simp only [hout, rearrange_mem.not_iff_not_of_iff.mp hout, ite_false]
State after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
⊢ length (uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) = length (uniqueAux zs (z :: (cs ++ y :: x :: as)))

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
⊢ length (uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) = length (uniqueAux zs (z :: (cs ++ y :: x :: as)))
Tactic:
have rw_help (stuff) : (z :: (cs ++ stuff)) = ((z :: cs) ++ stuff) := rfl
State after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
rw_help : ∀ (stuff : List α), z :: (cs ++ stuff) = z :: cs ++ stuff
⊢ length (uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) = length (uniqueAux zs (z :: (cs ++ y :: x :: as)))

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
rw_help : ∀ (stuff : List α), z :: (cs ++ stuff) = z :: cs ++ stuff
⊢ length (uniqueAux zs (z :: (cs ++ x :: (as ++ [y])))) = length (uniqueAux zs (z :: (cs ++ y :: x :: as)))
Tactic:
rw [rw_help, rw_help]
State after:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
rw_help : ∀ (stuff : List α), z :: (cs ++ stuff) = z :: cs ++ stuff
⊢ length (uniqueAux zs (z :: cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (z :: cs ++ y :: x :: as))

State before:
case cons.inr
α : Type u_1
inst✝ : DecidableEq α
x y : α
as : List α
z : α
zs : List α
ih : ∀ (cs : List α), length (uniqueAux zs (cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (cs ++ y :: x :: as))
cs : List α
rearrange_mem : z ∈ cs ++ x :: (as ++ [y]) ↔ z ∈ cs ++ y :: x :: as
hout : ¬z ∈ cs ++ x :: (as ++ [y])
rw_help : ∀ (stuff : List α), z :: (cs ++ stuff) = z :: cs ++ stuff
⊢ length (uniqueAux zs (z :: cs ++ x :: (as ++ [y]))) = length (uniqueAux zs (z :: cs ++ y :: x :: as))
Tactic:
apply ih
State after:
no goals