-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1)
    {a : α} {f : Option (β a) → Option (β a)} :
    Perm (toListModel (m.alterₘ a f).1.2) (alterKey a f (toListModel m.1.2))

Proof state:
case h_2
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
heq✝ : f none = some b✝
⊢ toListModel (m.consₘ a b✝).expandIfNecessary.val.buckets ~
    match f none with
    | none => eraseKey a (toListModel m.val.buckets)
    | some v => insertEntry a v (toListModel m.val.buckets)

Tactic:
next hs =>
simp only [hs]
refine Perm.trans (toListModel_expandIfNecessary _) ?_
refine Perm.trans (toListModel_consₘ m h _ _) ?_
rw [insertEntry_of_containsKey_eq_false]
exact hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel
      (if h : m.containsₘ a = true then
            let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l;
            let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
            ⟨{ size := size', buckets := buckets' }, ⋯⟩
          else
            match f none with
            | none => m
            | some b => (m.consₘ a b).expandIfNecessary).val.buckets ~
    alterKey a f (toListModel m.val.buckets)

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h✝ : m.containsₘ a = true
⊢ toListModel
      (let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l;
          let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
          ⟨{ size := size', buckets := buckets' }, ⋯⟩).val.buckets ~
    alterKey a f (toListModel m.val.buckets)

case isFalse
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
h✝ : ¬m.containsₘ a = true
⊢ toListModel
      (match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.buckets ~
    alterKey a f (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
hs : f none = some b✝
⊢ toListModel (m.consₘ a b✝).expandIfNecessary.val.buckets ~
    match f none with
    | none => eraseKey a (toListModel m.val.buckets)
    | some v => insertEntry a v (toListModel m.val.buckets)

Tactic:
simp only [hs]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
hs : f none = some b✝
⊢ toListModel (m.consₘ a b✝).expandIfNecessary.val.buckets ~ insertEntry a b✝ (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
hs : f none = some b✝
⊢ containsKey a (toListModel m.val.buckets) = false

Tactic:
exact hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
hn : f none = none
⊢ toListModel m.val.buckets ~
    match f none with
    | none => eraseKey a (toListModel m.val.buckets)
    | some v => insertEntry a v (toListModel m.val.buckets)

Tactic:
simp only [hn]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
hn : f none = none
⊢ toListModel m.val.buckets ~ eraseKey a (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel (m.alterₘ a f).val.buckets ~ alterKey a f (toListModel m.val.buckets)

Tactic:
rw [alterₘ]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ toListModel
      (if h : m.containsₘ a = true then
            let buckets' := updateBucket m.val.buckets ⋯ a fun l => AssocList.alter a f l;
            let size' := if containsₘ ⟨withComputedSize buckets', ⋯⟩ a = true then m.val.size else m.val.size - 1;
            ⟨{ size := size', buckets := buckets' }, ⋯⟩
          else
            match f none with
            | none => m
            | some b => (m.consₘ a b).expandIfNecessary).val.buckets ~
    alterKey a f (toListModel m.val.buckets)

Proof state:
case h_1
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
heq✝ : f none = none
⊢ toListModel m.val.buckets ~
    match f none with
    | none => eraseKey a (toListModel m.val.buckets)
    | some v => insertEntry a v (toListModel m.val.buckets)

Tactic:
next hn =>
simp only [hn]
rw [eraseKey_of_containsKey_eq_false]
exact hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
hn : f none = none
⊢ containsKey a (toListModel m.val.buckets) = false

Tactic:
exact hc

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
hs : f none = some b✝
⊢ toListModel (m.consₘ a b✝).expandIfNecessary.val.buckets ~ insertEntry a b✝ (toListModel m.val.buckets)

Tactic:
refine Perm.trans (toListModel_expandIfNecessary _) ?_

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
x✝ : Option (β a)
b✝ : β a
hs : f none = some b✝
⊢ toListModel (m.consₘ a b✝).val.buckets ~ insertEntry a b✝ (toListModel m.val.buckets)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : ¬m.containsₘ a = true
⊢ toListModel
      (match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.buckets ~
    alterKey a f (toListModel m.val.buckets)

Tactic:
rw [Bool.not_eq_true, containsₘ_eq_containsKey h] at hc

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
hc : containsKey a (toListModel m.val.buckets) = false
⊢ toListModel
      (match f none with
          | none => m
          | some b => (m.consₘ a b).expandIfNecessary).val.buckets ~
    alterKey a f (toListModel m.val.buckets)