-- 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:
α : 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
⊢ j + 1 < (self[i] :: l₂).length

Tactic:
simp only [Array.ugetElem_eq_getElem, List.length_cons]

Result:
α : 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
⊢ j + 1 < l₂.length + 1

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

Tactic:
refine ⟨l₁.flatMap AssocList.toList ++ l₂.flatMap AssocList.toList, ?_, ?_, ?_⟩

Result:
case intro.intro.intro.intro.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₂
⊢ (toListModel self).Perm
    (self[i.toNat].toList ++ (List.flatMap AssocList.toList l₁ ++ List.flatMap AssocList.toList l₂))

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₂))

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 α],
    IsHashSelf self →
      ∀ (k : α),
        (mkIdx self.size ⋯ (hash k)).val.toNat = i.toNat →
          containsKey k (List.flatMap AssocList.toList l₁ ++ 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 α β
⊢ 0 < self.size

Tactic:
omega

Result:
no goals

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

Tactic:
apply List.containsKey_flatMap_eq_false

Result:
case intro.intro.intro.intro.refine_3.refine_1.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
⊢ ∀ (i : Nat) (h : i < l₁.length), containsKey k l₁[i].toList = false

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
⊢ ∀ (i : Nat) (h : i < l₂.length), containsKey k l₂[i].toList = false

Tactic:
intro j hj

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 l₂[j].toList = false

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
⊢ ∃ 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:
have h₀ : 0 < self.size := by omega

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