-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem containsKey_insertEntryIfNew [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)}
    {k a : α} {v : β k} :
    containsKey a (insertEntryIfNew k v l) = ((k == a) || containsKey a l)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (k == a && !containsKey k l || (getEntry? a l).isSome) = (k == a || (getEntry? a l).isSome)

Tactic:
cases h : k == a

Result:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = false
⊢ (false && !containsKey k l || (getEntry? a l).isSome) = (false || (getEntry? a l).isSome)

case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ (true && !containsKey k l || (getEntry? a l).isSome) = (true || (getEntry? a l).isSome)

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ (true && !(getEntry? a l).isSome || (getEntry? a l).isSome) = (true || (getEntry? a l).isSome)

Tactic:
simp

Result:
no goals

Proof state:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ (true && !containsKey k l || (getEntry? a l).isSome) = (true || (getEntry? a l).isSome)

Tactic:
rw [containsKey_eq_isSome_getEntry?, getEntry?_congr h]

Result:
case true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = true
⊢ (true && !(getEntry? a l).isSome || (getEntry? a l).isSome) = (true || (getEntry? a l).isSome)

Proof state:
case false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
h : (k == a) = false
⊢ (false && !containsKey k l || (getEntry? a l).isSome) = (false || (getEntry? a l).isSome)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (if (k == a && !(getEntry? k l).isSome) = true then true else (getEntry? a l).isSome) =
    (k == a || (getEntry? a l).isSome)

Tactic:
simp only [Bool.and_eq_true, Bool.not_eq_true', Option.not_isSome, Option.isNone_iff_eq_none,
  getEntry?_eq_none, Bool.if_true_left, Bool.decide_and, Bool.decide_eq_true,
  Bool.decide_eq_false]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (k == a && !containsKey k l || (getEntry? a l).isSome) = (k == a || (getEntry? a l).isSome)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ containsKey a (insertEntryIfNew k v l) = (k == a || containsKey a l)

Tactic:
simp only [containsKey_eq_isSome_getEntry?, getEntry?_insertEntryIfNew, apply_ite Option.isSome,
  Option.isSome_some, if_true_left]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
k a : α
v : β k
⊢ (if (k == a && !(getEntry? k l).isSome) = true then true else (getEntry? a l).isSome) =
    (k == a || (getEntry? a l).isSome)