-- 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 < l₂.length + 1

Tactic:
omega

Result:
no goals

Proof state:
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
j : Nat
hj : j < l₁.length
⊢ (mkIdx self.size h₀ (hash k)).val.toNat ≠ j

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 (self[i] :: l₂)[j + 1].toList = false

Tactic:
rw [List.getElem_append_right' l₁, getElem_congr_coll h₁.symm]

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.toList[j + 1 + l₁.length].toList = false

Proof state:
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
j : Nat
hj : j < l₁.length
⊢ containsKey k l₁[j].toList = false

Tactic:
rw [List.getElem_append_left' (l₂ := self[i] :: l₂), getElem_congr_coll h₁.symm]

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
j : Nat
hj : j < l₁.length
⊢ containsKey k self.toList[j].toList = false

Proof state:
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
j : Nat
hj : j < l₁.length
⊢ containsKey k self.toList[j].toList = false

Tactic:
apply (h.hashes_to j _).containsKey_eq_false h₀ k

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
j : Nat
hj : j < l₁.length
⊢ (mkIdx self.size h₀ (hash k)).val.toNat ≠ j

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

Tactic:
intro j hj

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
j : Nat
hj : j < l₁.length
⊢ containsKey k l₁[j].toList = false

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

Tactic:
rw [toListModel, h₁]

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

Proof state:
α : Type u
β : α → Type v
γ : Type w
δ : α → Type w
inst✝² : BEq α
inst✝¹ : Hashable α
self : Array (AssocList α β)
i : USize
hi : i.toNat < self.size
d : AssocList α β
l : List ((a : α) × β a)
inst✝ : LawfulHashable α
k : α
⊢ 0 < self.size

Tactic:
omega

Result:
no goals