-- 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))
⊢ 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))

Tactic:
refine ih.trans ?_

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))
⊢ 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) target✝ (flatMap AssocList.toList (drop source target.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))
⊢ 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) target✝ (flatMap AssocList.toList (drop source target.toList))

Tactic:
simp only [Array.get_eq_getElem, AssocList.foldl_eq, Array.toList_set]

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))
⊢ 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))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
hi : ¬i < source.size
⊢ source.toList.length ≤ i

Tactic:
rwa [Array.size_eq_length_toList, Nat.not_lt] at hi

Result:
no goals

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) newSource newTarget =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) newTarget
      (flatMap AssocList.toList (drop (source + 1) newSource.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:
simp only [newSource, newTarget, es] at *

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 target target✝ =
    foldl (fun acc p => reinsertAux hash acc p.fst p.snd) target✝ (flatMap AssocList.toList (drop source target.toList))

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
hi : ¬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:
rw [expand.go_neg hi, List.drop_eq_nil_of_le, flatMap_nil, foldl_nil]

Result:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : PartialEquivBEq α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
hi : ¬i < source.size
⊢ source.toList.length ≤ i

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))
⊢ source < source + 1

Tactic:
omega

Result:
no goals