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

Proof state:
case cons.h_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option (β k)
heq✝ : getValueCast? 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✝ : LawfulBEq α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
⊢ containsKey k' (modifyKey k f l) = containsKey k' l

Tactic:
induction l

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

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
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 nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
⊢ containsKey k' (modifyKey k f []) = containsKey k' []

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

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k'
      (match getValueCast? 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✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option (β k)
heq✝ : getValueCast? k (head✝ :: tail✝) = none
⊢ containsKey k' (head✝ :: tail✝) = containsKey k' (head✝ :: tail✝)

case cons.h_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
x✝ : Option (β k)
v✝ : β k
heq✝ : getValueCast? 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✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
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✝ : LawfulBEq α
k k' : α
f : β k → β k
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ : containsKey k' (modifyKey k f tail✝) = containsKey k' tail✝
⊢ containsKey k'
      (match getValueCast? k (head✝ :: tail✝) with
      | none => head✝ :: tail✝
      | some v => replaceEntry k (f v) (head✝ :: tail✝)) =
    containsKey k' (head✝ :: tail✝)

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

Tactic:
rw [containsKey_replaceEntry]

Result:
no goals