-- 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) (getEntry? k' (List.map Prod.toSigma toInsert)) = some v

Tactic:
rw [getEntry?_of_mem _ k_beq _]

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

Proof state:
case left
α : 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
⊢ ∃ a, a ∈ toInsert ∧ a.fst = k

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:
. exists ⟨k, v⟩

Result:
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

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)
⊢ ∃ a, a ∈ toInsert ∧ Prod.toSigma a = ⟨k, v⟩

Tactic:
exists (k, v)

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
⊢ k ∈ List.map Prod.fst toInsert ∧ (k == k) = true

Tactic:
rw [List.mem_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
⊢ (∃ a, a ∈ toInsert ∧ a.fst = k) ∧ (k == k) = true

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) (getEntry? k' (insertList l (List.map Prod.toSigma toInsert))) = some v

Tactic:
rw [this]

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)
⊢ Option.map (fun x => x.snd) (getEntry? k' (List.map Prod.toSigma toInsert)) = some v

Proof state:
case left
α : 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
⊢ ∃ a, a ∈ toInsert ∧ a.fst = k

Tactic:
exists ⟨k, v⟩

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)
⊢ ⟨k, v⟩ ∈ List.map Prod.toSigma toInsert

Tactic:
simp only [List.mem_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
this : getEntry? k' (insertList l (List.map Prod.toSigma toInsert)) = getEntry? k' (List.map Prod.toSigma toInsert)
⊢ ∃ a, a ∈ toInsert ∧ Prod.toSigma a = ⟨k, 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)
⊢ ⟨k, v⟩ ∈ List.map Prod.toSigma toInsert

Tactic:
. simp only [List.mem_map]
  exists (k, v)

Result:
no goals