α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (Bucket.update
      (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val AssocList.nil
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size m.buckets.val))
      (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
      (AssocList.modify k f
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
      (_ :
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
          Array.size
            (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                AssocList.nil
                (_ :
                  USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                    Array.size m.buckets.val)).val))
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF (modify m k f).buckets
dsimp [modify, cond]
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
      (AssocList.modify k f
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
      (_ :
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
          Array.size m.buckets.val))
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (Bucket.update
      (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val AssocList.nil
        (_ :
          USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
            Array.size m.buckets.val))
      (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
      (AssocList.modify k f
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
      (_ :
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
          Array.size
            (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                AssocList.nil
                (_ :
                  USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
                    Array.size m.buckets.val)).val))
rw [Bucket.update_update]
case refine_1
α : Type u_1
β : Type u_2
f : α → β → β
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
H :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (AssocList.toList m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))

case refine_2
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
H :
  AssocList.All
    (fun k_1 x =>
      USize.toNat (UInt64.toUSize (hash k_1) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val)
    m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
a : α × β
h :
  a ∈
    List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
      (AssocList.modify k f
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
      (_ :
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val <
          Array.size m.buckets.val))
refine h.update (fun H => ?_) (fun H a h => ?_) <;> simp at h ⊢
no goals
case refine_1
α : Type u_1
β : Type u_2
f : α → β → β
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
H :
  List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (AssocList.toList m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ List.Pairwise (fun a b => ¬(a.fst == b.fst) = true)
    (List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
exact pairwise_replaceF H
case refine_2
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
H :
  ∀ (a : α × β),
    a ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
a : α × β
h :
  a ∈
    List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
case refine_2
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
H :
  AssocList.All
    (fun k_1 x =>
      USize.toNat (UInt64.toUSize (hash k_1) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val)
    m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
a : α × β
h :
  a ∈
    List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
simp [AssocList.All] at H h ⊢
no goals
case refine_2
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
H :
  ∀ (a : α × β),
    a ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
a : α × β
h :
  a ∈
    List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
match mem_replaceF h with
| .inl rfl => rfl
| .inr h => exact H _ h
no goals
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
h✝ : Bucket.WF m.buckets
a : α × β
H :
  ∀ (a_1 : α × β),
    a_1 ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val] →
      USize.toNat (UInt64.toUSize (hash a_1.fst) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val
h :
  a ∈
    List.replaceF (fun x => bif x.fst == a.fst then some (a.fst, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val
rfl
no goals
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
h✝¹ : Bucket.WF m.buckets
a : α × β
k : α
h :
  a ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
H :
  ∀ (a : α × β),
    a ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
        USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
h✝ :
  a ∈
    List.replaceF (fun x => bif x.fst == k then some (k, f x.fst x.snd) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ USize.toNat (UInt64.toUSize (hash a.fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
exact H _ h