no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
x✝³ : AssocList α β
x✝² : x✝³ ∈ (Bucket.mk (Array.size buckets.val * 2)).val.data
x✝¹ : α × β
x✝ : x✝¹ ∈ AssocList.toList x✝³
⊢ (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size buckets.val) < 0) x✝¹.fst x✝¹.snd
simp_all [Bucket.mk, List.mem_replicate]
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
⊢ Bucket.WF
    (if h : i < Array.size source then
      let idx := { val := i, isLt := h };
      let es := Array.get source idx;
      let source := Array.set source idx AssocList.nil;
      let target := AssocList.foldl reinsertAux target es;
      expand.go (i + 1) source target
    else target)
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
⊢ Bucket.WF (expand.go i source target)
unfold expand.go
case inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
h✝ : i < Array.size source
⊢ Bucket.WF
    (let idx := { val := i, isLt := h✝ };
    let es := Array.get source idx;
    let source := Array.set source idx AssocList.nil;
    let target := AssocList.foldl reinsertAux target es;
    expand.go (i + 1) source target)

case inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
h✝ : ¬i < Array.size source
⊢ Bucket.WF target
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
⊢ Bucket.WF
    (if h : i < Array.size source then
      let idx := { val := i, isLt := h };
      let es := Array.get source idx;
      let source := Array.set source idx AssocList.nil;
      let target := AssocList.foldl reinsertAux target es;
      expand.go (i + 1) source target
    else target)
split
case refine_1
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl : x✝ ∈ (Array.set source { val := i, isLt := H } AssocList.nil).data
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)

case refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
⊢ AssocList.All
    (fun k x =>
      USize.toNat (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)) = i)
    (Array.set source { val := i✝, isLt := H } AssocList.nil)[i]

case refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
⊢ Bucket.WF
    (let idx := { val := i, isLt := H };
    let es := Array.get source idx;
    let source := Array.set source idx AssocList.nil;
    let target := AssocList.foldl reinsertAux target es;
    expand.go (i + 1) source target)
refine go (i+1) (fun _ hl => ?_) (fun i h => ?_) ?_
no goals
case refine_1
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl : x✝ ∈ (Array.set source { val := i, isLt := H } AssocList.nil).data
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
match List.mem_or_eq_of_mem_set hl with
| .inl hl => exact hs₁ _ hl
| .inr e => exact e ▸ .nil
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl✝ : x✝ ∈ (Array.set source { val := i, isLt := H } AssocList.nil).data
hl : x✝ ∈ source.data
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
exact hs₁ _ hl
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl : x✝ ∈ (Array.set source { val := i, isLt := H } AssocList.nil).data
e : x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList x✝)
exact e ▸ .nil
case refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i)
    (if i✝ = i then AssocList.nil else List.get source.data { val := i, isLt := (_ : i < List.length source.data) })
case refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
⊢ AssocList.All
    (fun k x =>
      USize.toNat (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)) = i)
    (Array.set source { val := i✝, isLt := H } AssocList.nil)[i]
simp [Array.getElem_eq_data_get, List.get_set]
case refine_2.inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
h✝ : i✝ = i
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i) AssocList.nil

case refine_2.inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
h✝ : ¬i✝ = i
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i)
    (List.get source.data { val := i, isLt := (_ : i < List.length source.data) })
case refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i)
    (if i✝ = i then AssocList.nil else List.get source.data { val := i, isLt := (_ : i < List.length source.data) })
split
no goals
case refine_2.inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
h✝ : i✝ = i
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i) AssocList.nil
intro.
no goals
case refine_2.inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
h✝ : ¬i✝ = i
⊢ AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = i)
    (List.get source.data { val := i, isLt := (_ : i < List.length source.data) })
exact hs₂ _ (by simp_all)
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i✝ : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i✝) bucket
H : i✝ < Array.size source
i : Nat
h : i < Array.size (Array.set source { val := i✝, isLt := H } AssocList.nil)
h✝ : ¬i✝ = i
⊢ i < Array.size source
simp_all
case refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket
case refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket
let rank (k : α) := ((hash k).toUSize % source.size).toNat
case refine_3.refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
this :
  Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => rank k ≤ i) bucket
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket

case refine_3.refine_1
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
⊢ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList source[i])

