-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Model.lean
theorem erase_eq_eraseₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) :
    m.erase a = m.eraseₘ a

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
      (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
      (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.erase a l

Tactic:
rw [Array.set_set, updateBucket]

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
      (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    match mkIdx m.val.buckets.size ⋯ (hash a) with
    | ⟨i, h⟩ => m.val.buckets.uset i (AssocList.erase a m.val.buckets[i]) h

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ ⟨{ size := m.1.size - 1,
        buckets :=
          (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
            (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
            (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
      ⋯⟩ =
    m.eraseₘaux a

Tactic:
simp only [eraseₘaux, Subtype.mk.injEq, Raw.mk.injEq, true_and]

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
      (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
      (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.erase a l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
      ⟨{ size := m.1.size - 1,
          buckets :=
            (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
              (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
              (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
        ⋯⟩
    else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m.eraseₘaux a
    else m

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ ⟨{ size := m.1.size - 1,
        buckets :=
          (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
            (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
            (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
      ⋯⟩ =
    m.eraseₘaux a

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : ¬AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩ = m

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : ¬AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩ = m

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ m.erase a = m.eraseₘ a

Tactic:
rw [erase, eraseₘ, containsₘ, bucket]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
    | ⟨i, h⟩ =>
      let bkt := m.1.buckets[i];
      if AssocList.contains a bkt = true then
        let buckets' := m.1.buckets.uset i AssocList.nil h;
        ⟨{ size := m.1.size - 1, buckets := buckets'.uset i (AssocList.erase a bkt) ⋯ }, ⋯⟩
      else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m.eraseₘaux a
    else m

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
      (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    match mkIdx m.val.buckets.size ⋯ (hash a) with
    | ⟨i, h⟩ => m.val.buckets.uset i (AssocList.erase a m.val.buckets[i]) h

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

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
    | ⟨i, h⟩ =>
      let bkt := m.1.buckets[i];
      if AssocList.contains a bkt = true then
        let buckets' := m.1.buckets.uset i AssocList.nil h;
        ⟨{ size := m.1.size - 1, buckets := buckets'.uset i (AssocList.erase a bkt) ⋯ }, ⋯⟩
      else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m.eraseₘaux a
    else m

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

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
      ⟨{ size := m.1.size - 1,
          buckets :=
            (m.1.buckets.set (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat AssocList.nil ⋯).set
              (mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat
              (AssocList.erase a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
        ⋯⟩
    else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m.eraseₘaux a
    else m