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

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

Tactic:
cases h' : k' == k

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

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

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

Tactic:
induction l using assoc_induction

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

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

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

Tactic:
exact h.containsKey_eq_false

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

Tactic:
exact ih h.tail

Result:
no goals

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

Tactic:
rw [eraseKey_cons_of_beq h', ← Option.not_isSome_iff_eq_none, Bool.not_eq_true,
  ← containsKey_eq_isSome_getEntry?, ← containsKey_congr h']

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

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

Tactic:
rw [eraseKey_cons_of_false h', getEntry?_cons_of_false h']

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