-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} :
    (m.alter k f).getKey! k' =
      if k == k' then
        if (f (m.get? k)).isSome then k else default
      else
        m.getKey! k'

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
heq : ¬(k == k') = true
⊢ (m.getKey? k').get! = (m.getKey? k').get!

Tactic:
rfl

Result:
no goals

Proof state:
case isTrue
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h✝ : (k == k') = true
⊢ (if (f (m.get? k)).isSome = true then some k else none).get! = if (f (m.get? k)).isSome = true then k else default

Tactic:
next heq =>
cases eq_of_beq heq
split <;> rfl

Result:
no goals

Proof state:
case refl
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
heq : (k == k) = true
⊢ (if (f (m.get? k)).isSome = true then some k else none).get! = if (f (m.get? k)).isSome = true then k else default

Tactic:
split <;> rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
heq : (k == k') = true
⊢ (if (f (m.get? k)).isSome = true then some k else none).get! = if (f (m.get? k)).isSome = true then k else default

Tactic:
cases eq_of_beq heq

Result:
case refl
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k : α
f : Option (β k) → Option (β k)
heq : (k == k) = true
⊢ (if (f (m.get? k)).isSome = true then some k else none).get! = if (f (m.get? k)).isSome = true then k else default

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
⊢ (m.alter k f).getKey! k' =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else m.getKey! k'

Tactic:
simp [getKey!_eq_get!_getKey?, getKey?_alter]

Result:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
⊢ (if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k').get! =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else (m.getKey? k').get!

Proof state:
case isFalse
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h✝ : ¬(k == k') = true
⊢ (m.getKey? k').get! = (m.getKey? k').get!

Tactic:
next heq =>
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
⊢ (if (k == k') = true then if (f (m.get? k)).isSome = true then some k else none else m.getKey? k').get! =
    if (k == k') = true then if (f (m.get? k)).isSome = true then k else default else (m.getKey? k').get!

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h✝ : (k == k') = true
⊢ (if (f (m.get? k)).isSome = true then some k else none).get! = if (f (m.get? k)).isSome = true then k else default

case isFalse
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h✝ : ¬(k == k') = true
⊢ (m.getKey? k').get! = (m.getKey? k').get!