α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (match
        AssocList.contains k
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] with
      | true =>
        { size := m.size - 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.erase k
                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) }
      | false => m).buckets
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF (erase m k).buckets
dsimp [erase, cond]
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
⊢ Bucket.WF
    { size := m.size - 1,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.erase k
              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) }.buckets

case h_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    false
⊢ Bucket.WF m.buckets
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
⊢ Bucket.WF
    (match
        AssocList.contains k
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] with
      | true =>
        { size := m.size - 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.erase k
                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) }
      | false => m).buckets
split
case h_1.refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))

case h_1.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (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 h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
⊢ Bucket.WF
    { size := m.size - 1,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.erase k
              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) }.buckets
refine h.update (fun H => ?_) (fun H a h => ?_) <;> simp at h ⊢
case h_1.refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
case h_1.refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
simp
no goals
case h_1.refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
exact H.sublist (List.eraseP_sublist _)
no goals
case h_1.refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h✝ : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    true
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.eraseP (fun x => x.fst == k)
      (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 _ (List.mem_of_mem_eraseP h)
no goals
case h_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : Bucket.WF m.buckets
c✝ : Bool
heq✝ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    false
⊢ Bucket.WF m.buckets
exact h