-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α × β)} {i : Nat}
    (hl₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], l.Pairwise fun a b => ¬(a.1 == b.1))
    (hl₂ : ∀ x ∈ l, rank x.1 = i)
    {target : Buckets α β} (ht₁ : target.WF)
    (ht₂ : ∀ bucket ∈ target.1.toList,
      bucket.All fun k _ => rank k ≤ i ∧
        ∀ [PartialEquivBEq α] [LawfulHashable α], ∀ x ∈ l, ¬(x.1 == k)) :
    (l.foldl (fun d x => reinsertAux d x.1 x.2) target).WF ∧
    ∀ bucket ∈ (l.foldl (fun d x => reinsertAux d x.1 x.2) target).1.toList,
      bucket.All fun k _ => rank k ≤ i

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
rank : α → Nat
i : Nat
head✝ : α × β
tail✝ : List (α × β)
ih :
  (∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝) →
    (∀ (x : α × β), x ∈ tail✝ → rank x.fst = i) →
      ∀ {target : Buckets α β},
        target.WF →
          (∀ (bucket : AssocList α β),
              bucket ∈ target.val.toList →
                AssocList.All
                  (fun k x =>
                    rank k ≤ i ∧
                      ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
                        x ∈ tail✝ → ¬(x.fst == k) = true)
                  bucket) →
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).WF ∧
              ∀ (bucket : AssocList α β),
                bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.toList →
                  AssocList.All (fun k x => rank k ≤ i) bucket
target : Buckets α β
ht₁ : target.WF
hl₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    (∀ (a' : α × β), a' ∈ tail✝ → ¬(head✝.fst == a'.fst) = true) ∧
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝
hl₂ : rank head✝.fst = i ∧ ∀ (a : α × β), a ∈ tail✝ → rank a.fst = i
ht₂ :
  ∀ (bucket : AssocList α β),
    bucket ∈ target.val.toList →
      AssocList.All
        (fun k x =>
          rank k ≤ i ∧
            ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
              ¬(head✝.fst == k) = true ∧ ∀ (a : α × β), a ∈ tail✝ → ¬(a.fst == k) = true)
        bucket
x✝ : AssocList α β
h✝ :
  x✝ ∈
    target.val.toList.set (mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat
      (AssocList.cons head✝.fst head✝.snd target.val[(mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat])
h : x✝ ∈ target.val.toList
⊢ AssocList.All
    (fun k x =>
      rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β), x ∈ tail✝ → ¬(x.fst == k) = true)
    x✝

Tactic:
intro _ hf

Result:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
rank : α → Nat
i : Nat
head✝ : α × β
tail✝ : List (α × β)
ih :
  (∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝) →
    (∀ (x : α × β), x ∈ tail✝ → rank x.fst = i) →
      ∀ {target : Buckets α β},
        target.WF →
          (∀ (bucket : AssocList α β),
              bucket ∈ target.val.toList →
                AssocList.All
                  (fun k x =>
                    rank k ≤ i ∧
                      ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
                        x ∈ tail✝ → ¬(x.fst == k) = true)
                  bucket) →
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).WF ∧
              ∀ (bucket : AssocList α β),
                bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.toList →
                  AssocList.All (fun k x => rank k ≤ i) bucket
target : Buckets α β
ht₁ : target.WF
hl₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    (∀ (a' : α × β), a' ∈ tail✝ → ¬(head✝.fst == a'.fst) = true) ∧
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝
hl₂ : rank head✝.fst = i ∧ ∀ (a : α × β), a ∈ tail✝ → rank a.fst = i
ht₂ :
  ∀ (bucket : AssocList α β),
    bucket ∈ target.val.toList →
      AssocList.All
        (fun k x =>
          rank k ≤ i ∧
            ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
              ¬(head✝.fst == k) = true ∧ ∀ (a : α × β), a ∈ tail✝ → ¬(a.fst == k) = true)
        bucket
x✝ : AssocList α β
h✝ :
  x✝ ∈
    target.val.toList.set (mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat
      (AssocList.cons head✝.fst head✝.snd target.val[(mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat])
h : x✝ ∈ target.val.toList
a✝ : α × β
hf : a✝ ∈ x✝.toList
⊢ rank a✝.fst ≤ i ∧
    ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β), x ∈ tail✝ → ¬(x.fst == a✝.fst) = true

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
rank : α → Nat
i : Nat
head✝ : α × β
tail✝ : List (α × β)
ih :
  (∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α], List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝) →
    (∀ (x : α × β), x ∈ tail✝ → rank x.fst = i) →
      ∀ {target : Buckets α β},
        target.WF →
          (∀ (bucket : AssocList α β),
              bucket ∈ target.val.toList →
                AssocList.All
                  (fun k x =>
                    rank k ≤ i ∧
                      ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β),
                        x ∈ tail✝ → ¬(x.fst == k) = true)
                  bucket) →
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).WF ∧
              ∀ (bucket : AssocList α β),
                bucket ∈ (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.toList →
                  AssocList.All (fun k x => rank k ≤ i) bucket
target : Buckets α β
ht₁ : target.WF
hl₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    (∀ (a' : α × β), a' ∈ tail✝ → ¬(head✝.fst == a'.fst) = true) ∧
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) tail✝
hl₂ : rank head✝.fst = i ∧ ∀ (a : α × β), a ∈ tail✝ → rank a.fst = i
ht₂ :
  ∀ (bucket : AssocList α β),
    bucket ∈ target.val.toList →
      AssocList.All
        (fun k x =>
          rank k ≤ i ∧
            ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
              ¬(head✝.fst == k) = true ∧ ∀ (a : α × β), a ∈ tail✝ → ¬(a.fst == k) = true)
        bucket
h :
  AssocList.cons head✝.fst head✝.snd target.val[(mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat] ∈
    target.val.toList.set (mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat
      (AssocList.cons head✝.fst head✝.snd target.val[(mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat])
⊢ AssocList.All
    (fun k x =>
      rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α] (x : α × β), x ∈ tail✝ → ¬(x.fst == k) = true)
    (AssocList.cons head✝.fst head✝.snd target.val[(mkIdx ⋯ (hash head✝.fst).toUSize).val.toNat])

Tactic:
intro
| _, .head .. =>
exact ⟨hl₂.1 ▸ Nat.le_refl _, fun _ h h' => hl₁.1 _ h (PartialEquivBEq.symm h')⟩
| _, .tail _ h =>
have ⟨h₁, h₂⟩ := ht₂ _ (Array.getElem_mem_toList ..) _ h
exact ⟨h₁, h₂.2⟩

Result:
no goals