-- 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:
α : 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
⊢ (let es := source[i];
    let source := source.set i AssocList.nil H;
    let target := AssocList.foldl reinsertAux target es;
    expand.go (i + 1) source target).WF

Tactic:
refine go (i+1) (fun _ hl => ?_) (fun i h => ?_) ?_

Result:
case 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
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl : x✝ ∈ (source.set i AssocList.nil H).toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

case 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
i : Nat
h : i < (source.set i✝ AssocList.nil H).size
⊢ AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat (source.set i✝ AssocList.nil H).size).toNat = i)
    (source.set i✝ AssocList.nil H)[i]

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
⊢ (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

Proof state:
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
H : buckets.WF
x✝³ : AssocList α β
x✝² : x✝³ ∈ (Buckets.mk (buckets.val.size * 2) ⋯).val.toList
x✝¹ : α × β
x✝ : x✝¹ ∈ x✝³.toList
⊢ (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat < 0) x✝¹.fst x✝¹.snd

Tactic:
simp_all [Buckets.mk, List.mem_replicate]

Result:
no goals

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

Tactic:
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.size_set]

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
⊢ (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 => ((hash k).toUSize % USize.ofNat source.size).toNat < i + 1) bucket