-- 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 : α × β
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

Tactic:
revert hp

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

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

Tactic:
exact match List.mem_or_eq_of_mem_set hl with
| .inl hl => H.1 _ hl
| .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..))

Result:
no goals

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
⊢ ((hash p.fst).toUSize % USize.ofNat buckets.val.size).toNat = i

Tactic:
simp only [update_size, Array.length_toList] at hi

Result:
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

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

Tactic:
next eq => exact eq ▸ h₂ (H.2 _ _) _ hp

Result:
no goals