-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_alterKey {k k' : α} [Inhabited (β k')] {f : Option (β k) → Option (β k)}
    (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast! k' (alterKey k f l) =
      if heq : k == k' then
        (f (getValueCast? k l)).map (cast (congrArg β <| eq_of_beq heq)) |>.get!
      else
        getValueCast! k' l

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

Tactic:
next heq =>
cases eq_of_beq heq
simp only [cast_eq, Option.map_cast_apply]

Result:
no goals

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

Tactic:
simp only [cast_eq, Option.map_cast_apply]

Result:
no goals

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

Tactic:
simp only [hl, getValueCast!_eq_getValueCast?, getValueCast?_alterKey, beq_iff_eq,
  Function.comp_apply]

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

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

Tactic:
cases eq_of_beq heq

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

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
k k' : α
inst✝ : Inhabited (β k')
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
h✝ : ¬(k == k') = true
⊢ (getValueCast? k' l).get! = (getValueCast? k' l).get!

Tactic:
rfl

Result:
no goals

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

Tactic:
split

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

case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
k k' : α
inst✝ : Inhabited (β k')
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
hl : DistinctKeys l
h✝ : ¬(k == k') = true
⊢ (getValueCast? k' l).get! = (getValueCast? k' l).get!