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

Proof state:
case intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (⟨k, v⟩ :: l'')
⊢ t.Perm l''

Tactic:
apply ih hl.tail (hl'.perm hl''.symm).tail

Result:
case intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (⟨k, v⟩ :: l'')
⊢ ∀ (a : α), getEntry? a t = getEntry? a l''

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
hl : DistinctKeys []
k : α
v✝ : β k
tail✝ : List ((a : α) × β a)
a✝ : DistinctKeys tail✝ → (∀ (a : α), getEntry? a [] = getEntry? a tail✝) → [].Perm tail✝
hl' : DistinctKeys (⟨k, v✝⟩ :: tail✝)
h : ∀ (a : α), getEntry? a [] = getEntry? a (⟨k, v✝⟩ :: tail✝)
⊢ [].Perm (⟨k, v✝⟩ :: tail✝)

Tactic:
simpa using h k

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
⊢ containsKey k l' = true

Tactic:
rw [containsKey_eq_isSome_getEntry?, hl'k₁, Option.isSome_some]

Result:
no goals

Proof state:
case intro.false
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (⟨k, v⟩ :: l'')
k' : α
hk' : (k == k') = false
⊢ getEntry? k' t = getEntry? k' l''

Tactic:
simpa only [getEntry?_of_perm hl' hl'', getEntry?_cons_of_false hk'] using h k'

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
⊢ (⟨k, v⟩ :: t).Perm l'

Tactic:
obtain ⟨l'', hl''⟩ := perm_cons_getEntry hl'k₂

Result:
case intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (getEntry k l' hl'k₂ :: l'')
⊢ (⟨k, v⟩ :: t).Perm l'

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

Tactic:
induction l using assoc_induction generalizing l'

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

case cons
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys tail✝ → DistinctKeys l' → (∀ (a : α), getEntry? a tail✝ = getEntry? a l') → tail✝.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k✝, v✝⟩ :: tail✝)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k✝, v✝⟩ :: tail✝) = getEntry? a l'
⊢ (⟨k✝, v✝⟩ :: tail✝).Perm l'

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
⊢ (⟨k, v⟩ :: t).Perm l'

Tactic:
have hl'k₁ : getEntry? k l' = some ⟨k, v⟩ := by rw [← h, getEntry?_cons_self]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
⊢ (⟨k, v⟩ :: t).Perm l'

Proof state:
case intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (⟨k, v⟩ :: l'')
⊢ (⟨k, v⟩ :: t).Perm l'

Tactic:
suffices Perm t l'' from (this.cons _).trans hl''.symm

Result:
case intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k : α
v : β k
t : List ((a : α) × β a)
ih :
  ∀ {l' : List ((a : α) × β a)},
    DistinctKeys t → DistinctKeys l' → (∀ (a : α), getEntry? a t = getEntry? a l') → t.Perm l'
l' : List ((a : α) × β a)
hl : DistinctKeys (⟨k, v⟩ :: t)
hl' : DistinctKeys l'
h : ∀ (a : α), getEntry? a (⟨k, v⟩ :: t) = getEntry? a l'
hl'k₁ : getEntry? k l' = some ⟨k, v⟩
hl'k₂ : containsKey k l' = true
l'' : List ((a : α) × β a)
hl'' : l'.Perm (⟨k, v⟩ :: l'')
⊢ t.Perm l''