-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_eq_some [BEq α] {l : List ((a : α) × β a)} {a : α} {p : (a : α) × β a}
    (h : getEntry? a l = some p) : p.1 == a

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a (⟨k', v'⟩ :: t) = some p
h' : (k' == a) = true
⊢ (p.fst == a) = true

Tactic:
rw [getEntry?_cons_of_true h', Option.some.injEq] at h

Result:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : ⟨k', v'⟩ = p
h' : (k' == a) = true
⊢ (p.fst == a) = true

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
h : getEntry? a [] = some p
⊢ (p.fst == a) = true

Tactic:
simp at h

Result:
no goals

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a t = some p
h' : (k' == a) = false
⊢ (p.fst == a) = true

Tactic:
exact ih h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a (⟨k', v'⟩ :: t) = some p
⊢ (p.fst == a) = true

Tactic:
cases h' : k' == a

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a (⟨k', v'⟩ :: t) = some p
h' : (k' == a) = false
⊢ (p.fst == a) = true

case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a (⟨k', v'⟩ :: t) = some p
h' : (k' == a) = true
⊢ (p.fst == a) = true

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
v' : β p.fst
h : ⟨p.fst, v'⟩ = p
h' : (p.fst == a) = true
⊢ (p.fst == a) = true

Tactic:
exact h'

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
p : (a : α) × β a
h : getEntry? a l = some p
⊢ (p.fst == a) = true

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
h : getEntry? a [] = some p
⊢ (p.fst == a) = true

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getEntry? a tail✝ = some p → (p.fst == a) = true
h : getEntry? a (⟨k✝, v✝⟩ :: tail✝) = some p
⊢ (p.fst == a) = true

Proof state:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : ⟨k', v'⟩ = p
h' : (k' == a) = true
⊢ (p.fst == a) = true

Tactic:
obtain rfl := congrArg Sigma.fst h

Result:
case true
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
v' : β p.fst
h : ⟨p.fst, v'⟩ = p
h' : (p.fst == a) = true
⊢ (p.fst == a) = true

Proof state:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a (⟨k', v'⟩ :: t) = some p
h' : (k' == a) = false
⊢ (p.fst == a) = true

Tactic:
rw [getEntry?_cons_of_false h'] at h

Result:
case false
α : Type u
β : α → Type v
inst✝ : BEq α
a : α
p : (a : α) × β a
k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a t = some p → (p.fst == a) = true
h : getEntry? a t = some p
h' : (k' == a) = false
⊢ (p.fst == a) = true