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

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

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

Result:
case cons
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : α
tl : List α
ih :
  ∀ {m : Raw₀ α fun x => Unit},
    Raw.WFImp m.val →
      toListModel (insertListIfNewUnitₘ m tl).val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) tl
m : Raw₀ α fun x => Unit
h : Raw.WFImp m.val
⊢ insertListIfNewUnit (toListModel (m.insertIfNew hd ()).val.buckets) tl ~
    insertListIfNewUnit (insertEntryIfNew hd () (toListModel m.val.buckets)) tl

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

Tactic:
simp only [insertListIfNewUnitₘ, insertListIfNewUnit]

Result:
case cons
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : α
tl : List α
ih :
  ∀ {m : Raw₀ α fun x => Unit},
    Raw.WFImp m.val →
      toListModel (insertListIfNewUnitₘ m tl).val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) tl
m : Raw₀ α fun x => Unit
h : Raw.WFImp m.val
⊢ toListModel (insertListIfNewUnitₘ (m.insertIfNew hd ()) tl).val.buckets ~
    insertListIfNewUnit (insertEntryIfNew hd () (toListModel m.val.buckets)) tl

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

Tactic:
apply (wfImp_insertIfNew h).distinct

Result:
no goals

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

Tactic:
induction l generalizing m with
| nil => simp [insertListIfNewUnitₘ, List.insertListIfNewUnit]
| cons hd tl ih =>
  simp only [insertListIfNewUnitₘ, insertListIfNewUnit]
  apply Perm.trans (ih (wfImp_insertIfNew h))
  apply List.insertListIfNewUnit_perm_of_perm_first (toListModel_insertIfNew h)
  apply (wfImp_insertIfNew h).distinct

Result:
no goals

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

Tactic:
apply List.insertListIfNewUnit_perm_of_perm_first (toListModel_insertIfNew h)

Result:
case cons
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
hd : α
tl : List α
ih :
  ∀ {m : Raw₀ α fun x => Unit},
    Raw.WFImp m.val →
      toListModel (insertListIfNewUnitₘ m tl).val.buckets ~ insertListIfNewUnit (toListModel m.val.buckets) tl
m : Raw₀ α fun x => Unit
h : Raw.WFImp m.val
⊢ DistinctKeys (toListModel (m.insertIfNew hd ()).val.buckets)

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

Tactic:
simp [insertListIfNewUnitₘ, List.insertListIfNewUnit]

Result:
no goals