-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × Unit)} {toInsert : List α}
    {k k' : α} (k_beq : k == k')
    (mem' : containsKey k l = false)
    (distinct : toInsert.Pairwise (fun a b => (a == b) = false)) (mem : k ∈ toInsert):
    getKey? k' (insertListIfNewUnit l toInsert) = some k

Proof state:
case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Tactic:
apply getEntry?_of_mem (DistinctKeys.mapUnit distinct) k_beq

Result:
case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ⟨k, ()⟩ ∈ List.map (fun x => ⟨x, ()⟩) toInsert

Proof state:
case h.left
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k' l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false

Tactic:
exact mem'

Result:
no goals

Proof state:
case h.left
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false

Tactic:
rw [containsKey_congr k_beq] at mem'

Result:
case h.left
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k' l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ (getEntry? k' l = some ⟨k, ()⟩ ∨
      containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩) ∧
    ⟨k, ()⟩.fst = k

Tactic:
simp only [and_true]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getEntry? k' l = some ⟨k, ()⟩ ∨
    containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Proof state:
case h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Tactic:
constructor

Result:
case h.left
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false

case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Proof state:
case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ⟨k, ()⟩ ∈ List.map (fun x => ⟨x, ()⟩) toInsert

Tactic:
simp only [List.mem_map]

Result:
case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ∃ a, a ∈ toInsert ∧ ⟨a, ()⟩ = ⟨k, ()⟩

Proof state:
case h.right
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ∃ a, a ∈ toInsert ∧ ⟨a, ()⟩ = ⟨k, ()⟩

Tactic:
exists k

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getEntry? k' l = some ⟨k, ()⟩ ∨
    containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Tactic:
right

Result:
case h
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ getKey? k' (insertListIfNewUnit l toInsert) = some k

Tactic:
simp only [getKey?_eq_getEntry?, getEntry?_insertListIfNewUnit, Option.map_eq_some',
  Option.or_eq_some, getEntry?_eq_none]

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ∃ a,
    (getEntry? k' l = some a ∨
        containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some a) ∧
      a.fst = k

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ ∃ a,
    (getEntry? k' l = some a ∨
        containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some a) ∧
      a.fst = k

Tactic:
exists ⟨k, ()⟩

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × Unit)
toInsert : List α
k k' : α
k_beq : (k == k') = true
mem' : containsKey k l = false
distinct : List.Pairwise (fun a b => (a == b) = false) toInsert
mem : k ∈ toInsert
⊢ (getEntry? k' l = some ⟨k, ()⟩ ∨
      containsKey k' l = false ∧ getEntry? k' (List.map (fun x => ⟨x, ()⟩) toInsert) = some ⟨k, ()⟩) ∧
    ⟨k, ()⟩.fst = k