α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) buckets.val.data) +
      Bucket.size (Bucket.mk (Array.size buckets.val * 2)) =
    Bucket.size buckets

case hs
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ ∀ (j : Nat), j < 0 → List.getD buckets.val.data j AssocList.nil = AssocList.nil
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ Bucket.size (expand sz buckets).buckets = Bucket.size buckets
rw [expand, go]
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) buckets.val.data) + 0 = Bucket.size buckets
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) buckets.val.data) +
      Bucket.size (Bucket.mk (Array.size buckets.val * 2)) =
    Bucket.size buckets
rw [Bucket.mk_size]
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) buckets.val.data) + 0 = Bucket.size buckets
simp [Bucket.size]
no goals
case hs
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
⊢ ∀ (j : Nat), j < 0 → List.getD buckets.val.data j AssocList.nil = AssocList.nil
intro.
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
⊢ Bucket.size
      (if h : i < Array.size source then
        let idx := { val := i, isLt := h };
        let es := Array.get source idx;
        let source := Array.set source idx AssocList.nil;
        let target := AssocList.foldl reinsertAux target es;
        expand.go (i + 1) source target
      else target) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
⊢ Bucket.size (expand.go i source target) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
unfold expand.go
case inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
h✝ : i < Array.size source
⊢ Bucket.size
      (let idx := { val := i, isLt := h✝ };
      let es := Array.get source idx;
      let source := Array.set source idx AssocList.nil;
      let target := AssocList.foldl reinsertAux target es;
      expand.go (i + 1) source target) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target

case inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
h✝ : ¬i < Array.size source
⊢ Bucket.size target = Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
⊢ Bucket.size
      (if h : i < Array.size source then
        let idx := { val := i, isLt := h };
        let es := Array.get source idx;
        let source := Array.set source idx AssocList.nil;
        let target := AssocList.foldl reinsertAux target es;
        expand.go (i + 1) source target
      else target) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
split
case a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
⊢ List.getD (List.set source.data i AssocList.nil) j AssocList.nil = AssocList.nil

case b
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.set source.data i AssocList.nil)) +
      Bucket.size (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
⊢ Bucket.size
      (let idx := { val := i, isLt := H };
      let es := Array.get source idx;
      let source := Array.set source idx AssocList.nil;
      let target := AssocList.foldl reinsertAux target es;
      expand.go (i + 1) source target) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
⊢ Option.getD (if i = j then Option.map (fun x => AssocList.nil) (List.get? source.data j) else List.get? source.data j)
      AssocList.nil =
    AssocList.nil
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
⊢ List.getD (List.set source.data i AssocList.nil) j AssocList.nil = AssocList.nil
simp [List.getD_eq_get?, List.get?_set]
case inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
h✝ : i = j
⊢ Option.getD (Option.map (fun x => AssocList.nil) (List.get? source.data j)) AssocList.nil = AssocList.nil

case inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
h✝ : ¬i = j
⊢ Option.getD (List.get? source.data j) AssocList.nil = AssocList.nil
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
⊢ Option.getD (if i = j then Option.map (fun x => AssocList.nil) (List.get? source.data j) else List.get? source.data j)
      AssocList.nil =
    AssocList.nil
split
no goals
case inl
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
h✝ : i = j
⊢ Option.getD (Option.map (fun x => AssocList.nil) (List.get? source.data j)) AssocList.nil = AssocList.nil
cases List.get? .. <;> rfl
no goals
case inr
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
j : Nat
hj : j < i + 1
h✝ : ¬i = j
⊢ Option.getD (List.get? source.data j) AssocList.nil = AssocList.nil
next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H✝ : i < Array.size source
j : Nat
hj : j < i + 1
H : ¬i = j
⊢ Option.getD (List.get? source.data j) AssocList.nil = AssocList.nil
exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H))
no goals
case b
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.set source.data i AssocList.nil)) +
      Bucket.size (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
case b =>
refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set' H; eq ▸ ?_
simp [h₁, Bucket.size_eq]
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1
(conv => rhs; rw [Nat.add_left_comm]); congr 1
rw [← Array.getElem_eq_data_get]
have := @reinsertAux_size α β _; simp [Bucket.size] at this
induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (l₁ ++ AssocList.nil :: l₂)) +
      Bucket.size (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.set source.data i AssocList.nil)) +
      Bucket.size (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set' H; eq ▸ ?_
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (l₁ ++ AssocList.nil :: l₂)) +
      Bucket.size (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
simp [h₁, Bucket.size_eq]
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
        Nat.sum
          (List.map (fun x => List.length (AssocList.toList x))
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data)) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
        (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)))
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
        (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂)) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
        Nat.sum
          (List.map (fun x => List.length (AssocList.toList x))
            (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data)) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₁) +
      (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
        (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
          Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)))
