internlm/Lean-Github huggingface dataset:
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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'
Proof 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))
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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)))
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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])
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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 _
Proof 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])
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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'
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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 _
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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 _
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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 _
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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 _
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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])
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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'
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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])
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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'
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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])
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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]
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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]
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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'
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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))
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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)))
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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
Proof 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)))
Theorem: List.length_uniqueAux_congr_append_cons_acc
Proof 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]
Proof 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))