-- 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.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

Tactic:
apply List.containsKey_flatMap_eq_false

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

Tactic:
intro _ h k hki

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

Tactic:
simp only [containsKey_append, Bool.or_eq_false_iff]

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