internlm/Lean-Github huggingface dataset:
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
. intros hneq
  simp only [hneq]
  rw [ite_false]
  simp only [Prod.fst]
  apply Nat.succ_le_succ
  exact ih
Proof state after:
no goals
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
intros heq
Proof state after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Tactic:
simp only [heq]
Proof state after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (if True then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (k, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length
      (if True then (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd)
        else ((matchKey xs k).fst, (k, x.snd) :: (matchKey xs k).snd)).snd ≤
    length (x :: xs)
Tactic:
rw [ite_true]
Proof state after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd).snd ≤ length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (x.snd :: (matchKey xs k).fst, (matchKey xs k).snd).snd ≤ length (x :: xs)
Tactic:
simp only [Prod.snd]
Proof state after:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length (x :: xs)
Tactic:
apply Nat.le_step
Proof state after:
case cons.h1.h
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h1.h
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
heq : x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
⊢ ¬x.fst = k →
    length
        (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 ≤
      length (x :: xs)
Tactic:
intros hneq
Proof state after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (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 ≤
    length (x :: xs)
Tactic:
simp only [hneq]
Proof state after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (if False 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 ≤
    length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length
      (if False 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 ≤
    length (x :: xs)
Tactic:
rw [ite_false]
Proof state after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd).snd ≤ length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((matchKey xs k).fst, (x.fst, x.snd) :: (matchKey xs k).snd).snd ≤ length (x :: xs)
Tactic:
simp only [Prod.fst]
Proof state after:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((x.fst, x.snd) :: (matchKey xs k).snd) ≤ length (x :: xs)
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length ((x.fst, x.snd) :: (matchKey xs k).snd) ≤ length (x :: xs)
Tactic:
apply Nat.succ_le_succ
Proof state after:
case cons.h2.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Theorem: List.matchKey_snd_length
Proof state before:
case cons.h2.a
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).snd ≤ length xs
hneq : ¬x.fst = k
⊢ length (matchKey xs k).snd ≤ length xs
Tactic:
exact ih
Proof state after:
no goals
Theorem: List.matchKey_lengths_sum
Proof state before:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
⊢ ∀ (xs : List (κ × ν)) (k : κ), length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
Tactic:
intros xs k
Proof state after:
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
xs : List (κ × ν)
k : κ
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
Theorem: List.matchKey_lengths_sum
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
⊢ length (matchKey [] k).fst + length (matchKey [] k).snd = length []
Tactic:
rfl
Proof state after:
no goals
Theorem: List.matchKey_lengths_sum
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
⊢ length (matchKey (x :: xs) k).fst + length (matchKey (x :: xs) k).snd = length (x :: xs)
Tactic:
simp only [matchKey]
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
⊢ length
        (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)).fst +
      length
        (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 =
    length (x :: xs)
Theorem: List.matchKey_lengths_sum
Proof state before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length
        (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)).fst +
      length
        (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 =
    length (x :: xs)
Tactic:
simp only [hfalse, ite_false, List.length]
Proof state after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + (length (matchKey xs k).snd + 1) = length xs + 1
Theorem: List.matchKey_lengths_sum
Proof state before:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + (length (matchKey xs k).snd + 1) = length xs + 1
Tactic:
rw [←Nat.add_assoc]
Proof state after:
case cons.isFalse
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
hfalse : ¬x.fst = k
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd + 1 = length xs + 1
Theorem: List.matchKey_lengths_sum
Proof state before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length
        (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)).fst +
      length
        (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 =
    length (x :: xs)
Tactic:
simp only [htrue, ite_true, List.length]
Proof state after:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + 1 + length (matchKey xs k).snd = length xs + 1
Theorem: List.matchKey_lengths_sum
Proof state before:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + 1 + length (matchKey xs k).snd = length xs + 1
Tactic:
rw [Nat.add_assoc, Nat.add_comm 1, ←Nat.add_assoc]
Proof state after:
case cons.isTrue
κ : Type u_1
ν : Type u_2
inst : DecidableEq κ
k : κ
x : κ × ν
xs : List (κ × ν)
ih : length (matchKey xs k).fst + length (matchKey xs k).snd = length xs
htrue : x.fst = k
⊢ length (matchKey xs k).fst + length (matchKey xs k).snd + 1 = length xs + 1
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
⊢ ¬k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
intro hneg
Proof state after:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kvs : List (κ × ν)
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ False
Tactic:
induction kvs with
| nil => cases hneg
| cons kv kvs ih =>
  apply ih
  simp only [matchKey] at hneg
  cases Decidable.em (kv.fst = k) with
  | inl heq =>
    simp only [heq, ite_true] at hneg
    assumption
  | inr hneq =>
    simp only [hneq, ite_false] at hneg
    simp only [map] at hneg
    cases hneg with
    | head => exact absurd rfl hneq
    | tail _ h => exact h
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case nil
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
hneg : k ∈ map Prod.fst (matchKey [] k).snd
⊢ False
Tactic:
cases hneg
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ False
Tactic:
apply ih
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg : k ∈ map Prod.fst (matchKey (kv :: kvs) k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [matchKey] at hneg
Proof state after:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
cases Decidable.em (kv.fst = k) with
| inl heq =>
  simp only [heq, ite_true] at hneg
  assumption
| inr hneq =>
  simp only [hneq, ite_false] at hneg
  simp only [map] at hneg
  cases hneg with
  | head => exact absurd rfl hneq
  | tail _ h => exact h
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
heq : kv.fst = k
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [heq, ite_true] at hneg
Proof state after:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
heq : kv.fst = k
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inl
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
heq : kv.fst = k
hneg : k ∈ map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
assumption
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneg :
  k ∈
    map Prod.fst
      (if kv.fst = k 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
hneq : ¬kv.fst = k
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [hneq, ite_false] at hneg
Proof state after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ map Prod.fst ((kv.fst, kv.snd) :: (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ map Prod.fst ((kv.fst, kv.snd) :: (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
simp only [map] at hneg
Proof state after:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ kv.fst :: map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inr
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
hneg : k ∈ kv.fst :: map Prod.fst (matchKey kvs k).snd
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
cases hneg with
| head => exact absurd rfl hneq
| tail _ h => exact h
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inr.head
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
kv : κ × ν
kvs : List (κ × ν)
ih : kv.fst ∈ map Prod.fst (matchKey kvs kv.fst).snd → False
hneq : ¬kv.fst = kv.fst
⊢ kv.fst ∈ map Prod.fst (matchKey kvs kv.fst).snd
Tactic:
exact absurd rfl hneq
Proof state after:
no goals
Theorem: List.not_mem_matchKey_self_map_snd
Proof state before:
case cons.inr.tail
κ : Type u_1
ν : Type u_2
inst✝ : DecidableEq κ
k : κ
kv : κ × ν
kvs : List (κ × ν)
ih : k ∈ map Prod.fst (matchKey kvs k).snd → False
hneq : ¬kv.fst = k
h : Mem k (map Prod.fst (matchKey kvs k).snd)
⊢ k ∈ map Prod.fst (matchKey kvs k).snd
Tactic:
exact h
Proof state after:
no goals
Theorem: List.fst_mem_of_pair_mem
Proof state before:
α : Type u_1
β : Type u_2
x : α
y : β
hxy : (x, y) ∈ []
⊢ x ∈ map Prod.fst []
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverse xs
Tactic:
rw [reverse_eq_reverseSpec]
Proof state after:
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverseSpec xs
Theorem: List.mem_reverse_iff
Proof state before:
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs ↔ x ∈ reverseSpec xs
Tactic:
apply Iff.intro
Proof state after:
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs

case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Theorem: List.mem_reverse_iff
Proof state before:
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs

case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
. intro hf
  induction hf with
  | head xs =>
    simp only [reverseSpec]
    apply mem_append_singleton
  | @tail y ys h_x_ys ih =>
    simp only [reverseSpec]
    apply mem_append_front _ _ _ ih
Proof state after:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Theorem: List.mem_reverse_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
. intro hb
  induction xs with
  | nil => contradiction
  | cons y ys ih =>
    simp only [reverseSpec] at hb
    rw [List.mem_append_comm] at hb
    simp only [HAppend.hAppend, Append.append, List.append] at hb
    cases hb with
    | head => exact Mem.head _
    | tail _ htail => exact Mem.tail _ (ih htail)
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mp
α : Type u_1
x : α
xs : List α
⊢ x ∈ xs → x ∈ reverseSpec xs
Tactic:
intro hf
Proof state after:
case mp
α : Type u_1
x : α
xs : List α
hf : x ∈ xs
⊢ x ∈ reverseSpec xs
Theorem: List.mem_reverse_iff
Proof state before:
case mp
α : Type u_1
x : α
xs : List α
hf : x ∈ xs
⊢ x ∈ reverseSpec xs
Tactic:
induction hf with
| head xs =>
  simp only [reverseSpec]
  apply mem_append_singleton
| @tail y ys h_x_ys ih =>
  simp only [reverseSpec]
  apply mem_append_front _ _ _ ih
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec (x :: xs)
Tactic:
simp only [reverseSpec]
Proof state after:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec xs ++ [x]
Theorem: List.mem_reverse_iff
Proof state before:
case mp.head
α : Type u_1
x : α
xs✝ xs : List α
⊢ x ∈ reverseSpec xs ++ [x]
Tactic:
apply mem_append_singleton
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec (y :: ys)
Tactic:
simp only [reverseSpec]
Proof state after:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec ys ++ [y]
Theorem: List.mem_reverse_iff
Proof state before:
case mp.tail
α : Type u_1
x : α
xs : List α
y : α
ys : List α
h_x_ys : Mem x ys
ih : x ∈ reverseSpec ys
⊢ x ∈ reverseSpec ys ++ [y]
Tactic:
apply mem_append_front _ _ _ ih
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs : List α
⊢ x ∈ reverseSpec xs → x ∈ xs
Tactic:
intro hb
Proof state after:
case mpr
α : Type u_1
x : α
xs : List α
hb : x ∈ reverseSpec xs
⊢ x ∈ xs
Theorem: List.mem_reverse_iff
Proof state before:
case mpr
α : Type u_1
x : α
xs : List α
hb : x ∈ reverseSpec xs
⊢ x ∈ xs
Tactic:
induction xs with
| nil => contradiction
| cons y ys ih =>
  simp only [reverseSpec] at hb
  rw [List.mem_append_comm] at hb
  simp only [HAppend.hAppend, Append.append, List.append] at hb
  cases hb with
  | head => exact Mem.head _
  | tail _ htail => exact Mem.tail _ (ih htail)
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.nil
α : Type u_1
x : α
hb : x ∈ reverseSpec []
⊢ x ∈ []
Tactic:
contradiction
Proof state after:
no goals
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec (y :: ys)
⊢ x ∈ y :: ys
Tactic:
simp only [reverseSpec] at hb
Proof state after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec ys ++ [y]
⊢ x ∈ y :: ys
Theorem: List.mem_reverse_iff
Proof state before:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ reverseSpec ys ++ [y]
⊢ x ∈ y :: ys
Tactic:
rw [List.mem_append_comm] at hb
Proof state after:
case mpr.cons
α : Type u_1
x y : α
ys : List α
ih : x ∈ reverseSpec ys → x ∈ ys
hb : x ∈ [y] ++ reverseSpec ys
⊢ x ∈ y :: ys