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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (if AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true then
        (true,
          ⟨{ size := m.1.size,
              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.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
            ⋯⟩)
      else
        (false,
          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]) ⋯ },
              ⋯⟩)).snd =
    if AssocList.contains a m.val.buckets[(mkIdx m.val.buckets.size ⋯ (hash a)).val.toNat] = true then m.replaceₘ a b
    else (m.consₘ a b).expandIfNecessary

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (true,
        ⟨{ size := m.1.size,
            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.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
          ⋯⟩).snd =
    m.replaceₘ a b

case isFalse
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
h✝ : ¬AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (false,
        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]) ⋯ },
            ⋯⟩).snd =
    (m.consₘ a b).expandIfNecessary

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β 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.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.replace a b l

Tactic:
rw [Array.set_set, updateBucket]

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β 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.replace a b 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.replace a b m.val.buckets[i]) h

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
h✝ : AssocList.contains a m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat] = true
⊢ (true,
        ⟨{ size := m.1.size,
            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.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ },
          ⋯⟩).snd =
    m.replaceₘ a b

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

Result:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β 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.replace a b m.1.buckets[(mkIdx m.1.buckets.size ⋯ (hash a)).val.toNat]) ⋯ =
    updateBucket m.val.buckets ⋯ a fun l => AssocList.replace a b l

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.containsThenInsert a b).snd = m.insertₘ a b

Tactic:
rw [containsThenInsert, insertₘ, containsₘ, bucket]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β 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;
          (true, ⟨{ size := m.1.size, buckets := buckets'.uset i (AssocList.replace a b bkt) ⋯ }, ⋯⟩)
        else
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          (false, expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)).snd =
    if
        AssocList.contains a
            (match mkIdx m.val.buckets.size ⋯ (hash a) with
            | ⟨i, h⟩ => m.val.buckets[i]) =
          true then
      m.replaceₘ a b
    else (m.consₘ a b).expandIfNecessary

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β 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.replace a b 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.replace a b m.val.buckets[i]) h

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

Result:
no goals