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

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

Tactic:
split

Result:
case isTrue
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' fallback : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : (k == k') = true
⊢ (if (f (getValue? k l)).isSome = true then some k else none).getD fallback =
    if (f (getValue? k l)).isSome = true then k else fallback

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

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

Tactic:
simp only [hl, getKeyD_eq_getKey?, getKey?_alterKey, beq_iff_eq, Function.comp_apply]

Result:
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' fallback : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ (if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l).getD
      fallback =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then k else fallback else (getKey? k' l).getD fallback

Proof state:
case isFalse
α : Type u
inst✝¹ : BEq α
β : Type v
inst✝ : EquivBEq α
k k' fallback : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
h✝ : ¬(k == k') = true
⊢ (getKey? k' l).getD fallback = (getKey? k' l).getD fallback

Tactic:
rfl

Result:
no goals

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

Tactic:
next heq =>
split <;> rfl

Result:
no goals

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

Tactic:
split <;> rfl

Result:
no goals