-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF)
    (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α],
      (buckets.1[i].toList.Pairwise fun a b => ¬(a.1 == b.1)) →
      d.toList.Pairwise fun a b => ¬(a.1 == b.1))
    (h₂ : (buckets.1[i].All fun k _ => ((hash k).toUSize % .ofNat buckets.1.size).toNat = i.toNat) →
      d.All fun k _ => ((hash k).toUSize % USize.ofNat buckets.1.size).toNat = i.toNat) :
    (buckets.update i d h).WF

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
⊢ p ∈ (if i✝.toNat = i then d else buckets.val.toList[i]).toList →
    ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Tactic:
split <;> intro hp

Result:
case refine_2.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
h✝ : i✝.toNat = i
hp : p ∈ d.toList
⊢ ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

case refine_2.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
h✝ : ¬i✝.toNat = i
hp : p ∈ buckets.val.toList[i].toList
⊢ ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Proof state:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
⊢ p ∈ (buckets.update i✝ d h).val[i].toList →
    (fun k x => ((hash k).toUSize % USize.ofNat (buckets.update i✝ d h).val.size).toNat = i) p.fst p.snd

Tactic:
simp only [← Array.getElem_toList, toList_update, List.getElem_set,
  Array.length_toList, update_size]

Result:
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
⊢ p ∈ (if i✝.toNat = i then d else buckets.val.toList[i]).toList →
    ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Proof state:
case refine_2.isFalse
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi✝ : i < (buckets.update i✝ d h).val.size
p : α × β
h✝ : ¬i✝.toNat = i
hp : p ∈ buckets.val.toList[i].toList
hi : i < buckets.val.size
⊢ ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Tactic:
exact H.2 i hi _ hp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i : USize
d : AssocList α β
h : i.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat) buckets.val[i] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat) d
⊢ (buckets.update i d h).WF

Tactic:
refine ⟨fun l hl => ?_, fun i hi p hp => ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
buckets : Buckets α β
i : USize
d : AssocList α β
h : i.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat) buckets.val[i] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat) d
inst✝¹ : LawfulHashable α
inst✝ : PartialEquivBEq α
l : AssocList α β
hl : l ∈ (buckets.update i d h).val.toList
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) l.toList

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
i✝ : USize
d : AssocList α β
h : i✝.toNat < buckets.val.size
H : buckets.WF
h₁ :
  ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) buckets.val[i✝].toList →
      List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) d.toList
h₂ :
  AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) buckets.val[i✝] →
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i✝.toNat) d
i : Nat
hi : i < (buckets.update i✝ d h).val.size
p : α × β
hp : p ∈ (buckets.update i✝ d h).val[i].toList
⊢ (fun k x => ((hash k).toUSize % USize.ofNat (buckets.update i✝ d h).val.size).toNat = i) p.fst p.snd