-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_foldl_reinsertAux [BEq α] [Hashable α] [PartialEquivBEq α]
    (l : List ((a : α) × β a)) (target : { d : Array (AssocList α β) // 0 < d.size }) :
    Perm (toListModel (l.foldl (fun acc p => reinsertAux hash acc p.1 p.2) target).1)
      (l ++ toListModel target.1)

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
l : List ((a : α) × β a)
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target l).val ~ l ++ toListModel target.val

Tactic:
induction l generalizing target

Result:
case nil
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target []).val ~ [] ++ toListModel target.val

case cons
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target tail✝).val ~
      tail✝ ++ toListModel target.val
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (head✝ :: tail✝)).val ~
    head✝ :: tail✝ ++ toListModel target.val

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : PartialEquivBEq α
v : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target t).val ~ t ++ toListModel target.val
target : { d // 0 < d.size }
⊢ t ++ toListModel (reinsertAux hash target v.fst v.snd).val ~ v :: (t ++ toListModel target.val)

Tactic:
refine ((toListModel_reinsertAux _ _ _).append_left _).trans perm_middle

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
head✝ : (a : α) × β a
tail✝ : List ((a : α) × β a)
tail_ih✝ :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target tail✝).val ~
      tail✝ ++ toListModel target.val
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (head✝ :: tail✝)).val ~
    head✝ :: tail✝ ++ toListModel target.val

Tactic:
next k v t ih =>
simp only [foldl_cons, cons_append]
refine (ih _).trans ?_
refine ((toListModel_reinsertAux _ _ _).append_left _).trans perm_middle

Result:
no goals

Proof state:
case nil
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target []).val ~ [] ++ toListModel target.val

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : PartialEquivBEq α
v : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target t).val ~ t ++ toListModel target.val
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) (reinsertAux hash target v.fst v.snd) t).val ~
    v :: (t ++ toListModel target.val)

Tactic:
refine (ih _).trans ?_

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : PartialEquivBEq α
v : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target t).val ~ t ++ toListModel target.val
target : { d // 0 < d.size }
⊢ t ++ toListModel (reinsertAux hash target v.fst v.snd).val ~ v :: (t ++ toListModel target.val)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : PartialEquivBEq α
v : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target t).val ~ t ++ toListModel target.val
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (v :: t)).val ~
    v :: t ++ toListModel target.val

Tactic:
simp only [foldl_cons, cons_append]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
k : PartialEquivBEq α
v : (a : α) × β a
t : List ((a : α) × β a)
ih :
  ∀ (target : { d // 0 < d.size }),
    toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target t).val ~ t ++ toListModel target.val
target : { d // 0 < d.size }
⊢ toListModel (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) (reinsertAux hash target v.fst v.snd) t).val ~
    v :: (t ++ toListModel target.val)