-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_alterKey (k k' : α) (f : Option (β k) → Option (β k))
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) :
    getValueCast k' (alterKey k f l) hc =
      if h : k == k' then
        haveI hc' : (f (getValueCast? k l)).isSome

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

Tactic:
split

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

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getValueCast k' (alterKey k f l) hc) =
    if h : (k == k') = true then cast ⋯ (f (getValueCast? k l)) else getValueCast? k' l
h✝ : ¬(k == k') = true
⊢ getValueCast k' (alterKey k f l) hc = getValueCast k' l ⋯

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

Tactic:
rw [getValueCast?_eq_some_getValueCast hc] at this

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

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k k' : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
hc : containsKey k' (alterKey k f l) = true
this :
  some (getValueCast k' (alterKey k f l) hc) =
    if h : (k == k') = true then cast ⋯ (f (getValueCast? k l)) else getValueCast? k' l
h✝ : ¬(k == k') = true
⊢ getValueCast k' (alterKey k f l) hc = getValueCast k' l ⋯

Tactic:
next heq =>
apply Option.some_inj.mp
simp_all only [Bool.false_eq_true, Function.comp_apply, dite_false]
rw [getValueCast?_eq_some_getValueCast]

Result:
no goals

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

Tactic:
rw [getValueCast?_eq_some_getValueCast]

Result:
no goals