-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem exists_bucket_of_update [BEq α] [Hashable α] (m : Array (AssocList α β)) (h : 0 < m.size)
    (k : α) (f : AssocList α β → AssocList α β) :
    ∃ l : List ((a : α) × β a),
      Perm (toListModel m) ((bucket m h k).toList ++ l) ∧
      Perm (toListModel (updateBucket m h k f)) ((f (bucket m h k)).toList ++ l) ∧
      (∀ [LawfulHashable α], IsHashSelf m → ∀ k', hash k = hash k' → containsKey k' l = false)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
f : AssocList α β → AssocList α β
idx : { u // u.toNat < m.size } := mkIdx m.size h (hash k)
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧
        ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Tactic:
obtain ⟨l, h₁, h₂, h₃⟩ := exists_bucket_of_uset m idx.1 idx.2 (f m[idx.1])

Result:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
f : AssocList α β → AssocList α β
idx : { u // u.toNat < m.size } := mkIdx m.size h (hash k)
l : List ((a : α) × β a)
h₁ : (toListModel m).Perm (m[idx.val.toNat].toList ++ l)
h₂ : (toListModel (m.uset idx.val (f m[idx.val]) ⋯)).Perm ((f m[idx.val]).toList ++ l)
h₃ :
  ∀ [inst : LawfulHashable α],
    IsHashSelf m → ∀ (k : α), (mkIdx m.size ⋯ (hash k)).val.toNat = idx.val.toNat → containsKey k l = false
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧
        ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
f : AssocList α β → AssocList α β
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧
        ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Tactic:
let idx := mkIdx m.size h (hash k)

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
f : AssocList α β → AssocList α β
idx : { u // u.toNat < m.size } := mkIdx m.size h (hash k)
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧
        ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Proof state:
case intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Array (AssocList α β)
h : 0 < m.size
k : α
f : AssocList α β → AssocList α β
idx : { u // u.toNat < m.size } := mkIdx m.size h (hash k)
l : List ((a : α) × β a)
h₁ : (toListModel m).Perm (m[idx.val.toNat].toList ++ l)
h₂ : (toListModel (m.uset idx.val (f m[idx.val]) ⋯)).Perm ((f m[idx.val]).toList ++ l)
h₃ :
  ∀ [inst : LawfulHashable α],
    IsHashSelf m → ∀ (k : α), (mkIdx m.size ⋯ (hash k)).val.toNat = idx.val.toNat → containsKey k l = false
⊢ ∃ l,
    (toListModel m).Perm ((bucket m h k).toList ++ l) ∧
      (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧
        ∀ [inst : LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → containsKey k' l = false

Tactic:
exact ⟨l, h₁, h₂, fun h k' hk' => h₃ h _ (hk' ▸ rfl)⟩

Result:
no goals