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

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

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
k : α
p p' : (a : α) × β a
l✝ : List ((a : α) × β a)
⊢ (p'.fst == k || (p.fst == k || containsKey k l✝)) = (p.fst == k || (p'.fst == k || containsKey k l✝))

Tactic:
simp only [← Bool.or_assoc, Bool.or_comm]

Result:
no goals

Proof state:
case trans
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
k : α
l₁✝ l₂✝ l₃✝ : List ((a : α) × β a)
a✝¹ : l₁✝.Perm l₂✝
a✝ : l₂✝.Perm l₃✝
a_ih✝¹ : containsKey k l₁✝ = containsKey k l₂✝
a_ih✝ : containsKey k l₂✝ = containsKey k l₃✝
⊢ containsKey k l₁✝ = containsKey k l₃✝

Tactic:
next _ _ _ _ _ ih₁ ih₂ => exact ih₁.trans ih₂

Result:
no goals

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

Tactic:
rw [containsKey_cons, containsKey_cons, ih₂]

Result:
no goals

Proof state:
case swap
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
k : α
x✝ y✝ : (a : α) × β a
l✝ : List ((a : α) × β a)
⊢ containsKey k (y✝ :: x✝ :: l✝) = containsKey k (x✝ :: y✝ :: l✝)

Tactic:
next p p' _ =>
rw [containsKey_cons, containsKey_cons, containsKey_cons, containsKey_cons]
simp only [← Bool.or_assoc, Bool.or_comm]

Result:
no goals

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

Tactic:
induction h

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

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

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

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

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

Tactic:
exact ih₁.trans ih₂

Result:
no goals

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

Tactic:
rw [containsKey_cons, containsKey_cons, containsKey_cons, containsKey_cons]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
k : α
p p' : (a : α) × β a
l✝ : List ((a : α) × β a)
⊢ (p'.fst == k || (p.fst == k || containsKey k l✝)) = (p.fst == k || (p'.fst == k || containsKey k l✝))

Proof state:
case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l l' : List ((a : α) × β a)
k : α
x✝ : (a : α) × β a
l₁✝ l₂✝ : List ((a : α) × β a)
a✝ : l₁✝.Perm l₂✝
a_ih✝ : containsKey k l₁✝ = containsKey k l₂✝
⊢ containsKey k (x✝ :: l₁✝) = containsKey k (x✝ :: l₂✝)

Tactic:
next p t₁ t₂ _ ih₂ => rw [containsKey_cons, containsKey_cons, ih₂]

Result:
no goals