-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_of_perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)} {a : α}
    (hl : DistinctKeys l) (h : Perm l l') : getEntry? a l = getEntry? a l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
hl : DistinctKeys l
h : l.Perm l'
⊢ getEntry? a l = getEntry? a l'

Tactic:
induction h

Result:
case nil
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
hl : DistinctKeys []
⊢ getEntry? a [] = getEntry? a []

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
x✝ : (a : α) × β a
l₁✝ l₂✝ : List ((a : α) × β a)
a✝ : l₁✝.Perm l₂✝
a_ih✝ : DistinctKeys l₁✝ → getEntry? a l₁✝ = getEntry? a l₂✝
hl : DistinctKeys (x✝ :: l₁✝)
⊢ getEntry? a (x✝ :: l₁✝) = getEntry? a (x✝ :: l₂✝)

case swap
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
x✝ y✝ : (a : α) × β a
l✝ : List ((a : α) × β a)
hl : DistinctKeys (y✝ :: x✝ :: l✝)
⊢ getEntry? a (y✝ :: x✝ :: l✝) = getEntry? a (x✝ :: y✝ :: l✝)

case trans
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
l₁✝ l₂✝ l₃✝ : List ((a : α) × β a)
a✝¹ : l₁✝.Perm l₂✝
a✝ : l₂✝.Perm l₃✝
a_ih✝¹ : DistinctKeys l₁✝ → getEntry? a l₁✝ = getEntry? a l₂✝
a_ih✝ : DistinctKeys l₂✝ → getEntry? a l₂✝ = getEntry? a l₃✝
hl : DistinctKeys l₁✝
⊢ getEntry? a l₁✝ = getEntry? a l₃✝

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
p p' : (a : α) × β a
l✝ : List ((a : α) × β a)
hl : DistinctKeys (p' :: p :: l✝)
⊢ getEntry? a (p' :: p :: l✝) = getEntry? a (p :: p' :: l✝)

Tactic:
rcases p with ⟨k₁, v₁⟩

Result:
case mk
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
p' : (a : α) × β a
l✝ : List ((a : α) × β a)
k₁ : α
v₁ : β k₁
hl : DistinctKeys (p' :: ⟨k₁, v₁⟩ :: l✝)
⊢ getEntry? a (p' :: ⟨k₁, v₁⟩ :: l✝) = getEntry? a (⟨k₁, v₁⟩ :: p' :: l✝)

Proof state:
case mk.mk
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
l✝ : List ((a : α) × β a)
k₁ : α
v₁ : β k₁
k₂ : α
v₂ : β k₂
hl : DistinctKeys (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝)
⊢ getEntry? a (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝) = getEntry? a (⟨k₁, v₁⟩ :: ⟨k₂, v₂⟩ :: l✝)

Tactic:
simp only [getEntry?_cons]

Result:
case mk.mk
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
l✝ : List ((a : α) × β a)
k₁ : α
v₁ : β k₁
k₂ : α
v₂ : β k₂
hl : DistinctKeys (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝)
⊢ (bif k₂ == a then some ⟨k₂, v₂⟩ else bif k₁ == a then some ⟨k₁, v₁⟩ else getEntry? a l✝) =
    bif k₁ == a then some ⟨k₁, v₁⟩ else bif k₂ == a then some ⟨k₂, v₂⟩ else getEntry? a l✝

Proof state:
case mk.mk
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
l✝ : List ((a : α) × β a)
k₁ : α
v₁ : β k₁
k₂ : α
v₂ : β k₂
hl : DistinctKeys (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝)
⊢ (bif k₂ == a then some ⟨k₂, v₂⟩ else bif k₁ == a then some ⟨k₁, v₁⟩ else getEntry? a l✝) =
    bif k₁ == a then some ⟨k₁, v₁⟩ else bif k₂ == a then some ⟨k₂, v₂⟩ else getEntry? a l✝

Tactic:
cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done

Result:
case mk.mk.true.true
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
a : α
l✝ : List ((a : α) × β a)
k₁ : α
v₁ : β k₁
k₂ : α
v₂ : β k₂
hl : DistinctKeys (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝)
h₂ : (k₂ == a) = true
h₁ : (k₁ == a) = true
⊢ (bif true then some ⟨k₂, v₂⟩ else bif true then some ⟨k₁, v₁⟩ else getEntry? a l✝) =
    bif true then some ⟨k₁, v₁⟩ else bif true then some ⟨k₂, v₂⟩ else getEntry? a l✝