internlm/Lean-Github huggingface dataset:
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof 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)
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof 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)
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof 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)
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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
Proof 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
Theorem: List.length_uniqueAux_matchKey
Proof 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
Proof 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
Theorem: List.length_uniqueAux_matchKey
Proof 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
Proof state after:
no goals
Theorem: List.length_uniqueAux_matchKey
Proof 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)]
Proof 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)
Theorem: List.length_uniqueAux_matchKey
Proof 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]
Proof state after:
no goals
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
have hterm : length (matchKey xs k).snd < Nat.succ (length xs) :=
  Nat.lt_of_succ_le $ Nat.succ_le_succ $ matchKey_snd_length xs k
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
have ih := length_groupByKey (matchKey xs k).2
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey ((k, v) :: xs)) = length (unique (map Prod.fst ((k, v) :: xs)))
Tactic:
simp only [map, unique, uniqueAux, List.not_mem_nil, ite_false, groupByKey]
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd) = length (uniqueAux (map Prod.fst xs) [k])
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length ((k, v :: (matchKey xs k).fst) :: groupByKey (matchKey xs k).snd) = length (uniqueAux (map Prod.fst xs) [k])
Tactic:
simp only [length]
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey (matchKey xs k).snd) + 1 = length (uniqueAux (map Prod.fst xs) [k])
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey (matchKey xs k).snd) + 1 = length (uniqueAux (map Prod.fst xs) [k])
Tactic:
rw [length_uniqueAux_matchKey _ k _ $ List.Mem.head _]
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey (matchKey xs k).snd) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (groupByKey (matchKey xs k).snd) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])
Tactic:
rw [ih]
Proof state after:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (unique (map Prod.fst (matchKey xs k).snd)) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (unique (map Prod.fst (matchKey xs k).snd)) + 1 = length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k])
Tactic:
apply Eq.symm
Proof state after:
case h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k]) = length (unique (map Prod.fst (matchKey xs k).snd)) + 1
Theorem: List.length_groupByKey
Proof state before:
case h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ length (uniqueAux (map Prod.fst (matchKey xs k).snd) [k]) = length (unique (map Prod.fst (matchKey xs k).snd)) + 1
Tactic:
apply List.length_uniqueAux (acc := [k])
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ ∀ (x : κ), x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
⊢ ∀ (x : κ), x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Tactic:
intro x
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x ∈ [k]
Tactic:
rw [mem_singleton_iff]
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x = k
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
⊢ x ∈ map Prod.fst (matchKey xs k).snd → ¬x = k
Tactic:
intro hmem hneg
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
⊢ False
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
⊢ False
Tactic:
have := not_mem_matchKey_self_map_snd x xs
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs k).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Tactic:
rw [←hneg] at hmem
Proof state after:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs x).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Theorem: List.length_groupByKey
Proof state before:
case h.h
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
k : κ
v : ν
xs : List (κ × ν)
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
ih : length (groupByKey (matchKey xs k).snd) = length (unique (map Prod.fst (matchKey xs k).snd))
x : κ
hmem : x ∈ map Prod.fst (matchKey xs x).snd
hneg : x = k
this : ¬x ∈ map Prod.fst (matchKey xs x).snd
⊢ False
Tactic:
exact this hmem
Proof state after:
no goals
Theorem: List.length_groupByKey
Proof state before:
κ : Type u_1
inst✝ : DecidableEq κ
ν : Type u_2
xs✝ : List (κ × ν)
a✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y xs✝ →
      length (groupByKey y) = length (unique (map Prod.fst y))
k : κ
v : ν
xs : List (κ × ν)
x✝ :
  ∀ (y : List (κ × ν)),
    (invImage (fun a => length a) instWellFoundedRelation).1 y ((k, v) :: xs) →
      length (groupByKey y) = length (unique (map Prod.fst y))
hterm : length (matchKey xs k).snd < Nat.succ (length xs)
⊢ (invImage (fun a => length a) instWellFoundedRelation).1 (matchKey xs k).snd ((k, v) :: xs)
Tactic:
assumption
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey (kv :: kvs) k).snd <+ kv :: kvs
Tactic:
simp only [matchKey, h, ite_true]
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey kvs k).snd <+ kv :: kvs
Theorem: List.matchKey_snd_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : kv.fst = k
⊢ (matchKey kvs k).snd <+ kv :: kvs
Tactic:
exact Sublist.cons _ _ _ ih
Proof state after:
no goals
Theorem: List.matchKey_snd_sublist
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : ¬kv.fst = k
⊢ (matchKey (kv :: kvs) k).snd <+ kv :: kvs
Tactic:
simp only [matchKey, h, ite_true]
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : (matchKey kvs k).snd <+ kvs
h : ¬kv.fst = k
⊢ (if False then (kv.snd :: (matchKey kvs k).fst, (matchKey kvs k).snd)
      else ((matchKey kvs k).fst, (kv.fst, kv.snd) :: (matchKey kvs k).snd)).snd <+
    kv :: kvs