-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertList_of_contains_eq_false [BEq α] [PartialEquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (not_contains : containsKey k toInsert = false) :
    getEntry? k (insertList l toInsert) = getEntry? k l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : containsKey k toInsert = false
⊢ getEntry? k (insertList l toInsert) = getEntry? k l

Tactic:
induction toInsert generalizing l with
| nil => simp [insertList]
| cons h t ih =>
  unfold insertList
  rw [containsKey_cons_eq_false] at not_contains
  rw [ih not_contains.right, getEntry?_insertEntry]
  simp [not_contains]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : containsKey k (h :: t) = false
⊢ getEntry? k (insertList (insertEntry h.fst h.snd l) t) = getEntry? k l

Tactic:
rw [containsKey_cons_eq_false] at not_contains

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : (h.fst == k) = false ∧ containsKey k t = false
⊢ getEntry? k (insertList (insertEntry h.fst h.snd l) t) = getEntry? k l

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : (h.fst == k) = false ∧ containsKey k t = false
⊢ (if (h.fst == k) = true then some ⟨h.fst, h.snd⟩ else getEntry? k l) = getEntry? k l

Tactic:
simp [not_contains]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
l : List ((a : α) × β a)
not_contains : containsKey k [] = false
⊢ getEntry? k (insertList l []) = getEntry? k l

Tactic:
simp [insertList]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : (h.fst == k) = false ∧ containsKey k t = false
⊢ getEntry? k (insertList (insertEntry h.fst h.snd l) t) = getEntry? k l

Tactic:
rw [ih not_contains.right, getEntry?_insertEntry]

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : (h.fst == k) = false ∧ containsKey k t = false
⊢ (if (h.fst == k) = true then some ⟨h.fst, h.snd⟩ else getEntry? k l) = getEntry? k l

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : containsKey k (h :: t) = false
⊢ getEntry? k (insertList l (h :: t)) = getEntry? k l

Tactic:
unfold insertList

Result:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
h : (a : α) × β a
t : List ((a : α) × β a)
ih : ∀ {l : List ((a : α) × β a)}, containsKey k t = false → getEntry? k (insertList l t) = getEntry? k l
l : List ((a : α) × β a)
not_contains : containsKey k (h :: t) = false
⊢ getEntry? k (insertList (insertEntry h.fst h.snd l) t) = getEntry? k l