-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eraseKey [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    (hl : DistinctKeys l) :
    getValueCast? a (eraseKey k l) = if k == a then none else getValueCast? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

Tactic:
by_cases h : k == a

Result:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

Tactic:
rw [Option.dmap_congr (if_neg h), getValueCast?_eq_getEntry?]

Result:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? a l) fun a_1 h' => cast ⋯ a_1.snd) =
    if (k == a) = true then none else Std.DHashMap.Internal.List.Option.dmap (getEntry? a l) fun p h => cast ⋯ p.snd

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

Tactic:
rw [Option.dmap_congr (if_pos h), Option.dmap_none, if_pos h]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ getValueCast? a (eraseKey k l) = if (k == a) = true then none else getValueCast? a l

Tactic:
rw [getValueCast?_eq_getEntry?, Option.dmap_congr (getEntry?_eraseKey hl)]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ (Std.DHashMap.Internal.List.Option.dmap (if (k == a) = true then none else getEntry? a l) fun a_1 h' =>
      cast ⋯ a_1.snd) =
    if (k == a) = true then none else getValueCast? a l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? a l) fun a_1 h' => cast ⋯ a_1.snd) =
    if (k == a) = true then none else Std.DHashMap.Internal.List.Option.dmap (getEntry? a l) fun p h => cast ⋯ p.snd

Tactic:
exact (if_neg h).symm

Result:
no goals