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

Tactic:
exact ⟨this.1, fun _ h₁ _ h₂ => Nat.lt_succ_of_le (this.2 _ h₁ _ h₂)⟩

Result:
no goals

Proof state:
case refine_2.isFalse
α : 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
h✝ : ¬i✝ = i
⊢ AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat = i) source.toList[i]

Tactic:
exact hs₂ _ (by simp_all)

Result:
no goals

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

Tactic:
simp only [Array.length_toList, Array.size_set, ← Array.getElem_toList,
  Array.toList_set, List.getElem_set]

Result:
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.size).toNat = i)
    (if i✝ = i then AssocList.nil else source.toList[i])

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
⊢ (expand.go i source target).WF

Tactic:
unfold expand.go

Result:
α : 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
⊢ (if h : i < source.size then
      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
    else target).WF