-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_insertListIfNewUnit_of_contains_eq_false [BEq α] [PartialEquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α } {k : α}
    (not_contains : toInsert.contains k = false) :
    getEntry? k (insertListIfNewUnit l toInsert) = getEntry? k l

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
h' : false = true
⊢ containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Tactic:
simp at h'

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (h :: t).contains k = false
⊢ getEntry? k (insertListIfNewUnit l (h :: t)) = getEntry? k l

Tactic:
unfold insertListIfNewUnit

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (h :: t).contains k = false
⊢ getEntry? k (insertListIfNewUnit (insertEntryIfNew h () l) t) = getEntry? k l

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ (h == k) = true → containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Tactic:
intro h'

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
h' : (h == k) = true
⊢ containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (h :: t).contains k = false
⊢ getEntry? k (insertListIfNewUnit (insertEntryIfNew h () l) t) = getEntry? k l

Tactic:
simp only [List.contains_cons, Bool.or_eq_false_iff] at not_contains

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ getEntry? k (insertListIfNewUnit (insertEntryIfNew h () l) t) = getEntry? k l

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ (if (h == k && !containsKey h l) = true then some ⟨h, ()⟩ else getEntry? k l) = getEntry? k l

Tactic:
simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, ite_eq_right_iff, and_imp]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ (h == k) = true → containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
not_contains : toInsert.contains k = false
⊢ getEntry? k (insertListIfNewUnit l toInsert) = getEntry? k l

Tactic:
induction toInsert generalizing l with
| nil => simp [insertListIfNewUnit]
| cons h t ih =>
  unfold insertListIfNewUnit
  simp only [List.contains_cons, Bool.or_eq_false_iff] at not_contains
  rw [ih not_contains.right, getEntry?_insertEntryIfNew]
  simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true, ite_eq_right_iff, and_imp]
  intro h'
  rw [BEq.comm, And.left not_contains] at h'
  simp at h'

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
h' : (h == k) = true
⊢ containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Tactic:
rw [BEq.comm, And.left not_contains] at h'

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
h' : false = true
⊢ containsKey h l = false → some ⟨h, ()⟩ = getEntry? k l

Proof state:
case nil
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k : α
l : List ((_ : α) × Unit)
not_contains : [].contains k = false
⊢ getEntry? k (insertListIfNewUnit l []) = getEntry? k l

Tactic:
simp [insertListIfNewUnit]

Result:
no goals

Proof state:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ getEntry? k (insertListIfNewUnit (insertEntryIfNew h () l) t) = getEntry? k l

Tactic:
rw [ih not_contains.right, getEntry?_insertEntryIfNew]

Result:
case cons
α : Type u
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k h : α
t : List α
ih : ∀ {l : List ((_ : α) × Unit)}, t.contains k = false → getEntry? k (insertListIfNewUnit l t) = getEntry? k l
l : List ((_ : α) × Unit)
not_contains : (k == h) = false ∧ t.contains k = false
⊢ (if (h == k && !containsKey h l) = true then some ⟨h, ()⟩ else getEntry? k l) = getEntry? k l