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

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i : PartialEquivBEq α
source : Nat
target : Array (AssocList α β)
target✝ : { d // 0 < d.size }
hi : source < target.size
es : AssocList α β := target[source]
newSource : Array (AssocList α β) := target.set source AssocList.nil hi
newTarget : { d // 0 < d.size } := AssocList.foldl (reinsertAux hash) target✝ es
ih :
  go (source + 1) (target.set source AssocList.nil hi) (AssocList.foldl (reinsertAux hash) target✝ target[source]) =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) (AssocList.foldl (reinsertAux hash) target✝ target[source])
      (flatMap AssocList.toList (drop (source + 1) (target.set source AssocList.nil hi).toList))
⊢ foldl (fun acc p => reinsertAux hash acc p.fst p.snd)
      (foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ target[source].toList)
      (flatMap AssocList.toList (drop (source + 1) (target.toList.set source AssocList.nil))) =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop source target.toList))

Tactic:
rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
  List.drop_set_of_lt _ _ (by omega), Array.getElem_toList]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
i : Nat
⊢ go i source target =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (flatMap AssocList.toList (drop i source.toList))

Tactic:
induction i, source, target using expand.go.induct

Result:
case case1
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i✝ : Nat
source✝¹ : Array (AssocList α β)
target✝¹ : { d // 0 < d.size }
h✝ : i✝ < source✝¹.size
es✝ : AssocList α β := source✝¹[i✝]
source✝ : Array (AssocList α β) := source✝¹.set i✝ AssocList.nil h✝
target✝ : { d // 0 < d.size } := AssocList.foldl (reinsertAux hash) target✝¹ es✝
ih1✝ :
  go (i✝ + 1) source✝ target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝
      (flatMap AssocList.toList (drop (i✝ + 1) source✝.toList))
⊢ go i✝ source✝¹ target✝¹ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝¹ (flatMap AssocList.toList (drop i✝ source✝¹.toList))

case case2
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i✝ : Nat
source✝ : Array (AssocList α β)
target✝ : { d // 0 < d.size }
h✝ : ¬i✝ < source✝.size
⊢ go i✝ source✝ target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop i✝ source✝.toList))

Proof state:
case case2
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i✝ : Nat
source✝ : Array (AssocList α β)
target✝ : { d // 0 < d.size }
h✝ : ¬i✝ < source✝.size
⊢ go i✝ source✝ target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop i✝ source✝.toList))

Tactic:
next i source target hi =>
rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil]
rwa [Array.size_eq_length_toList, Nat.not_lt] at hi

Result:
no goals

Proof state:
case case1
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i✝ : Nat
source✝¹ : Array (AssocList α β)
target✝¹ : { d // 0 < d.size }
h✝ : i✝ < source✝¹.size
es✝ : AssocList α β := source✝¹[i✝]
source✝ : Array (AssocList α β) := source✝¹.set i✝ AssocList.nil h✝
target✝ : { d // 0 < d.size } := AssocList.foldl (reinsertAux hash) target✝¹ es✝
ih1✝ :
  go (i✝ + 1) source✝ target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝
      (flatMap AssocList.toList (drop (i✝ + 1) source✝.toList))
⊢ go i✝ source✝¹ target✝¹ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝¹ (flatMap AssocList.toList (drop i✝ source✝¹.toList))

Tactic:
next i source target _ hi es newSource newTarget ih =>
simp only [newSource, newTarget, es] at *
rw [expand.go_pos hi]
refine ih.trans ?_
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]
rw [List.drop_eq_getElem_cons hi, List.flatMap_cons, List.foldl_append,
  List.drop_set_of_lt _ _ (by omega), Array.getElem_toList]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
⊢ ∀ (i : Nat),
    go i source target =
      foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (flatMap AssocList.toList (drop i source.toList))

Tactic:
intro i

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
source : Array (AssocList α β)
target : { d // 0 < d.size }
i : Nat
⊢ go i source target =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target (flatMap AssocList.toList (drop i source.toList))

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i : PartialEquivBEq α
source : Nat
target : Array (AssocList α β)
target✝ : { d // 0 < d.size }
hi : source < target.size
es : AssocList α β := target[source]
newSource : Array (AssocList α β) := target.set source AssocList.nil hi
newTarget : { d // 0 < d.size } := AssocList.foldl (reinsertAux hash) target✝ es
ih :
  go (source + 1) (target.set source AssocList.nil hi) (AssocList.foldl (reinsertAux hash) target✝ target[source]) =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) (AssocList.foldl (reinsertAux hash) target✝ target[source])
      (flatMap AssocList.toList (drop (source + 1) (target.set source AssocList.nil hi).toList))
⊢ go source target target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop source target.toList))

Tactic:
rw [expand.go_pos hi]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
i : PartialEquivBEq α
source : Nat
target : Array (AssocList α β)
target✝ : { d // 0 < d.size }
hi : source < target.size
es : AssocList α β := target[source]
newSource : Array (AssocList α β) := target.set source AssocList.nil hi
newTarget : { d // 0 < d.size } := AssocList.foldl (reinsertAux hash) target✝ es
ih :
  go (source + 1) (target.set source AssocList.nil hi) (AssocList.foldl (reinsertAux hash) target✝ target[source]) =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) (AssocList.foldl (reinsertAux hash) target✝ target[source])
      (flatMap AssocList.toList (drop (source + 1) (target.set source AssocList.nil hi).toList))
⊢ go (source + 1) (target.set source AssocList.nil hi) (AssocList.foldl (reinsertAux hash) target✝ target[source]) =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop source target.toList))