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

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

Tactic:
simp only [alterKey, Bool.coe_iff_coe]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
⊢ containsKey a
      (match f (getValue? a (x :: xs)) with
      | none => eraseKey a (x :: xs)
      | some v => insertEntry a v (x :: xs)) =
    (f (getValue? a (x :: xs))).isSome

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys []
⊢ containsKey a
      (match f none with
      | none => []
      | some b => [⟨a, b⟩]) =
    (f none).isSome

Tactic:
split <;> { rename_i heq; simp [heq] }

Result:
no goals

Proof state:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
heq✝ : f (getValue? a (x :: xs)) = none
⊢ containsKey a (eraseKey a (x :: xs)) = (f (getValue? a (x :: xs))).isSome

Tactic:
next heq =>
simp only [hl, heq, Option.isSome_none, containsKey_eraseKey_self]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
heq : f (getValue? a (x :: xs)) = none
⊢ containsKey a (eraseKey a (x :: xs)) = (f (getValue? a (x :: xs))).isSome

Tactic:
simp only [hl, heq, Option.isSome_none, containsKey_eraseKey_self]

Result:
no goals

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a (x :: xs)) = some v✝
⊢ containsKey a (insertEntry a v✝ (x :: xs)) = (f (getValue? a (x :: xs))).isSome

Tactic:
next heq =>
simp only [containsKey_insertEntry, BEq.refl, Bool.true_or, heq, Option.isSome_some]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
⊢ containsKey a
      (match f (getValue? a (x :: xs)) with
      | none => eraseKey a (x :: xs)
      | some v => insertEntry a v (x :: xs)) =
    (f (getValue? a (x :: xs))).isSome

Tactic:
split

Result:
case h_1
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
heq✝ : f (getValue? a (x :: xs)) = none
⊢ containsKey a (eraseKey a (x :: xs)) = (f (getValue? a (x :: xs))).isSome

case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
v✝ : β
heq✝ : f (getValue? a (x :: xs)) = some v✝
⊢ containsKey a (insertEntry a v✝ (x :: xs)) = (f (getValue? a (x :: xs))).isSome

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys []
x✝ : Option β
v✝ : β
heq : f none = some v✝
⊢ containsKey a [⟨a, v✝⟩] = (f none).isSome

Tactic:
simp [heq]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
x : (_ : α) × β
xs : List ((_ : α) × β)
hl : DistinctKeys (x :: xs)
x✝ : Option β
v✝ : β
heq : f (getValue? a (x :: xs)) = some v✝
⊢ containsKey a (insertEntry a v✝ (x :: xs)) = (f (getValue? a (x :: xs))).isSome

Tactic:
simp only [containsKey_insertEntry, BEq.refl, Bool.true_or, heq, Option.isSome_some]

Result:
no goals

Proof state:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys []
x✝ : Option β
v✝ : β
heq✝ : f none = some v✝
⊢ containsKey a [⟨a, v✝⟩] = (f none).isSome

Tactic:
rename_i heq

Result:
case h_2
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys []
x✝ : Option β
v✝ : β
heq : f none = some v✝
⊢ containsKey a [⟨a, v✝⟩] = (f none).isSome

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

Tactic:
simp only [getValue?_nil, Bool.coe_iff_coe, alterKey_nil]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
a : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys []
⊢ containsKey a
      (match f none with
      | none => []
      | some b => [⟨a, b⟩]) =
    (f none).isSome