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

Proof state:
case nil
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ toListModel (m.insertListₘ []).val.buckets ~ insertList (toListModel m.val.buckets) []

Tactic:
simp [insertListₘ, List.insertList]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {m : Raw₀ α β},
    Raw.WFImp m.val → toListModel (m.insertListₘ tl).val.buckets ~ insertList (toListModel m.val.buckets) tl
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ toListModel (m.insertListₘ (hd :: tl)).val.buckets ~ insertList (toListModel m.val.buckets) (hd :: tl)

Tactic:
simp only [insertListₘ, List.insertList]

Result:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {m : Raw₀ α β},
    Raw.WFImp m.val → toListModel (m.insertListₘ tl).val.buckets ~ insertList (toListModel m.val.buckets) tl
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ toListModel ((m.insert hd.fst hd.snd).insertListₘ tl).val.buckets ~
    insertList (insertEntry hd.fst hd.snd (toListModel m.val.buckets)) tl

Proof state:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {m : Raw₀ α β},
    Raw.WFImp m.val → toListModel (m.insertListₘ tl).val.buckets ~ insertList (toListModel m.val.buckets) tl
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ insertList (toListModel (m.insert hd.fst hd.snd).val.buckets) tl ~
    insertList (insertEntry hd.fst hd.snd (toListModel m.val.buckets)) tl

Tactic:
apply List.insertList_perm_of_perm_first (toListModel_insert h) (wfImp_insert h).distinct

Result:
no goals

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

Tactic:
induction l generalizing m with
| nil =>
  simp [insertListₘ, List.insertList]
| cons hd tl ih =>
  simp only [insertListₘ, List.insertList]
  apply Perm.trans (ih (wfImp_insert h))
  apply List.insertList_perm_of_perm_first (toListModel_insert h) (wfImp_insert h).distinct

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {m : Raw₀ α β},
    Raw.WFImp m.val → toListModel (m.insertListₘ tl).val.buckets ~ insertList (toListModel m.val.buckets) tl
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ toListModel ((m.insert hd.fst hd.snd).insertListₘ tl).val.buckets ~
    insertList (insertEntry hd.fst hd.snd (toListModel m.val.buckets)) tl

Tactic:
apply Perm.trans (ih (wfImp_insert h))

Result:
case cons
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : (a : α) × β a
tl : List ((a : α) × β a)
ih :
  ∀ {m : Raw₀ α β},
    Raw.WFImp m.val → toListModel (m.insertListₘ tl).val.buckets ~ insertList (toListModel m.val.buckets) tl
m : Raw₀ α β
h : Raw.WFImp m.val
⊢ insertList (toListModel (m.insert hd.fst hd.snd).val.buckets) tl ~
    insertList (insertEntry hd.fst hd.snd (toListModel m.val.buckets)) tl