-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
    {l : List ((_ : α) × β)} {toInsert : List (α × β)}
    {k k' : α} (k_beq : k == k') {v : β}
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert) :
    getValue? k' (insertListConst l toInsert) = v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ Option.map (fun x => x.snd) (some ⟨k, ?m.191246⟩) = some v

α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ DistinctKeys (List.map Prod.toSigma toInsert)

α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ β

α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ ⟨k, ?m.191246⟩ ∈ List.map Prod.toSigma toInsert

Tactic:
. rfl

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ DistinctKeys (List.map Prod.toSigma toInsert)

α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ ⟨k, v⟩ ∈ List.map Prod.toSigma toInsert

Proof state:
case right
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ (k == k) = true

Tactic:
. simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ List.Pairwise (fun a b => (a.fst == b.fst) = false) (List.map Prod.toSigma toInsert)

Tactic:
simpa [List.pairwise_map]

Result:
no goals

Proof state:
case right
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ (k == k) = true

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ getValue? k' (insertList l (List.map Prod.toSigma toInsert)) = some v

Tactic:
rw [getValue?_eq_getEntry?]

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ Option.map (fun x => x.snd) (getEntry? k' (insertList l (List.map Prod.toSigma toInsert))) = some v

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ DistinctKeys (List.map Prod.toSigma toInsert)

Tactic:
simpa [DistinctKeys.def, List.pairwise_map]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ Option.map (fun x => x.snd) (some ⟨k, ?m.191246⟩) = some v

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)

Tactic:
apply getEntry?_insertList_of_contains_eq_true distinct_l (by simpa [List.pairwise_map])

Result:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((_ : α) × β)
toInsert : List (α × β)
k k' : α
k_beq : (k == k') = true
v : β
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : (k, v) ∈ toInsert
⊢ containsKey k' (List.map Prod.toSigma toInsert) = true