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

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

Tactic:
rwa [containsKey_modifyKey] at h

Result:
no goals

Proof state:
case isFalse
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
h✝ : ¬(k == k') = true
⊢ getValue k' l ⋯ = getValue k' l ⋯

Tactic:
rfl

Result:
no goals

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

Tactic:
rwa [containsKey_modifyKey, ← containsKey_congr heq] at h

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ (if h_1 : (k == k') = true then (Option.map f (getValue? k l)).get ⋯ else getValue k' l ⋯) =
    if heq : (k == k') = true then f (getValue k l ⋯) else getValue k' l ⋯

Tactic:
split

Result:
case isTrue
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
h✝ : (k == k') = true
⊢ (Option.map f (getValue? k l)).get ⋯ = f (getValue k l ⋯)

case isFalse
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
h✝ : ¬(k == k') = true
⊢ getValue k' l ⋯ = getValue k' l ⋯

Proof state:
case isTrue
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
h✝ : (k == k') = true
⊢ (Option.map f (getValue? k l)).get ⋯ = f (getValue k l ⋯)

Tactic:
next heq =>
haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← containsKey_congr heq] at h
simp [getValue?_eq_some_getValue, h']

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ getValue k' (modifyKey k f l) h = if heq : (k == k') = true then f (getValue k l ⋯) else getValue k' l ⋯

Tactic:
simp only [modifyKey_eq_alterKey, getValue_alterKey, hl]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
⊢ (if h_1 : (k == k') = true then (Option.map f (getValue? k l)).get ⋯ else getValue k' l ⋯) =
    if heq : (k == k') = true then f (getValue k l ⋯) else getValue k' l ⋯

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
heq : (k == k') = true
h' : containsKey k l = true
⊢ (Option.map f (getValue? k l)).get ⋯ = f (getValue k l ⋯)

Tactic:
simp [getValue?_eq_some_getValue, h']

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
heq : (k == k') = true
⊢ (Option.map f (getValue? k l)).get ⋯ = f (getValue k l ⋯)

Tactic:
haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← containsKey_congr heq] at h

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
heq : (k == k') = true
h' : containsKey k l = true
⊢ (Option.map f (getValue? k l)).get ⋯ = f (getValue k l ⋯)

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k' (modifyKey k f l) = true
heq : (k == k') = true
⊢ containsKey k l = true

Tactic:
rwa [containsKey_modifyKey, ← containsKey_congr heq] at h

Result:
no goals