-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertListIfNewUnit [BEq α] [PartialEquivBEq α] {l : List ((_ : α) × Unit)}
    {toInsert : List α} {k : α} :
    getEntry? k (insertListIfNewUnit l toInsert) =
      (getEntry? k l).or (getEntry? k (toInsert.map (⟨·, ()⟩)))

Proof state:
case cons.true
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
⊢ (if (true && !containsKey hd l) = true then some ⟨hd, ()⟩ else getEntry? k l).or
      (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) =
    (getEntry? k l).or (bif true then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Tactic:
cases hc : containsKey hd l

Result:
case cons.true.false
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
hc : containsKey hd l = false
⊢ (if (true && !false) = true then some ⟨hd, ()⟩ else getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) =
    (getEntry? k l).or (bif true then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

case cons.true.true
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
hc : containsKey hd l = true
⊢ (if (true && !true) = true then some ⟨hd, ()⟩ else getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) =
    (getEntry? k l).or (bif true then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Proof state:
case cons.true.true.intro
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
hc : (getEntry? k l).isSome = true
v : (_ : α) × Unit
hv : getEntry? k l = some v
⊢ (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) = some ((getEntry? k l).getD ⟨hd, ()⟩)

Tactic:
simp [hv]

Result:
no goals

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
l : List ((_ : α) × Unit)
⊢ getEntry? k (insertListIfNewUnit l []) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) []))

Tactic:
simp [insertListIfNewUnit]

Result:
no goals

Proof state:
case cons.true.false
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
hc : containsKey hd l = false
⊢ (if (true && !false) = true then some ⟨hd, ()⟩ else getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) =
    (getEntry? k l).or (bif true then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Tactic:
simp only [Bool.not_false, Bool.and_self, ↓reduceIte, Option.some_or, cond_true,
  Option.or_some', Option.some.injEq]

Result:
case cons.true.false
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k hd : α
tl : List α
ih :
  ∀ {l : List ((_ : α) × Unit)},
    getEntry? k (insertListIfNewUnit l tl) = (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))
l : List ((_ : α) × Unit)
hhd : (hd == k) = true
hc : containsKey hd l = false
⊢ ⟨hd, ()⟩ = (getEntry? k l).getD ⟨hd, ()⟩