-- 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 (getEntry k l' hl'k₂ :: l'')
⊢ (⟨k, v⟩ :: t).Perm l'

Tactic:
rw [getEntry_eq_of_getEntry?_eq_some hl'k₁] at hl''

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'')
⊢ (⟨k, v⟩ :: t).Perm l'

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

Tactic:
induction l' using assoc_induction

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

case nil.cons
α : 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✝)

Proof state:
case intro.true
α : 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') = true
⊢ getEntry? k' t = getEntry? k' l''

Tactic:
rw [← getEntry?_congr hk', ← getEntry?_congr hk', getEntry?_eq_none.2 hl.containsKey_eq_false,
    getEntry?_eq_none.2 (hl'.perm hl''.symm).containsKey_eq_false]

Result:
no goals

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

Tactic:
exact Perm.refl _

Result:
no goals

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'')
⊢ ∀ (a : α), getEntry? a t = getEntry? a l''

Tactic:
intro 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 (⟨k, v⟩ :: l'')
k' : α
⊢ getEntry? k' t = getEntry? k' l''

Proof state:
case nil.cons
α : 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:
next k _ _ _ => simpa using h k

Result:
no goals

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' : α
⊢ getEntry? k' t = getEntry? k' l''

Tactic:
cases hk' : k == k'

Result:
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''

case intro.true
α : 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') = true
⊢ getEntry? k' t = getEntry? k' 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'
⊢ getEntry? k l' = some ⟨k, v⟩

Tactic:
rw [← h, getEntry?_cons_self]

Result:
no goals