-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_eq_getEntry? [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α} :
    getValueCast? a l = Option.dmap (getEntry? a l)
      (fun p h => cast (congrArg β (eq_of_beq (getEntry?_eq_some h))) p.2)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : List ((a : α) × β a)
ih : getValueCast? a t = Std.DHashMap.Internal.List.Option.dmap (getEntry? a t) fun p h => cast ⋯ p.snd
⊢ getValueCast? a (⟨k, v⟩ :: t) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k, v⟩ :: t)) fun p h => cast ⋯ p.snd

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : List ((a : α) × β a)
ih : getValueCast? a t = Std.DHashMap.Internal.List.Option.dmap (getEntry? a t) fun p h => cast ⋯ p.snd
h : (k == a) = false
⊢ getValueCast? a (⟨k, v⟩ :: t) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k, v⟩ :: t)) fun p h => cast ⋯ p.snd

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : List ((a : α) × β a)
ih : getValueCast? a t = Std.DHashMap.Internal.List.Option.dmap (getEntry? a t) fun p h => cast ⋯ p.snd
h : (k == a) = true
⊢ getValueCast? a (⟨k, v⟩ :: t) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k, v⟩ :: t)) fun p h => cast ⋯ p.snd

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : List ((a : α) × β a)
ih : getValueCast? a t = Std.DHashMap.Internal.List.Option.dmap (getEntry? a t) fun p h => cast ⋯ p.snd
h : (k == a) = true
⊢ getValueCast? a (⟨k, v⟩ :: t) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k, v⟩ :: t)) fun p h => cast ⋯ p.snd

Tactic:
rw [getValueCast?_cons_of_true h, Option.dmap_congr (getEntry?_cons_of_true h),
  Option.dmap_some]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a : α
⊢ getValueCast? a l = Std.DHashMap.Internal.List.Option.dmap (getEntry? a l) fun p h => cast ⋯ p.snd

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ getValueCast? a [] = Std.DHashMap.Internal.List.Option.dmap (getEntry? a []) fun p h => cast ⋯ p.snd

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getValueCast? a tail✝ = Std.DHashMap.Internal.List.Option.dmap (getEntry? a tail✝) fun p h => cast ⋯ p.snd
⊢ getValueCast? a (⟨k✝, v✝⟩ :: tail✝) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k✝, v✝⟩ :: tail✝)) fun p h => cast ⋯ p.snd

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a k : α
v : β k
t : List ((a : α) × β a)
ih : getValueCast? a t = Std.DHashMap.Internal.List.Option.dmap (getEntry? a t) fun p h => cast ⋯ p.snd
h : (k == a) = false
⊢ getValueCast? a (⟨k, v⟩ :: t) =
    Std.DHashMap.Internal.List.Option.dmap (getEntry? a (⟨k, v⟩ :: t)) fun p h => cast ⋯ p.snd

Tactic:
rw [getValueCast?_cons_of_false h, ih, Option.dmap_congr (getEntry?_cons_of_false h)]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ getValueCast? a [] = Std.DHashMap.Internal.List.Option.dmap (getEntry? a []) fun p h => cast ⋯ p.snd

Tactic:
simp

Result:
no goals