-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast?_replaceEntry [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a k : α}
    {v : β k} : getValueCast? a (replaceEntry k v l) =
      if h : containsKey k l ∧ k == a then some (cast (congrArg β (eq_of_beq h.2)) v)
        else getValueCast? a l

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

Tactic:
simp only [Decidable.not_and_iff_or_not_not] at h

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

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

Tactic:
rw [Option.dmap_congr (getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h)),
  getValueCast?_eq_getEntry?]

Result:
no goals

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

Tactic:
rw [Option.dmap_congr (getEntry?_replaceEntry_of_true h.1 h.2), Option.dmap_some]

Result:
no goals

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

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h✝ : containsKey k l = true ∧ (k == a) = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? a (replaceEntry k v l)) fun p h => cast ⋯ p.snd) = some (cast ⋯ v)

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h✝ : ¬(containsKey k l = true ∧ (k == a) = true)
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? a (replaceEntry k v l)) fun p h => cast ⋯ p.snd) =
    getValueCast? a l

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

Tactic:
next h =>
rw [Option.dmap_congr (getEntry?_replaceEntry_of_true h.1 h.2), Option.dmap_some]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a k : α
v : β k
⊢ getValueCast? a (replaceEntry k v l) =
    if h : containsKey k l = true ∧ (k == a) = true then some (cast ⋯ v) else getValueCast? a l

Tactic:
rw [getValueCast?_eq_getEntry?]

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

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

Tactic:
rcases h with h|h

Result:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬containsKey k l = true
⊢ (Std.DHashMap.Internal.List.Option.dmap (getEntry? a (replaceEntry k v l)) fun p h => cast ⋯ p.snd) =
    getValueCast? a l

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

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

Tactic:
rw [Option.dmap_congr
    (getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h)),
  getValueCast?_eq_getEntry?]

Result:
no goals