-- 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:
α : 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

Tactic:
split

Result:
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 },
      ⋯⟩

case isFalse
α : 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
⊢ (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 isFalse
α : 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
⊢ (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

Tactic:
congr

Result:
no goals