congr 1
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
(conv => rhs; rw [Nat.add_left_comm])
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
congr 1
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
rw [← Array.getElem_eq_data_get]
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this : ∀ (data : Bucket α β) (a : α) (b : β), Bucket.size (reinsertAux data a b) = Nat.succ (Bucket.size data)
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
have := @reinsertAux_size α β _
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this :
  ∀ (data : Bucket α β) (a : α) (b : β),
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (reinsertAux data a b).val.data) =
      Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this : ∀ (data : Bucket α β) (a : α) (b : β), Bucket.size (reinsertAux data a b) = Nat.succ (Bucket.size data)
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
simp [Bucket.size] at this
case e_a.e_a.cons
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this :
  ∀ (data : Bucket α β) (a : α) (b : β),
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (reinsertAux data a b).val.data) =
      Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
head✝ : α × β
tail✝ : List (α × β)
tail_ih✝ :
  ∀ (target : Bucket α β),
    Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.data) =
      List.length tail✝ + Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
target : Bucket α β
⊢ List.length tail✝ + Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)) =
    Nat.succ (List.length tail✝ + Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
case e_a.e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this :
  ∀ (data : Bucket α β) (a : α) (b : β),
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (reinsertAux data a b).val.data) =
      Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
⊢ Nat.sum
      (List.map (fun x => List.length (AssocList.toList x))
        (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList source[i]) +
      Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]
no goals
case e_a.e_a.cons
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
this :
  ∀ (data : Bucket α β) (a : α) (b : β),
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (reinsertAux data a b).val.data) =
      Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) data.val.data))
head✝ : α × β
tail✝ : List (α × β)
tail_ih✝ :
  ∀ (target : Bucket α β),
    Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target tail✝).val.data) =
      List.length tail✝ + Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)
target : Bucket α β
⊢ List.length tail✝ + Nat.succ (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data)) =
    Nat.succ (List.length tail✝ + Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
rfl
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      (List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
case e_a
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : i < Array.size source
l₁ l₂ : List (AssocList α β)
h₁ : source.data = l₁ ++ List.get source.data { val := i, isLt := H } :: l₂
left✝ : List.length l₁ = i
eq : List.set source.data i AssocList.nil = l₁ ++ AssocList.nil :: l₂
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
      Nat.sum
        (List.map (fun x => List.length (AssocList.toList x))
          (List.foldl (fun d x => reinsertAux d x.fst x.snd) target (AssocList.toList source[i])).val.data) =
    List.length (AssocList.toList (List.get source.data { val := i, isLt := H })) +
      (Nat.sum (List.map (fun x => List.length (AssocList.toList x)) l₂) +
        Nat.sum (List.map (fun x => List.length (AssocList.toList x)) target.val.data))
conv => rhs; rw [Nat.add_left_comm]
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) = 0
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Bucket.size target = Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) + Bucket.size target
rw [(_ : Nat.sum _ = 0), Nat.zero_add]
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.map (fun x => AssocList.nil) source.data)) = 0

α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ List.map (fun x => AssocList.nil) source.data = source.data
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) source.data) = 0
rw [← (_ : source.data.map (fun _ => .nil) = source.data)]
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
⊢ List.get (List.map (fun x => AssocList.nil) source.data) { val := j, isLt := h₁ } =
    List.get source.data { val := j, isLt := h₂ }
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ List.map (fun x => AssocList.nil) source.data = source.data
refine List.ext_get (by simp) fun j h₁ h₂ => ?_
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
⊢ AssocList.nil = List.get source.data { val := j, isLt := h₂ }
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
⊢ List.get (List.map (fun x => AssocList.nil) source.data) { val := j, isLt := h₁ } =
    List.get source.data { val := j, isLt := h₂ }
simp
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
this : AssocList.nil = List.getD source.data j AssocList.nil
⊢ AssocList.nil = List.get source.data { val := j, isLt := h₂ }
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
⊢ AssocList.nil = List.get source.data { val := j, isLt := h₂ }
have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
j : Nat
h₁ : j < List.length (List.map (fun x => AssocList.nil) source.data)
h₂ : j < List.length source.data
this : AssocList.nil = List.getD source.data j AssocList.nil
⊢ AssocList.nil = List.get source.data { val := j, isLt := h₂ }
rwa [List.getD_eq_get?, List.get?_eq_get, Option.getD_some] at this
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map ((fun x => List.length (AssocList.toList x)) ∘ fun x => AssocList.nil) source.data) = 0
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map (fun x => List.length (AssocList.toList x)) (List.map (fun x => AssocList.nil) source.data)) = 0
simp
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ Nat.sum (List.map ((fun x => List.length (AssocList.toList x)) ∘ fun x => AssocList.nil) source.data) = 0
induction source.data <;> simp [*]
no goals
α : Type u_1
β : Type u_2
sz : Nat
inst✝ : Hashable α
buckets : Bucket α β
i : Nat
source : Array (AssocList α β)
target : Bucket α β
hs : ∀ (j : Nat), j < i → List.getD source.data j AssocList.nil = AssocList.nil
H : ¬i < Array.size source
⊢ List.length (List.map (fun x => AssocList.nil) source.data) = List.length source.data
simp