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

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
⊢ (match mkIdx m.1.buckets.size ⋯ (hash a) with
    | ⟨i, hi⟩ =>
      let bucket := m.1.buckets[i];
      if AssocList.contains a bucket = true then
        let buckets := m.1.buckets.uset i AssocList.nil hi;
        let bucket := AssocList.Const.modify a f bucket;
        ⟨{ size := m.1.size, buckets := buckets.uset i bucket ⋯ }, ⋯⟩
      else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    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;
        let bkt' := AssocList.Const.alter a (fun x => Option.map f x) bkt;
        let size' := if AssocList.contains a bkt' = true then m.1.size else m.1.size - 1;
        ⟨{ size := size', buckets := buckets'.uset i bkt' ⋯ }, ⋯⟩
      else
        match Option.map f none with
        | none => ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
        | some b =>
          let size' := m.1.size + 1;
          let buckets' := m.1.buckets.uset i (AssocList.cons a b bkt) h;
          expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩

Tactic:
split

Result:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
⊢ (let bucket := m.1.buckets[i✝];
    if AssocList.contains a bucket = true then
      let buckets := m.1.buckets.uset i✝ AssocList.nil hi✝;
      let bucket := AssocList.Const.modify a f bucket;
      ⟨{ size := m.1.size, buckets := buckets.uset i✝ bucket ⋯ }, ⋯⟩
    else ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩) =
    let bkt := m.1.buckets[i✝];
    if AssocList.contains a bkt = true then
      let buckets' := m.1.buckets.uset i✝ AssocList.nil hi✝;
      let bkt' := AssocList.Const.alter a (fun x => Option.map f x) bkt;
      let size' := if AssocList.contains a bkt' = true then m.1.size else m.1.size - 1;
      ⟨{ size := size', buckets := buckets'.uset i✝ bkt' ⋯ }, ⋯⟩
    else
      match Option.map f none with
      | none => ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩
      | some b =>
        let size' := m.1.size + 1;
        let buckets' := m.1.buckets.uset i✝ (AssocList.cons a b bkt) hi✝;
        expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩

Proof state:
case isTrue
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
h✝ : AssocList.contains a m.1.buckets[i✝.toNat] = true
⊢ ⟨{ size := m.1.size,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat (AssocList.Const.modify a f m.1.buckets[i✝.toNat])
            ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) = true then
            m.1.size
          else m.1.size - 1,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat
            (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) ⋯ },
      ⋯⟩

Tactic:
next h =>
simp only [AssocList.contains_eq] at h
simp only [AssocList.Const.modify_eq_alter, Array.set_set, AssocList.contains_eq,
  containsKey_of_perm AssocList.Const.toList_alter, ← Const.modifyKey_eq_alterKey,
  Const.containsKey_modifyKey, h, reduceIte]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
h : AssocList.contains a m.1.buckets[i✝.toNat] = true
⊢ ⟨{ size := m.1.size,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat (AssocList.Const.modify a f m.1.buckets[i✝.toNat])
            ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) = true then
            m.1.size
          else m.1.size - 1,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat
            (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) ⋯ },
      ⋯⟩

Tactic:
simp only [AssocList.contains_eq] at h

Result:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
h : containsKey a m.1.buckets[i✝.toNat].toList = true
⊢ ⟨{ size := m.1.size,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat (AssocList.Const.modify a f m.1.buckets[i✝.toNat])
            ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) = true then
            m.1.size
          else m.1.size - 1,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat
            (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) ⋯ },
      ⋯⟩

Proof state:
case isFalse
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
h✝ : ¬AssocList.contains a m.1.buckets[i✝.toNat] = true
⊢ ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩ = ⟨{ size := m.1.size, buckets := m.1.buckets }, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : EquivBEq α
m : Raw₀ α fun x => β
a : α
f : β → β
x✝ : { u // u.toNat < m.1.buckets.size }
i✝ : USize
hi✝ : i✝.toNat < m.1.buckets.size
heq✝ : mkIdx m.1.buckets.size ⋯ (hash a) = ⟨i✝, hi✝⟩
h : containsKey a m.1.buckets[i✝.toNat].toList = true
⊢ ⟨{ size := m.1.size,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat (AssocList.Const.modify a f m.1.buckets[i✝.toNat])
            ⋯ },
      ⋯⟩ =
    ⟨{
        size :=
          if AssocList.contains a (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) = true then
            m.1.size
          else m.1.size - 1,
        buckets :=
          (m.1.buckets.set i✝.toNat AssocList.nil hi✝).set i✝.toNat
            (AssocList.Const.alter a (fun x => Option.map f x) m.1.buckets[i✝.toNat]) ⋯ },
      ⋯⟩

Tactic:
simp only [AssocList.Const.modify_eq_alter, Array.set_set, AssocList.contains_eq,
  containsKey_of_perm AssocList.Const.toList_alter, ← Const.modifyKey_eq_alterKey,
  Const.containsKey_modifyKey, h, reduceIte]

Result:
no goals