-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α)
    (f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f

Proof state:
case isTrue.e_val.e_size
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (if AssocList.contains a (AssocList.alter a f (bucket m.1.buckets ⋯ a)) = true then m.1.size else m.1.size - 1) =
    if
        AssocList.contains a
            (bucket (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l)).buckets ⋯ a) =
          true then
      m.val.size
    else m.val.size - 1

Tactic:
simp only [withComputedSize, bucket_updateBucket]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
⊢ m.alter a f = m.alterₘ a f

Tactic:
dsimp only [alter, alterₘ, containsₘ, ← bucket_eq]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
⊢ (if AssocList.contains a (bucket m.1.buckets ⋯ a) = true then
      ⟨{
          size :=
            if AssocList.contains a (AssocList.alter a f (bucket m.1.buckets ⋯ a)) = true then m.1.size
            else m.1.size - 1,
          buckets :=
            (m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val AssocList.nil ⋯).uset
              (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.alter a f (bucket m.1.buckets ⋯ a)) ⋯ },
        ⋯⟩
    else
      match f none with
      | none => m
      | some b =>
        expandIfNecessary
          ⟨{ size := m.1.size + 1,
              buckets :=
                m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.cons a b (bucket m.1.buckets ⋯ a))
                  ⋯ },
            ⋯⟩) =
    if h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true then
      ⟨{
          size :=
            if
                AssocList.contains a
                    (bucket (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l)).buckets ⋯
                      a) =
                  true then
              m.val.size
            else m.val.size - 1,
          buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l },
        ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ ⟨{
        size :=
          if AssocList.contains a (AssocList.alter a f (bucket m.1.buckets ⋯ a)) = true then m.1.size else m.1.size - 1,
        buckets :=
          (m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val AssocList.nil ⋯).uset
            (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.alter a f (bucket m.1.buckets ⋯ a)) ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if
              AssocList.contains a
                  (bucket (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l)).buckets ⋯
                    a) =
                true then
            m.val.size
          else m.val.size - 1,
        buckets := updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l },
      ⋯⟩

Tactic:
congr 2

Result:
case isTrue.e_val.e_size
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (if AssocList.contains a (AssocList.alter a f (bucket m.1.buckets ⋯ a)) = true then m.1.size else m.1.size - 1) =
    if
        AssocList.contains a
            (bucket (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l)).buckets ⋯ a) =
          true then
      m.val.size
    else m.val.size - 1

case isTrue.e_val.e_buckets
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val AssocList.nil ⋯).uset
      (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.alter a f (bucket m.1.buckets ⋯ a)) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l

Proof state:
case isTrue.e_val.e_buckets
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
f : Option (β a) → Option (β a)
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (m.1.buckets.uset (mkIdx m.1.buckets.size ⋯ (hash a)).val AssocList.nil ⋯).uset
      (mkIdx m.1.buckets.size ⋯ (hash a)).val (AssocList.alter a f (bucket m.1.buckets ⋯ a)) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l

Tactic:
simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket]

Result:
no goals