case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝¹ : AssocList α β
h₁ : x✝¹ ∈ target.val.data
x✝ : α × β
h₂ : x✝ ∈ AssocList.toList x✝¹
⊢ (fun k x =>
      rank k ≤ i ∧
        ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
          x ∈ AssocList.toList source[i] → ¬(x.fst == k) = true)
    x✝.fst x✝.snd
case refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket
have := expand_WF.foldl rank ?_ (hs₂ _ H) ht.1 (fun _ h₁ _ h₂ => ?_)
case refine_3.refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
this :
  Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => rank k ≤ i) bucket
⊢ Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i + 1) bucket
case refine_3.refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
this :
  Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => rank k ≤ i) bucket
⊢ Bucket.WF (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target (Array.get source { val := i, isLt := H })).val.data →
        AssocList.All
          (fun k x =>
            USize.toNat
                (UInt64.toUSize (hash k) % Array.size (Array.set source { val := i, isLt := H } AssocList.nil)) <
              i + 1)
          bucket
simp
no goals
case refine_3.refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
this :
  Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => rank k ≤ i) bucket
⊢ Bucket.WF (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i + 1) bucket
exact ⟨this.1, fun _ h₁ _ h₂ => Nat.lt_succ_of_le (this.2 _ h₁ _ h₂)⟩
no goals
case refine_3.refine_1
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
⊢ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList source[i])
exact hs₁ _ (Array.getElem_mem_data ..)
case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝¹ : AssocList α β
h₁ : x✝¹ ∈ target.val.data
x✝ : α × β
h₂ : x✝ ∈ AssocList.toList x✝¹
this : (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) x✝.fst x✝.snd
⊢ (fun k x =>
      rank k ≤ i ∧
        ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
          x ∈ AssocList.toList source[i] → ¬(x.fst == k) = true)
    x✝.fst x✝.snd
case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝¹ : AssocList α β
h₁ : x✝¹ ∈ target.val.data
x✝ : α × β
h₂ : x✝ ∈ AssocList.toList x✝¹
⊢ (fun k x =>
      rank k ≤ i ∧
        ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
          x ∈ AssocList.toList source[i] → ¬(x.fst == k) = true)
    x✝.fst x✝.snd
have := ht.2 _ h₁ _ h₂
case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝² : AssocList α β
h₁ : x✝² ∈ target.val.data
x✝¹ : α × β
h₂ : x✝¹ ∈ AssocList.toList x✝²
this : (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) x✝¹.fst x✝¹.snd
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
x✝ : α × β
h : x✝ ∈ AssocList.toList source[i]
h' : (x✝.fst == x✝¹.fst) = true
⊢ USize.toNat (UInt64.toUSize (hash x✝¹.fst) % Array.size source) = i
case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝¹ : AssocList α β
h₁ : x✝¹ ∈ target.val.data
x✝ : α × β
h₂ : x✝ ∈ AssocList.toList x✝¹
this : (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) x✝.fst x✝.snd
⊢ (fun k x =>
      rank k ≤ i ∧
        ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
          x ∈ AssocList.toList source[i] → ¬(x.fst == k) = true)
    x✝.fst x✝.snd
refine ⟨Nat.le_of_lt this, fun _ h h' => Nat.ne_of_lt this ?_⟩
no goals
case refine_3.refine_2
α : Type u_1
β : Type u_2
sz : Nat
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Bucket α β
H✝ : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
H : i < Array.size source
rank : α → Nat := fun k => USize.toNat (UInt64.toUSize (hash k) % Array.size source)
x✝² : AssocList α β
h₁ : x✝² ∈ target.val.data
x✝¹ : α × β
h₂ : x✝¹ ∈ AssocList.toList x✝²
this : (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) x✝¹.fst x✝¹.snd
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
x✝ : α × β
h : x✝ ∈ AssocList.toList source[i]
h' : (x✝.fst == x✝¹.fst) = true
⊢ USize.toNat (UInt64.toUSize (hash x✝¹.fst) % Array.size source) = i
exact LawfulHashable.hash_eq h' ▸ hs₂ _ H _ h
no goals
case inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Bucket α β
H : Bucket.WF buckets
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.data → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) (AssocList.toList bucket)
hs₂ :
  ∀ (j : Nat) (h : j < Array.size source),
    AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) = j) source[j]
target : Bucket α β
ht :
  Bucket.WF target ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.data →
        AssocList.All (fun k x => USize.toNat (UInt64.toUSize (hash k) % Array.size source) < i) bucket
h✝ : ¬i < Array.size source
⊢ Bucket.WF target
exact ht.1