-- 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_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])

Tactic:
split

Result:
case refine_2.isTrue
α : 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) AssocList.nil

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]

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
i : Nat
h : i < (source.set i✝ AssocList.nil H).size
h✝ : ¬i✝ = i
⊢ i < source.size

Tactic:
simp_all

Result:
no goals

Proof state:
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
this : (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat < i) x✝.fst x✝.snd
⊢ (fun k x =>
      rank k ≤ i ∧
        ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β), x ∈ source[i].toList → ¬(x.fst == k) = true)
    x✝.fst x✝.snd

Tactic:
refine ⟨Nat.le_of_lt this, fun _ h h' => Nat.ne_of_lt this ?_⟩

Result:
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
this : (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat < i) x✝¹.fst x✝¹.snd
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
x✝ : α × β
h : x✝ ∈ source[i].toList
h' : (x✝.fst == x✝¹.fst) = true
⊢ ((hash x✝¹.fst).toUSize % USize.ofNat source.size).toNat = 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
H : i < source.size
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
x✝ : AssocList α β
hl : x✝ ∈ (source.set i AssocList.nil H).toList
e : x✝ = AssocList.nil
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) x✝.toList

Tactic:
exact e ▸ .nil

Result:
no goals