α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
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,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.replace k v
                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 =>
        if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
          { size := m.size + 1,
            buckets :=
              Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                (AssocList.cons k v
                  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) }
        else
          expand (m.size + 1)
            (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
⊢ Bucket.WF (insert m k v).buckets
dsimp [insert, cond]
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
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,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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 : α
v : β
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
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
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,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.replace k v
                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 =>
        if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
          { size := m.size + 1,
            buckets :=
              Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
                (AssocList.cons k v
                  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) }
        else
          expand (m.size + 1)
            (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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
split
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
⊢ Bucket.WF
    { size := m.size,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  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,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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
simp at h₁
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = true
⊢ Bucket.WF
    { size := m.size,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
⊢ Bucket.WF
    { size := m.size,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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
have ⟨x, hx₁, hx₂⟩ := h₁
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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)
    (AssocList.toList
      (AssocList.replace k v
        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
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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 ∈
    AssocList.toList
      (AssocList.replace k v
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ (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)
    a.fst a.snd
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = true
⊢ Bucket.WF
    { size := m.size,
        buckets :=
          Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.replace k v
              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 => ?_)
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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.replaceF (fun x => bif x.fst == k then some (k, v) else none)
      (AssocList.toList
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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)
    (AssocList.toList
      (AssocList.replace k v
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]))
simp
no goals
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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.replaceF (fun x => bif x.fst == k then some (k, v) 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
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = true
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, v) 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
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = 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 ∈
    AssocList.toList
      (AssocList.replace k v
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ (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)
    a.fst a.snd
simp [AssocList.All] at H h ⊢
no goals
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
x : α × β
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = true
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, v) 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
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
x a : α × β
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val] ∧
      (x.fst == a.fst) = true
hx₁ :
  x ∈
    AssocList.toList
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash a.fst))).val]
hx₂ : (x.fst == a.fst) = true
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, v) 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
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
v : β
h✝¹ : Bucket.WF m.buckets
c✝ : Bool
x a : α × β
k : α
h :
  a ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
h₁ :
  ∃ x,
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ∧
      (x.fst == k) = true
hx₁ :
  x ∈
    AssocList.toList m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val]
hx₂ : (x.fst == k) = true
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, v) 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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ≠
    true
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] =
    false
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
rw [Bool.eq_false_iff] at h₁
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = true
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  AssocList.contains k
      m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] ≠
    true
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
simp at h₁
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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.cons k v
              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
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = true
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
suffices _ by split <;> [exact this; refine expand_WF this]
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = true
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
⊢ ∀ (a' : α × β),
    a' ∈ AssocList.toList m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬((k, v).fst == a'.fst) = true

case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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 ∈
    AssocList.toList
      (AssocList.cons k v
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ (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)
    a.fst a.snd
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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.cons k v
              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 (.cons ?_) (fun H a h => ?_)
no goals
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = true
this : ?m.87772
⊢ Bucket.WF
    (if numBucketsForCapacity (m.size + 1) ≤ Array.size m.buckets.val then
        { size := m.size + 1,
          buckets :=
            Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
              (AssocList.cons k v
                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) }
      else
        expand (m.size + 1)
          (Bucket.update m.buckets (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
            (AssocList.cons k v
              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
split <;> [exact this; refine expand_WF this]
no goals
case refine_1
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = true
inst✝¹ : PartialEquivBEq α
inst✝ : LawfulHashable α
⊢ ∀ (a' : α × β),
    a' ∈ AssocList.toList m.buckets.val[(mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬((k, v).fst == a'.fst) = true
exact fun a h h' => h₁ a h (PartialEquivBEq.symm h')
no goals
case refine_2
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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 ∈
    AssocList.toList
      (AssocList.cons k v
        m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val])
⊢ (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)
    a.fst a.snd
cases h with
| head => rfl
| tail _ h => exact H _ h
no goals
case refine_2.head
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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]
⊢ USize.toNat (UInt64.toUSize (hash (k, v).fst) % Array.size m.buckets.val) =
    USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val
rfl
no goals
case refine_2.tail
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h✝ : Bucket.WF m.buckets
c✝ : Bool
h₁ :
  ∀ (x : α × β),
    x ∈
        AssocList.toList
          m.buckets.val[USize.toNat (mkIdx (_ : 0 < Array.size m.buckets.val) (UInt64.toUSize (hash k))).val] →
      ¬(x.fst == k) = 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 :
  List.Mem 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
exact H _ h