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

State before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
Tactic:
induction xs with
| nil => intros; simp [uniqueAux]
| cons x xs ih =>
  intros acc hk
  simp only [length, uniqueAux]
  cases Decidable.em (x.fst ∈ acc) with
  | inl hin =>
    simp only [hin, ite_true, matchKey]
    rw [ih _ hk]
    cases Decidable.em (x.1 = k) with
    | inl heq => simp only [heq, ite_true]
    | inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
  | inr hout =>
    simp only [hout, ite_false, matchKey]
    cases Decidable.em (x.1 = k) with
    | inl heq =>
      apply absurd hk
      rw [heq] at hout
      exact hout
    | inr hneq =>
      rw [ih _ (List.Mem.tail _ hk)]
      simp only [hneq, ite_false, uniqueAux, hout]
State after:
no goals

State before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
⊢ ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst []) acc) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc)
Tactic:
intros
State after:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
acc✝ : List κ
hk✝ : k ∈ acc✝
⊢ length (uniqueAux (map Prod.fst []) acc✝) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc✝)

State before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
acc✝ : List κ
hk✝ : k ∈ acc✝
⊢ length (uniqueAux (map Prod.fst []) acc✝) = length (uniqueAux (map Prod.fst (matchKey [] k).snd) acc✝)
Tactic:
simp [uniqueAux]
State after:
no goals

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
⊢ ∀ (acc : List κ),
    k ∈ acc →
      length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
intros acc hk
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (uniqueAux (map Prod.fst (x :: xs)) acc) = length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
simp only [length, uniqueAux]
State after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)

State before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
cases Decidable.em (x.fst ∈ acc) with
| inl hin =>
  simp only [hin, ite_true, matchKey]
  rw [ih _ hk]
  cases Decidable.em (x.1 = k) with
  | inl heq => simp only [heq, ite_true]
  | inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
| inr hout =>
  simp only [hout, ite_false, matchKey]
  cases Decidable.em (x.1 = k) with
  | inl heq =>
    apply absurd hk
    rw [heq] at hout
    exact hout
  | inr hneq =>
    rw [ih _ (List.Mem.tail _ hk)]
    simp only [hneq, ite_false, uniqueAux, hout]
State after:
no goals

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
simp only [hin, ite_true, matchKey]
State after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst xs) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst xs) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
rw [ih _ hk]
State after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)

State before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
cases Decidable.em (x.1 = k) with
| inl heq => simp only [heq, ite_true]
| inr hneq => simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
State after:
no goals

State before:
case cons.inl.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
heq : x.fst = k
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
simp only [heq, ite_true]
State after:
no goals

State before:
case cons.inl.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hin : x.fst ∈ acc
hneq : ¬x.fst = k
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
simp only [hneq, ite_false, map, uniqueAux, hin, ite_true]
State after:
no goals

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
⊢ length (if x.fst ∈ acc then uniqueAux (map Prod.fst xs) acc else uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length (uniqueAux (map Prod.fst (matchKey (x :: xs) k).snd) acc)
Tactic:
simp only [hout, ite_false, matchKey]
State after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)

State before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
⊢ length (uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
cases Decidable.em (x.1 = k) with
| inl heq =>
  apply absurd hk
  rw [heq] at hout
  exact hout
| inr hneq =>
  rw [ih _ (List.Mem.tail _ hk)]
  simp only [hneq, ite_false, uniqueAux, hout]
State after:
no goals

State before:
case cons.inr.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
heq : x.fst = k
⊢ length (uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
apply absurd hk
State after:
case cons.inr.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
heq : x.fst = k
⊢ ¬k ∈ acc

State before:
case cons.inr.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
heq : x.fst = k
⊢ ¬k ∈ acc
Tactic:
rw [heq] at hout
State after:
case cons.inr.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬k ∈ acc
heq : x.fst = k
⊢ ¬k ∈ acc

State before:
case cons.inr.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬k ∈ acc
heq : x.fst = k
⊢ ¬k ∈ acc
Tactic:
exact hout
State after:
no goals

State before:
case cons.inr.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
hneq : ¬x.fst = k
⊢ length (uniqueAux (map Prod.fst xs) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
rw [ih _ (List.Mem.tail _ hk)]
State after:
case cons.inr.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
hneq : ¬x.fst = k
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)

State before:
case cons.inr.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih :
  ∀ (acc : List κ),
    k ∈ acc → length (uniqueAux (map Prod.fst xs) acc) = length (uniqueAux (map Prod.fst (matchKey xs k).snd) acc)
acc : List κ
hk : k ∈ acc
hout : ¬x.fst ∈ acc
hneq : ¬x.fst = k
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) (x.fst :: acc)) =
    length
      (uniqueAux
        (map Prod.fst
          (if x.fst = k then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
            else ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd)).snd)
        acc)
Tactic:
simp only [hneq, ite_false, uniqueAux, hout]
State after:
no goals