-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β}
    {l : List ((_ : α) × β)} (hl : DistinctKeys l) :
    containsKey k' (alterKey k f l) =
      if k == k' then
        f (getValue? k l) |>.isSome
      else
        containsKey k' l

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ containsKey k' (insertEntry k v✝ l) = containsKey k' l

Tactic:
next heq =>
simp_all only [Bool.not_eq_true, containsKey_insertEntry, Bool.false_or]

Result:
no goals

Proof state:
case isTrue
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : (k == k') = true
⊢ containsKey k' (alterKey k f l) = (f (getValue? k l)).isSome

Tactic:
next h =>
rw [← containsKey_congr h]
exact containsKey_alterKey_self hl

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
⊢ containsKey k' (alterKey k f l) = containsKey k' l

Tactic:
rw [alterKey]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
⊢ containsKey k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    containsKey k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : (k == k') = true
⊢ containsKey k (alterKey k f l) = (f (getValue? k l)).isSome

Tactic:
exact containsKey_alterKey_self hl

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
⊢ containsKey k'
      (match f (getValue? k l) with
      | none => eraseKey k l
      | some v => insertEntry k v l) =
    containsKey k' l

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ containsKey k' (eraseKey k l) = containsKey k' l

case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
v✝ : β
heq✝ : f (getValue? k l) = some v✝
⊢ containsKey k' (insertEntry k v✝ l) = containsKey k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : (k == k') = true
⊢ containsKey k' (alterKey k f l) = (f (getValue? k l)).isSome

Tactic:
rw [← containsKey_congr h]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : (k == k') = true
⊢ containsKey k (alterKey k f l) = (f (getValue? k l)).isSome

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
heq✝ : f (getValue? k l) = none
⊢ containsKey k' (eraseKey k l) = containsKey k' l

Tactic:
next heq =>
simp only [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ containsKey k' (alterKey k f l) = if (k == k') = true then (f (getValue? k l)).isSome else containsKey k' l

Tactic:
split

Result:
case isTrue
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : (k == k') = true
⊢ containsKey k' (alterKey k f l) = (f (getValue? k l)).isSome

case isFalse
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : ¬(k == k') = true
⊢ containsKey k' (alterKey k f l) = containsKey k' l

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
heq : f (getValue? k l) = none
⊢ containsKey k' (eraseKey k l) = containsKey k' l

Tactic:
simp only [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : ¬(k == k') = true
x✝ : Option β
v✝ : β
heq : f (getValue? k l) = some v✝
⊢ containsKey k' (insertEntry k v✝ l) = containsKey k' l

Tactic:
simp_all only [Bool.not_eq_true, containsKey_insertEntry, Bool.false_or]

Result:
no goals