refine Nat.fold'_induction
  (motive := fun (k : Nat) (bs : Array β) => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ as.size) (hbsk : bs.size = k), bs[j]'(hbsk ▸ hjk) = f (as[j]'(trans (r:=LT.lt (α:=Nat)) hjk hk)) (h j (trans (r:=LT.lt (α:=Nat)) hjk hk)))
  as.size _ #[] ?_ ?_ i (as.size_pmap f h ▸ hi) .refl ((as.pmap_eq_nat_fold'_push f h) ▸ as.size_pmap f h)
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (Nat.fold' (size as) (fun i x => push x (f as[i.val] (_ : p as[i.val]))) #[])[i] = f as[i] (_ : p as[i])
case refine_1
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) 0 #[]

case refine_2
α : Type u
β : Type v
p : α → Prop
f : (a : α) → p a → β
as : Array α
h : ∀ (i : Nat) (hi : i < size as), p as[i]
i : Nat
hi : i < size (pmap f as h)
⊢ ∀ (i : Nat) (hi : i < size as) (a : Array β),
    (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j])) i a →
      (fun k bs => ∀ (j : Nat) (hjk : j < k) (hk : k ≤ size as) (hbsk : size bs = k), bs[j] = f as[j] (_ : p as[j]))
        (i + 1) (push a (f as[{ val := i, isLt := hi }.val] (_ : p as[{ val := i, isLt := hi }.val])))