-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_insertIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} :
    Perm (toListModel (m.insertIfNewₘ a b).1.buckets)
      (insertEntryIfNew a b (toListModel m.1.buckets))

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel
      (if containsKey a (toListModel m.val.buckets) = true then m else (m.consₘ a b).expandIfNecessary).val.buckets ~
    if containsKey a (toListModel m.val.buckets) = true then toListModel m.val.buckets
    else ⟨a, b⟩ :: toListModel m.val.buckets

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel m.val.buckets ~ toListModel m.val.buckets

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel m.val.buckets ~ toListModel m.val.buckets

Tactic:
next h' => exact Perm.refl _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : containsKey a (toListModel m.val.buckets) = true
⊢ toListModel m.val.buckets ~ toListModel m.val.buckets

Tactic:
exact Perm.refl _

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h' : ¬containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Tactic:
exact (toListModel_expandIfNecessary _).trans (toListModel_consₘ m h a b)

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel (m.insertIfNewₘ a b).val.buckets ~ insertEntryIfNew a b (toListModel m.val.buckets)

Tactic:
rw [insertIfNewₘ, insertEntryIfNew, containsₘ_eq_containsKey h, cond_eq_if]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ toListModel
      (if containsKey a (toListModel m.val.buckets) = true then m else (m.consₘ a b).expandIfNecessary).val.buckets ~
    if containsKey a (toListModel m.val.buckets) = true then toListModel m.val.buckets
    else ⟨a, b⟩ :: toListModel m.val.buckets

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬containsKey a (toListModel m.val.buckets) = true
⊢ toListModel (m.consₘ a b).expandIfNecessary.val.buckets ~ ⟨a, b⟩ :: toListModel m.val.buckets

Tactic:
next h' => exact (toListModel_expandIfNecessary _).trans (toListModel_consₘ m h a b)

Result:
no goals