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

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

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

Result:
no goals

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

Tactic:
split

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

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

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

Tactic:
simp [getValueCast?_eq_some_getValueCast, h']

Result:
no goals

Proof state:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
heq : (k == k) = true
⊢ cast ⋯ ((Option.map f (getValueCast? k l)).get ⋯) = cast ⋯ (f (getValueCast k l ⋯))

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

Result:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
heq : (k == k) = true
h' : containsKey k l = true
⊢ cast ⋯ ((Option.map f (getValueCast? k l)).get ⋯) = cast ⋯ (f (getValueCast k l ⋯))

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

Tactic:
simp only [modifyKey_eq_alterKey, getValueCast_alterKey, hl]

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

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

Tactic:
next heq =>
cases eq_of_beq heq
haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← eq_of_beq heq] at h
simp [getValueCast?_eq_some_getValueCast, h']

Result:
no goals

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

Tactic:
cases eq_of_beq heq

Result:
case refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : β k → β k
l : List ((a : α) × β a)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
heq : (k == k) = true
⊢ cast ⋯ ((Option.map f (getValueCast? k l)).get ⋯) = cast ⋯ (f (getValueCast k l ⋯))

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

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

Result:
no goals

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

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : β k → β k
l : List ((a : α) × β a)
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