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

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ (m.modify k f).size = (m.modify k f).buckets.size

Tactic:
dsimp [modify, cond]

Result:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ m.size =
    ((m.buckets.update (mkIdx ⋯ (hash k).toUSize).val AssocList.nil ⋯).update (mkIdx ⋯ (hash k).toUSize).val
        (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map (fun x => x.toList.length)
        (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
              (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList).sum

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

Result:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.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.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList =
    w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map (fun x => x.toList.length)
        (w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝)).sum

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ m.size =
    (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
        (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size

Tactic:
simp only [h, Buckets.size]

Result:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map (fun x => x.toList.length)
        (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
              (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList).sum

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ m.size =
    ((m.buckets.update (mkIdx ⋯ (hash k).toUSize).val AssocList.nil ⋯).update (mkIdx ⋯ (hash k).toUSize).val
        (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size

Tactic:
rw [Buckets.update_update]

Result:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.size
⊢ m.size =
    (m.buckets.update (mkIdx ⋯ (hash k).toUSize).val
        (AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).size

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
inst✝¹ : BEq α
inst✝ : Hashable α
m : Imp α β
k : α
h : m.size = m.buckets.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.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat]) ⋯).val.toList =
    w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝
⊢ (List.map (fun x => x.toList.length) m.buckets.val.toList).sum =
    (List.map (fun x => x.toList.length)
        (w✝¹ ++ AssocList.modify k f m.buckets.val[(mkIdx ⋯ (hash k).toUSize).val.toNat] :: w✝)).sum

Tactic:
simp [h, h₁, Buckets.size_eq]

Result:
no goals