-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem getThenInsertIfNew?_eq_insertIfNewₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β)
    (a : α) (b : β a) : (m.getThenInsertIfNew? a b).2 = m.insertIfNewₘ a b

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (match AssocList.getCast? a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] with
      | none =>
        (none,
          expandIfNecessary
            ⟨{ size := m.1.size + 1,
                buckets :=
                  m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                    (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
              ⋯⟩)
      | some v => (some v, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)).snd =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m
    else (m.consₘ a b).expandIfNecessary

Tactic:
split <;> simp_all [consₘ, updateBucket, List.containsKey_eq_isSome_getValueCast?]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (m.getThenInsertIfNew? a b).snd = m.insertIfNewₘ a b

Tactic:
rw [getThenInsertIfNew?, insertIfNewₘ, containsₘ, bucket]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ =>
        let bkt := m.1.buckets[i];
        match AssocList.getCast? a bkt with
        | none =>
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (none, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
        | some v => (some v, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)).snd =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m
    else (m.consₘ a b).expandIfNecessary

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
      | ⟨i, h⟩ =>
        let bkt := m.1.buckets[i];
        match AssocList.getCast? a bkt with
        | none =>
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (none, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
        | some v => (some v, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)).snd =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m
    else (m.consₘ a b).expandIfNecessary

Tactic:
dsimp only [Array.ugetElem_eq_getElem, Array.uset]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
b : β a
⊢ (match AssocList.getCast? a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] with
      | none =>
        (none,
          expandIfNecessary
            ⟨{ size := m.1.size + 1,
                buckets :=
                  m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
                    (AssocList.cons a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
              ⋯⟩)
      | some v => (some v, ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩)).snd =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m
    else (m.consₘ a b).expandIfNecessary