-- 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:
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✝)

Tactic:
rcases p' with ⟨k₂, v₂⟩

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✝)
⊢ getEntry? a (⟨k₂, v₂⟩ :: ⟨k₁, v₁⟩ :: l✝) = getEntry? a (⟨k₁, v₁⟩ :: ⟨k₂, v₂⟩ :: l✝)

Proof state:
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₂
h₂ : (k₂ == a) = true
h₁ : (k₁ == a) = true
hl : (DistinctKeys l✝ ∧ containsKey k₁ l✝ = false) ∧ (k₁ == k₂) = false ∧ containsKey k₂ l✝ = false
⊢ (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✝

Tactic:
exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim

Result:
no goals

Proof state:
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
⊢ k₂ = k₁ ∧ HEq v₂ v₁

Tactic:
done

Result:
no goals

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

Tactic:
simp

Result:
no goals

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

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

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

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

Tactic:
exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))

Result:
no goals

Proof state:
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₃✝

Tactic:
next l₁ l₂ l₃ hl₁₂ _ ih₁ ih₂ => exact (ih₁ hl).trans (ih₂ (hl.perm (hl₁₂.symm)))

Result:
no goals

Proof state:
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✝

Tactic:
simp

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
⊢ k₂ = k₁ ∧ HEq v₂ v₁

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

Tactic:
simp only [getEntry?_cons, ih₂ hl.tail]

Result:
no goals

Proof state:
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✝)

Tactic:
next p p' _ =>
rcases p with ⟨k₁, v₁⟩
rcases p' with ⟨k₂, v₂⟩
simp only [getEntry?_cons]
cases h₂ : k₂ == a <;> cases h₁ : k₁ == a <;> try simp; done
simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl
exact ((Bool.eq_false_iff.1 hl.2.1).elim (BEq.trans h₁ (BEq.symm h₂))).elim

Result:
no goals

Proof state:
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✝

Tactic:
simp only [distinctKeys_cons_iff, containsKey_cons, Bool.or_eq_false_iff] at hl

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₂
h₂ : (k₂ == a) = true
h₁ : (k₁ == a) = true
hl : (DistinctKeys l✝ ∧ containsKey k₁ l✝ = false) ∧ (k₁ == k₂) = false ∧ containsKey k₂ l✝ = false
⊢ (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✝

Proof state:
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₂✝)

Tactic:
next p t₁ t₂ _ ih₂ =>
rcases p with ⟨k', v'⟩
simp only [getEntry?_cons, ih₂ hl.tail]

Result:
no goals