-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem insert_size [BEq α] [Hashable α] {m : Imp α β} {k v}
    (h : m.size = m.buckets.size) :
    (insert m k v).size = (insert m k v).buckets.size

Proof state:
case h_2.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = false
h✝ : numBucketsForCapacity (m.size + 1) ≤ m.buckets.val.size
⊢ { size := m.size + 1,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    (List.map (fun x => x.toList.length)
        { size := m.size + 1,
                buckets :=
                  m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
                    (AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.buckets.val.toList).sum

Tactic:
refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_

Result:
case h_2.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = false
h✝ : numBucketsForCapacity (m.size + 1) ≤ m.buckets.val.size
w✝¹ w✝ : List (AssocList α β)
h₁ : m.buckets.val.toList = w✝¹ ++ m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val] :: w✝
left✝ : w✝¹.length = (mkIdx ⋯ (hash k).toUSize).val.toNat
eq :
  (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
          (AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList =
    w✝¹ ++ AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝
⊢ { size := m.size + 1,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    (List.map (fun x => x.toList.length)
        (w✝¹ ++ AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝)).sum

Proof state:
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = true
⊢ { size := m.size,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    { size := m.size,
          buckets :=
            m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
              (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.buckets.size

Tactic:
unfold Buckets.size

Result:
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = true
⊢ { size := m.size,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    (List.map (fun x => x.toList.length)
        { size := m.size,
                buckets :=
                  m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
                    (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat])
                    ⋯ }.buckets.val.toList).sum

Proof state:
case h_2.isTrue
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = false
h✝ : numBucketsForCapacity (m.size + 1) ≤ m.buckets.val.size
w✝¹ w✝ : List (AssocList α β)
h₁ : m.buckets.val.toList = w✝¹ ++ m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val] :: w✝
left✝ : w✝¹.length = (mkIdx ⋯ (hash k).toUSize).val.toNat
eq :
  (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
          (AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList =
    w✝¹ ++ AssocList.cons k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝
⊢ (List.map (fun x => x.toList.length) w✝¹).sum +
        (m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat].toList.length +
          (List.map (fun x => x.toList.length) w✝).sum) +
      1 =
    (List.map (fun x => x.toList.length) w✝¹).sum +
      (m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat].toList.length +
          (List.map (fun x => x.toList.length) w✝).sum +
        1)

Tactic:
rfl

Result:
no goals

Proof state:
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = true
⊢ { size := m.size,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    (List.map (fun x => x.toList.length)
        { size := m.size,
                buckets :=
                  m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
                    (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat])
                    ⋯ }.buckets.val.toList).sum

Tactic:
refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_

Result:
case h_1
α : Type u_1
β : Type u_2
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
v : β
h : m.size = m.buckets.size
c✝ : Bool
heq✝ : AssocList.contains k m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] = true
w✝¹ w✝ : List (AssocList α β)
h₁ : m.buckets.val.toList = w✝¹ ++ m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val] :: w✝
left✝ : w✝¹.length = (mkIdx ⋯ (hash k).toUSize).val.toNat
eq :
  (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
          (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList =
    w✝¹ ++ AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝
⊢ { size := m.size,
        buckets :=
          m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
            (AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯ }.size =
    (List.map (fun x => x.toList.length)
        (w✝¹ ++ AssocList.replace k v m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝)).sum