-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_replaceEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a k : α}
    {v : β k} : getKey? a (replaceEntry k v l) =
      if containsKey k l ∧ k == a then some k else getKey? a l

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h✝ : containsKey k l = true ∧ (k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = some k

Tactic:
next h => simp [getEntry?_replaceEntry_of_true h.1 h.2]

Result:
no goals

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

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h✝ : containsKey k l = true ∧ (k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = some k

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h✝ : ¬(containsKey k l = true ∧ (k == a) = true)
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬containsKey k l = true ∨ ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

Tactic:
rcases h with h|h

Result:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬containsKey k l = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

case inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : containsKey k l = true ∧ (k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = some k

Tactic:
simp [getEntry?_replaceEntry_of_true h.1 h.2]

Result:
no goals

Proof state:
case inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬containsKey k l = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

Tactic:
rw [getEntry?_replaceEntry_of_containsKey_eq_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
⊢ getKey? a (replaceEntry k v l) = if containsKey k l = true ∧ (k == a) = true then some k else getKey? a l

Tactic:
rw [getKey?_eq_getEntry?]

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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬(containsKey k l = true ∧ (k == a) = true)
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

Tactic:
simp only [Decidable.not_and_iff_or_not_not] at h

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
a k : α
v : β k
h : ¬containsKey k l = true ∨ ¬(k == a) = true
⊢ Option.map (fun x => x.fst) (getEntry? a (replaceEntry k v l)) = getKey? a l

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

Tactic:
rw [getEntry?_replaceEntry_of_false (Bool.eq_false_iff.2 h), getKey?_eq_getEntry?]

Result:
no goals