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

Proof state:
case refine_2.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif true then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

Tactic:
rw [cond_true, Option.some.injEq]

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

Proof state:
case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
⊢ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Tactic:
suffices (k == p.fst) = false by simp_all

Result:
case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
⊢ (k == p.fst) = false

Proof state:
case refine_2.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ getEntry? p.fst t = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

Tactic:
exact Or.inr

Result:
no goals

Proof state:
case refine_1.inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
h : DistinctKeys (⟨k, v⟩ :: t)
ih : DistinctKeys t → (⟨k, v⟩ ∈ t ↔ getEntry? ⟨k, v⟩.fst t = some ⟨k, v⟩)
⊢ (bif k == ⟨k, v⟩.fst then some ⟨k, v⟩ else getEntry? ⟨k, v⟩.fst t) = some ⟨k, v⟩

Tactic:
simp

Result:
no goals

Proof state:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p → (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Tactic:
rintro (rfl|hk)

Result:
case refine_1.inl
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
h : DistinctKeys (⟨k, v⟩ :: t)
ih : DistinctKeys t → (⟨k, v⟩ ∈ t ↔ getEntry? ⟨k, v⟩.fst t = some ⟨k, v⟩)
⊢ (bif k == ⟨k, v⟩.fst then some ⟨k, v⟩ else getEntry? ⟨k, v⟩.fst t) = some ⟨k, v⟩

case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
⊢ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Proof state:
case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

Tactic:
cases k == p.fst

Result:
case refine_2.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif false then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

case refine_2.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif true then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

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

Tactic:
simp only [List.mem_cons, getEntry?_cons, ih h.tail]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p ↔ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
this : (k == p.fst) = false
⊢ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Tactic:
simp_all

Result:
no goals

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

Tactic:
exact Or.inl ∘ Eq.symm

Result:
no goals

Proof state:
case refine_1.inr
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
hk : getEntry? p.fst t = some p
hcon : (k == p.fst) = true
⊢ false = true

Tactic:
rw [← h.containsKey_eq_false, containsKey_congr hcon,
  containsKey_eq_isSome_getEntry?, hk, Option.isSome_some]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p ↔ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p → (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p

case refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif k == p.fst then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

Proof state:
case refine_2.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ (bif false then some ⟨k, v⟩ else getEntry? p.fst t) = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p

Tactic:
rw [cond_false]

Result:
case refine_2.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
p : (a : α) × β a
k : α
v : β k
t : List ((a : α) × β a)
ih : DistinctKeys t → (p ∈ t ↔ getEntry? p.fst t = some p)
h : DistinctKeys (⟨k, v⟩ :: t)
⊢ getEntry? p.fst t = some p → p = ⟨k, v⟩ ∨ getEntry? p.fst t = some p