-- 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.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
⊢ containsKey k l = false

Tactic:
rwa [← containsKey_congr hhd]

Result:
no goals

Proof state:
case cons
α : 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)
⊢ getEntry? k (insertListIfNewUnit l (hd :: tl)) =
    (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) (hd :: tl)))

Tactic:
simp only [insertListIfNewUnit, ih, getEntry?_insertEntryIfNew, List.map_cons,
  getEntry?_cons]

Result:
case cons
α : 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)
⊢ (if (hd == k && !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 hd == k then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Proof state:
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 : (getEntry? k l).isSome = true
⊢ (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) = some ((getEntry? k l).getD ⟨hd, ()⟩)

Tactic:
obtain ⟨v, hv⟩ := Option.isSome_iff_exists.1 hc

Result:
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, ()⟩)

Proof state:
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
⊢ (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) = some ((getEntry? k l).getD ⟨hd, ()⟩)

Tactic:
rw [containsKey_congr hhd, containsKey_eq_isSome_getEntry?] at hc

Result:
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 : (getEntry? k l).isSome = true
⊢ (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) = some ((getEntry? k l).getD ⟨hd, ()⟩)

Proof state:
case cons
α : 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)
⊢ (if (hd == k && !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 hd == k then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Tactic:
cases hhd : hd == k

Result:
case cons.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) = false
⊢ (if (false && !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 false then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

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))

Proof state:
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))

Tactic:
simp only [Bool.not_true, Bool.and_false, Bool.false_eq_true, ↓reduceIte, cond_true,
  Option.or_some', getEntry?_eq_none]

Result:
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
⊢ (getEntry? k l).or (getEntry? k (List.map (fun x => ⟨x, ()⟩) tl)) = some ((getEntry? k l).getD ⟨hd, ()⟩)

Proof state:
case cons.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) = false
⊢ (if (false && !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 false then some ⟨hd, ()⟩ else getEntry? k (List.map (fun x => ⟨x, ()⟩) tl))

Tactic:
simp

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
⊢ ⟨hd, ()⟩ = (getEntry? k l).getD ⟨hd, ()⟩

Tactic:
rw [getEntry?_eq_none.2, Option.getD_none]

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
⊢ containsKey k l = false