-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem replaceEntry_append_of_containsKey_left [BEq α] {l l' : List ((a : α) × β a)} {k : α}
    {v : β k} (h : containsKey k l) : replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
h' : (k' == k) = false
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Tactic:
simpa [replaceEntry_cons, h'] using ih (h.resolve_left (Bool.not_eq_true _ ▸ h'))

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k [] = true
⊢ replaceEntry k v ([] ++ l') = replaceEntry k v [] ++ l'

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : containsKey k (⟨k', v'⟩ :: t) = true
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Tactic:
simp only [containsKey_cons, Bool.or_eq_true] at h

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Tactic:
cases h' : k' == k

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
h' : (k' == k) = false
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

case true
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
h' : (k' == k) = true
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : containsKey k t = true → replaceEntry k v (t ++ l') = replaceEntry k v t ++ l'
h : (k' == k) = true ∨ containsKey k t = true
h' : (k' == k) = true
⊢ replaceEntry k v (⟨k', v'⟩ :: t ++ l') = replaceEntry k v (⟨k', v'⟩ :: t) ++ l'

Tactic:
simp [replaceEntry_cons, h']

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k l = true
⊢ replaceEntry k v (l ++ l') = replaceEntry k v l ++ l'

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
h : containsKey k [] = true
⊢ replaceEntry k v ([] ++ l') = replaceEntry k v [] ++ l'

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
v : β k
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : containsKey k tail✝ = true → replaceEntry k v (tail✝ ++ l') = replaceEntry k v tail✝ ++ l'
h : containsKey k (⟨k✝, v✝⟩ :: tail✝) = true
⊢ replaceEntry k v (⟨k✝, v✝⟩ :: tail✝ ++ l') = replaceEntry k v (⟨k✝, v✝⟩ :: tail✝) ++ l'