case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : x✝ ∈ (Bucket.mk n).val.data
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)

case refine_2
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h✝ : 0 < n
i : Nat
h : i < Array.size (Bucket.mk n).val
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size (Bucket.mk n).val) = i)
    (Bucket.mk n).val[i]
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h : 0 < n
⊢ WF (Bucket.mk n)
refine ⟨fun _ h => ?_, fun i h => ?_⟩
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : ¬n = 0 ∧ x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : x✝ ∈ (Bucket.mk n).val.data
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
simp [Bucket.mk, empty', mkArray, List.mem_replicate] at h
no goals
case refine_1
α : Type u_1
β : Type u_2
n : Nat
inst✝³ : BEq α
inst✝² : Hashable α
h✝ : 0 < n
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
h : ¬n = 0 ∧ x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
simp [h, List.Pairwise.nil]
no goals
case refine_2
α : Type u_1
β : Type u_2
n : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
h✝ : 0 < n
i : Nat
h : i < Array.size (Bucket.mk n).val
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size (Bucket.mk n).val) = i)
    (Bucket.mk n).val[i]
simp [Bucket.mk, empty', mkArray, Array.getElem_eq_data_get, AssocList.All]