-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_of_mem [BEq α] [PartialEquivBEq α]
    {l : List ((a : α) × β a)} (hl : DistinctKeys l)
    {k k' : α} (hk : k == k') {v : β k} (hkv : ⟨k, v⟩ ∈ l) :
    getEntry? k' l = some ⟨k, v⟩

Proof state:
case cons.inl.refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k, v⟩ :: t)
hkv : ⟨k, v⟩ ∈ ⟨k, v⟩ :: t
⊢ getEntry? k' (⟨k, v⟩ :: t) = some ⟨k, v⟩

Tactic:
rw [getEntry?_cons_of_true hk]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
k₁ : α
v₁ : β k₁
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k₁, v₁⟩ :: t)
hkv : ⟨k, v⟩ ∈ ⟨k₁, v₁⟩ :: t
⊢ getEntry? k' (⟨k₁, v₁⟩ :: t) = some ⟨k, v⟩

Tactic:
obtain ⟨⟨⟩⟩|hkv := List.mem_cons.1 hkv

Result:
case cons.inl.refl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k, v⟩ :: t)
hkv : ⟨k, v⟩ ∈ ⟨k, v⟩ :: t
⊢ getEntry? k' (⟨k, v⟩ :: t) = some ⟨k, v⟩

case cons.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
k₁ : α
v₁ : β k₁
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k₁, v₁⟩ :: t)
hkv✝ : ⟨k, v⟩ ∈ ⟨k₁, v₁⟩ :: t
hkv : ⟨k, v⟩ ∈ t
⊢ getEntry? k' (⟨k₁, v₁⟩ :: t) = some ⟨k, v⟩

Proof state:
case cons.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
k₁ : α
v₁ : β k₁
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k₁, v₁⟩ :: t)
hkv✝ : ⟨k, v⟩ ∈ ⟨k₁, v₁⟩ :: t
hkv : ⟨k, v⟩ ∈ t
⊢ (k₁ == k') = false

Tactic:
exact BEq.neq_of_neq_of_beq (containsKey_eq_false_iff.1 hl.containsKey_eq_false _ hkv) hk

Result:
no goals

Proof state:
case cons.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
k₁ : α
v₁ : β k₁
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k₁, v₁⟩ :: t)
hkv✝ : ⟨k, v⟩ ∈ ⟨k₁, v₁⟩ :: t
hkv : ⟨k, v⟩ ∈ t
⊢ getEntry? k' (⟨k₁, v₁⟩ :: t) = some ⟨k, v⟩

Tactic:
rw [getEntry?_cons_of_false, ih hl.tail hkv]

Result:
case cons.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
k₁ : α
v₁ : β k₁
t : List ((a : α) × β a)
ih : DistinctKeys t → ⟨k, v⟩ ∈ t → getEntry? k' t = some ⟨k, v⟩
hl : DistinctKeys (⟨k₁, v₁⟩ :: t)
hkv✝ : ⟨k, v⟩ ∈ ⟨k₁, v₁⟩ :: t
hkv : ⟨k, v⟩ ∈ t
⊢ (k₁ == k') = false

Proof state:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
k k' : α
hk : (k == k') = true
v : β k
hl : DistinctKeys []
hkv : ⟨k, v⟩ ∈ []
⊢ getEntry? k' [] = some ⟨k, v⟩

Tactic:
simp at hkv

Result:
no goals