-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_replaceEntry_of_true [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {a k : α} {v : β k} (hl : containsKey k l = true) (h : k == a) :
    getEntry? a (replaceEntry k v l) = some ⟨k, v⟩

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
⊢ getEntry? a (replaceEntry k v (⟨k', v'⟩ :: l)) = some ⟨k, v⟩

Tactic:
rw [replaceEntry_cons_of_false hk'a]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
⊢ getEntry? a (⟨k', v'⟩ :: replaceEntry k v l) = some ⟨k, v⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
hl : containsKey k l = true
h : (k == a) = true
⊢ getEntry? a (replaceEntry k v l) = some ⟨k, v⟩

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
hl : containsKey k [] = true
⊢ getEntry? a (replaceEntry k v []) = some ⟨k, v⟩

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = true → getEntry? a (replaceEntry k v tail✝) = some ⟨k, v⟩
hl : containsKey k (⟨k✝, v✝⟩ :: tail✝) = true
⊢ getEntry? a (replaceEntry k v (⟨k✝, v✝⟩ :: tail✝)) = some ⟨k, v⟩

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
⊢ getEntry? a (⟨k', v'⟩ :: replaceEntry k v l) = some ⟨k, v⟩

Tactic:
have hk'k : (k' == a) = false := BEq.neq_of_neq_of_beq hk'a h

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
hk'k : (k' == a) = false
⊢ getEntry? a (⟨k', v'⟩ :: replaceEntry k v l) = some ⟨k, v⟩

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
hk'k : (k' == a) = false
⊢ getEntry? a (replaceEntry k v l) = some ⟨k, v⟩

Tactic:
exact ih (containsKey_of_containsKey_cons hl hk'a)

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
hl : containsKey k [] = true
⊢ getEntry? a (replaceEntry k v []) = some ⟨k, v⟩

Tactic:
simp at hl

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = true
⊢ getEntry? a (replaceEntry k v (⟨k', v'⟩ :: l)) = some ⟨k, v⟩

Tactic:
rw [replaceEntry_cons_of_true hk'a, getEntry?_cons_of_true h]

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
hk'k : (k' == a) = false
⊢ getEntry? a (⟨k', v'⟩ :: replaceEntry k v l) = some ⟨k, v⟩

Tactic:
rw [getEntry?_cons_of_false hk'k]

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
hk'k : (k' == a) = false
⊢ getEntry? a (replaceEntry k v l) = some ⟨k, v⟩

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
⊢ getEntry? a (replaceEntry k v (⟨k', v'⟩ :: l)) = some ⟨k, v⟩

Tactic:
cases hk'a : k' == k

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = false
⊢ getEntry? a (replaceEntry k v (⟨k', v'⟩ :: l)) = some ⟨k, v⟩

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = true
k' : α
v' : β k'
l : List ((a : α) × β a)
ih : containsKey k l = true → getEntry? a (replaceEntry k v l) = some ⟨k, v⟩
hl : containsKey k (⟨k', v'⟩ :: l) = true
hk'a : (k' == k) = true
⊢ getEntry? a (replaceEntry k v (⟨k', v'⟩ :: l)) = some ⟨k, v⟩