-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem exists_bucket_of_uset [BEq α] [Hashable α]
  (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) (d : AssocList α β) :
    ∃ l, Perm (toListModel self) (self[i.toNat].toList ++ l) ∧
      Perm (toListModel (self.uset i d hi)) (d.toList ++ l) ∧
      (∀ [LawfulHashable α], IsHashSelf self →
        ∀ k : α, (mkIdx self.size (by omega) (hash k)).1.toNat = i.toNat →
          containsKey k l = false)

Proof state:
case intro.intro.intro.intro.refine_3
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
⊢ containsKey k (List.flatMap AssocList.toList l₁) = false ∧ containsKey k (List.flatMap AssocList.toList l₂) = false

Tactic:
refine ⟨?_, ?_⟩

Result:
case intro.intro.intro.intro.refine_3.refine_1
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
⊢ containsKey k (List.flatMap AssocList.toList l₁) = false

case intro.intro.intro.intro.refine_3.refine_2
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
⊢ containsKey k (List.flatMap AssocList.toList l₂) = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
⊢ ∃ l,
    (toListModel self).Perm (self[i.toNat].toList ++ l) ∧
      (toListModel (self.uset i d hi)).Perm (d.toList ++ l) ∧
        ∀ [inst : LawfulHashable α],
          IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false

Tactic:
obtain ⟨l₁, l₂, h₁, h₂, h₃⟩ := Array.exists_of_uset self i d hi

Result:
case intro.intro.intro.intro
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
⊢ ∃ l,
    (toListModel self).Perm (self[i.toNat].toList ++ l) ∧
      (toListModel (self.uset i d hi)).Perm (d.toList ++ l) ∧
        ∀ [inst : LawfulHashable α],
          IsHashSelf self → ∀ (k : α), (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat → containsKey k l = false

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
⊢ (toListModel (self.uset i d hi)).Perm
    (d.toList ++ (List.flatMap AssocList.toList l₁ ++ List.flatMap AssocList.toList l₂))

Tactic:
rw [toListModel, h₃]

Result:
case intro.intro.intro.intro.refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
⊢ (List.flatMap AssocList.toList (l₁ ++ d :: l₂)).Perm
    (d.toList ++ (List.flatMap AssocList.toList l₁ ++ List.flatMap AssocList.toList l₂))

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
⊢ (List.flatMap AssocList.toList (l₁ ++ d :: l₂)).Perm
    (d.toList ++ (List.flatMap AssocList.toList l₁ ++ List.flatMap AssocList.toList l₂))

Tactic:
simpa using perm_append_comm_assoc _ _ _

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3.refine_2.h
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
j : Nat
hj : j < l₂.length
⊢ containsKey k self.toList[j + 1 + l₁.length].toList = false

Tactic:
apply (h.hashes_to (j + 1 + l₁.length) _).containsKey_eq_false h₀ k

Result:
case intro.intro.intro.intro.refine_3.refine_2.h
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
j : Nat
hj : j < l₂.length
⊢ (mkIdx self.size h₀ (hash k)).val.toNat ≠ j + 1 + l₁.length

Proof state:
case intro.intro.intro.intro.refine_3.refine_2.h
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
j : Nat
hj : j < l₂.length
⊢ (mkIdx self.size h₀ (hash k)).val.toNat ≠ j + 1 + l₁.length

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_3.refine_2.h
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
j : Nat
hj : j < l₂.length
⊢ containsKey k l₂[j].toList = false

Tactic:
rw [← List.getElem_cons_succ self[i] _ _
  (by simp only [Array.ugetElem_eq_getElem, List.length_cons]; omega)]

Result:
case intro.intro.intro.intro.refine_3.refine_2.h
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
h₀ : 0 < self.size
l₁ l₂ : List (AssocList α β)
h₁ : self.toList = l₁ ++ self[i] :: l₂
h₂ : l₁.length = i.toNat
h₃ : (self.uset i d hi).toList = l₁ ++ d :: l₂
inst✝ : LawfulHashable α
h : IsHashSelf self
k : α
hki : (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat
j : Nat
hj : j < l₂.length
⊢ containsKey k (self[i] :: l₂)[j + 1].toList = false