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

Tactic:
have : getEntry? k' (insertList l (toInsert.map Prod.toSigma)) =
    getEntry? k' (toInsert.map Prod.toSigma) := by
  apply getEntry?_insertList_of_contains_eq_true distinct_l (by simpa [List.pairwise_map])
  apply containsKey_of_beq _ k_beq
  rw [containsKey_eq_contains_map_fst, List.map_map, Prod.fst_comp_toSigma,
    List.contains_iff_exists_mem_beq]
  exists k
  rw [List.mem_map]
  constructor
  . exists ⟨k, v⟩
  . simp

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' (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
⊢ containsKey k' (List.map Prod.toSigma toInsert) = true

Tactic:
apply containsKey_of_beq _ 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
⊢ containsKey k (List.map Prod.toSigma toInsert) = 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
⊢ containsKey k (List.map Prod.toSigma toInsert) = true

Tactic:
rw [containsKey_eq_contains_map_fst, List.map_map, Prod.fst_comp_toSigma,
  List.contains_iff_exists_mem_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
⊢ ∃ a', a' ∈ List.map Prod.fst toInsert ∧ (k == a') = 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
⊢ ∃ a', a' ∈ List.map Prod.fst toInsert ∧ (k == a') = true

Tactic:
exists k

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
⊢ k ∈ List.map Prod.fst 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
⊢ getValue? k' (insertListConst l toInsert) = some v

Tactic:
unfold insertListConst

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
⊢ getValue? 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
⊢ (∃ a, a ∈ toInsert ∧ a.fst = k) ∧ (k == k) = true

Tactic:
constructor

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