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

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
⊢ alter m a f = alterₘ m a f

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

Result:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
⊢ (if AssocList.contains a (bucket m.1.buckets ⋯ a) = true then
      ⟨{
          size :=
            if AssocList.contains a (AssocList.Const.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.Const.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.Const.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.Const.alter a f l },
        ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary

Proof state:
case isTrue.e_val.e_size
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (if AssocList.contains a (AssocList.Const.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.Const.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✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
⊢ (if AssocList.contains a (bucket m.1.buckets ⋯ a) = true then
      ⟨{
          size :=
            if AssocList.contains a (AssocList.Const.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.Const.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.Const.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.Const.alter a f l },
        ⋯⟩
    else
      match f none with
      | none => m
      | some b => (m.consₘ a b).expandIfNecessary

Tactic:
split

Result:
case isTrue
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.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.Const.alter a f (bucket m.1.buckets ⋯ a)) ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if
              AssocList.contains a
                  (bucket
                    (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.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.Const.alter a f l },
      ⋯⟩

case isFalse
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : ¬AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (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))
                ⋯ },
          ⋯⟩) =
    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✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.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.Const.alter a f (bucket m.1.buckets ⋯ a)) ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if
              AssocList.contains a
                  (bucket
                    (withComputedSize (updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.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.Const.alter a f l },
      ⋯⟩

Tactic:
congr 2

Result:
case isTrue.e_val.e_size
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
h✝ : AssocList.contains a (bucket m.1.buckets ⋯ a) = true
⊢ (if AssocList.contains a (AssocList.Const.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.Const.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✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : Option β → Option β
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.Const.alter a f (bucket m.1.buckets ⋯ a)) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.Const.alter a f l