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

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Tactic:
simp [h, getKey?_eq_getEntry?]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ getKey? a (eraseKey k l) = if (k == a) = true then none else getKey? a l

Tactic:
rw [getKey?_eq_getEntry?, getEntry?_eraseKey hl]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Tactic:
. simp [h]

Result:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Tactic:
. simp [h, getKey?_eq_getEntry?]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

Tactic:
by_cases h : k == a

Result:
case pos
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : (k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l

case neg
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (if (k == a) = true then none else getEntry? a l) =
    if (k == a) = true then none else getKey? a l