-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
    getKey k' (alterKey k f l) hc =
      if heq : k == k' then
        k
      else
        haveI h' : containsKey k' l

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

Tactic:
rwa [containsKey_alterKey hl, if_neg heq] at hc

Result:
no goals

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

Tactic:
apply Option.some_inj.mp

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

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
heq : ¬(k == k') = true
this : some (getKey k' (alterKey k f l) hc) = getKey? k' l
⊢ getKey? k' l = some (getKey k' l ⋯)

Tactic:
rw [getKey?_eq_some_getKey]

Result:
no goals

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
⊢ getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

Tactic:
have := getKey?_alterKey (f := f) (k := k) (k' := k') _ hl

Result:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  getKey? k' (alterKey k f l) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
⊢ getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
heq : ¬(k == k') = true
⊢ some (getKey k' (alterKey k f l) hc) = some (getKey k' l ⋯)

Tactic:
simp_all only [Bool.false_eq_true, ite_false]

Result:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
heq : ¬(k == k') = true
this : some (getKey k' (alterKey k f l) hc) = getKey? k' l
⊢ getKey? k' l = some (getKey k' l ⋯)

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

Tactic:
split

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

case isFalse
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
h✝ : ¬(k == k') = true
⊢ getKey k' (alterKey k f l) hc = getKey k' l ⋯

Proof state:
case isFalse
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
h✝ : ¬(k == k') = true
⊢ getKey k' (alterKey k f l) hc = getKey k' l ⋯

Tactic:
next heq =>
apply Option.some_inj.mp
simp_all only [Bool.false_eq_true, ite_false]
rw [getKey?_eq_some_getKey]

Result:
no goals

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

Tactic:
simp_all

Result:
no goals

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

Tactic:
rw [getKey?_eq_some_getKey hc] at this

Result:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
⊢ getKey k' (alterKey k f l) hc = if heq : (k == k') = true then k else getKey k' l ⋯

Proof state:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
heq : ¬(k == k') = true
⊢ getKey k' (alterKey k f l) hc = getKey k' l ⋯

Tactic:
apply Option.some_inj.mp

Result:
α : Type u
inst✝² : BEq α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k k' : α
f : Option β → Option β
l : List ((_ : α) × β)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getKey k' (alterKey k f l) hc) =
    if (k == k') = true then if (f (getValue? k l)).isSome = true then some k else none else getKey? k' l
heq : ¬(k == k') = true
⊢ some (getKey k' (alterKey k f l) hc) = some (getKey k' l ⋯)