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

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

Tactic:
simp only [alterKey, Bool.coe_iff_coe]

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

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

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

Result:
no goals

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

Tactic:
cases f (getValueCast? a (x :: xs))

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

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

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

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

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

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

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

Result:
no goals

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

Tactic:
cases f none <;> simp

Result:
no goals