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

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

Tactic:
unfold insertListConst

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

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

Tactic:
simp [Const.insertListₘ, insertListConst, insertList]

Result:
no goals

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

Tactic:
simp only [Const.insertListₘ, insertListConst]

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

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

Tactic:
induction l generalizing m with
| nil => simp [Const.insertListₘ, insertListConst, insertList]
| cons hd tl ih =>
  simp only [Const.insertListₘ, insertListConst]
  apply Perm.trans (ih (wfImp_insert h))
  unfold insertListConst
  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 : α × β
tl : List (α × β)
ih :
  ∀ {m : Raw₀ α fun x => β},
    Raw.WFImp m.val → toListModel (insertListₘ m tl).val.buckets ~ insertListConst (toListModel m.val.buckets) tl
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
⊢ insertList (toListModel (m.insert hd.fst hd.snd).val.buckets) (List.map Prod.toSigma tl) ~
    insertList (toListModel m.val.buckets) (List.map Prod.toSigma (hd :: tl))

Tactic:
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 : α × β
tl : List (α × β)
ih :
  ∀ {m : Raw₀ α fun x => β},
    Raw.WFImp m.val → toListModel (insertListₘ m tl).val.buckets ~ insertListConst (toListModel m.val.buckets) tl
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
⊢ toListModel (insertListₘ (m.insert hd.fst hd.snd) tl).val.buckets ~
    insertList (toListModel m.val.buckets) (List.map Prod.toSigma (hd :: 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 : α × β
tl : List (α × β)
ih :
  ∀ {m : Raw₀ α fun x => β},
    Raw.WFImp m.val → toListModel (insertListₘ m tl).val.buckets ~ insertListConst (toListModel m.val.buckets) tl
m : Raw₀ α fun x => β
h : Raw.WFImp m.val
⊢ insertListConst (toListModel (m.insert hd.fst hd.snd).val.buckets) tl ~
    insertList (toListModel m.val.buckets) (List.map Prod.toSigma (hd :: tl))