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

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

Tactic:
simp [eraseKey_of_containsKey_eq_false h]

Result:
no goals

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

Tactic:
cases k' == k

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

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

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

Tactic:
rw [cond_true, cond_true]

Result:
no goals

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

Tactic:
rw [cond_false, cond_false, ih, List.cons_append]

Result:
no goals

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

Tactic:
induction l using assoc_induction

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

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

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

Tactic:
rw [List.cons_append, eraseKey_cons, eraseKey_cons]

Result:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
k : α
h : containsKey k l' = false
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : eraseKey k (t ++ l') = eraseKey k t ++ l'
⊢ (bif k' == k then t ++ l' else ⟨k', v'⟩ :: eraseKey k (t ++ l')) =
    (bif k' == k then t else ⟨k', v'⟩ :: eraseKey k t) ++ l'