-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem expand_WF [BEq α] [Hashable α] {buckets : Buckets α β} (H : buckets.WF) :
    (expand sz buckets).buckets.WF :=
  go _ H.1 H.2 ⟨.mk' _, fun _ _ _ _ => by simp_all [Buckets.mk, List.mem_replicate]⟩
where
  go (i) {source : Array (AssocList α β)}
      (hs₁ : ∀ [LawfulHashable α] [PartialEquivBEq α], ∀ bucket ∈ source.toList,
        bucket.toList.Pairwise fun a b => ¬(a.1 == b.1))
      (hs₂ : ∀ (j : Nat) (h : j < source.size),
        source[j].All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat = j)
      {target : Buckets α β} (ht : target.WF ∧ ∀ bucket ∈ target.1.toList,
        bucket.All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat < i) :
      (expand.go i source target).WF

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

Tactic:
have := expand_WF.foldl rank ?_ (hs₂ _ H) ht.1 (fun _ h₁ _ h₂ => ?_)

Result:
case refine_3.refine_3
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
H✝ : buckets.WF
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) bucket.toList
hs₂ :
  ∀ (j : Nat) (h : j < source.size),
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat = j) source[j]
target : Buckets α β
ht :
  target.WF ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.toList →
        AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat < i) bucket
H : i < source.size
rank : α → Nat := fun k => ((hash k).toUSize % USize.ofNat source.size).toNat
this :
  (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).WF ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target source[i].toList).val.toList →
        AssocList.All (fun k x => rank k ≤ i) bucket
⊢ (AssocList.foldl reinsertAux target source[i]).WF ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ (AssocList.foldl reinsertAux target source[i]).val.toList →
        AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat (source.set i AssocList.nil H).size).toNat < i + 1)
          bucket

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

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