-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_modifyKey [EquivBEq α] (k k': α) (f : β → β) (l : List ((_ : α) × β)) :
    containsKey k' (modifyKey k f l) = containsKey k' l

Proof state:
case cons.h_2
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option β
v✝ : β
heq✝ : getValue? k (head✝ :: tail✝) = some v✝
⊢ containsKey k' (replaceEntry k (f v✝) (head✝ :: tail✝)) = containsKey k' (head✝ :: tail✝)

Tactic:
rw [containsKey_replaceEntry]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
⊢ containsKey k' (modifyKey k f []) = containsKey k' []

Tactic:
simp only [modifyKey, getValue?_nil, eraseKey_nil, containsKey_nil, Bool.false_eq_true]

Result:
no goals

Proof state:
case cons.h_1
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option β
heq✝ : getValue? k (head✝ :: tail✝) = none
⊢ containsKey k' (head✝ :: tail✝) = containsKey k' (head✝ :: tail✝)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
⊢ containsKey k' (modifyKey k f l) = containsKey k' l

Tactic:
induction l

Result:
case nil
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
⊢ containsKey k' (modifyKey k f []) = containsKey k' []

case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k' (modifyKey k f (head✝ :: tail✝)) = containsKey k' (head✝ :: tail✝)

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k'
      (match getValue? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)) =
    containsKey k' (head✝ :: tail✝)

Tactic:
split

Result:
case cons.h_1
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option β
heq✝ : getValue? k (head✝ :: tail✝) = none
⊢ containsKey k' (head✝ :: tail✝) = containsKey k' (head✝ :: tail✝)

case cons.h_2
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option β
v✝ : β
heq✝ : getValue? k (head✝ :: tail✝) = some v✝
⊢ containsKey k' (replaceEntry k (f v✝) (head✝ :: tail✝)) = containsKey k' (head✝ :: tail✝)

Proof state:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k' (modifyKey k f (head✝ :: tail✝)) = containsKey k' (head✝ :: tail✝)

Tactic:
simp only [modifyKey, Bool.coe_iff_coe]

Result:
case cons
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
head✝ : (_ : α) × β
tail✝ : List ((_ : α) × β)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k'
      (match getValue? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)) =
    containsKey k' (head✝ :: tail✝)