-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_replaceEntry_of_false [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {a k : α} {v : β k} (h : (k == a) = false) :
    getEntry? a (replaceEntry k v l) = getEntry? a l

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

Tactic:
cases h' : k' == k

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

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

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

Tactic:
rw [replaceEntry_cons_of_true h']

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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : (k == a) = false
⊢ getEntry? a (replaceEntry k v l) = getEntry? a l

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = false
⊢ getEntry? a (replaceEntry k v []) = getEntry? a []

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

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

Tactic:
simp only [getEntry?_cons_of_false h, getEntry?_cons_of_false hk]

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
a k : α
v : β k
h : (k == a) = false
⊢ getEntry? a (replaceEntry k v []) = getEntry? a []

Tactic:
simp

Result:
no goals

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

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

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

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

Tactic:
rw [replaceEntry_cons_of_false h', getEntry?_cons, getEntry?_cons, ih]

Result:
no goals