cases Nat.eq_or_lt_of_le (Nat.le_of_succ_le_succ hj) with
| inl heq =>
  cases heq; exact get_push_eq ..
| inr hlt =>
  rewrite [bs.get_push_lt _ j hlt]
  exact IH j hlt (Nat.le_of_lt hk) rfl
case refine_2.refl
α : 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)
bs : Array β
j : Nat
hk : List.length bs.data < size as
IH :
  ∀ (j : Nat) (hjk : j < List.length bs.data) (hk : List.length bs.data ≤ size as)
    (hbsk : size bs = List.length bs.data), bs[j] = f as[j] (_ : p as[j])
hj : j < List.length bs.data + 1
hk✝ : List.length bs.data + 1 ≤ size as
hbsk :
  size
      (push bs
        (f as[{ val := List.length bs.data, isLt := hk }.val]
          (_ : p as[{ val := List.length bs.data, isLt := hk }.val]))) =
    List.length bs.data + 1
⊢ (push bs (f as[List.length bs.data] (_ : p as[{ val := List.length bs.data, isLt := hk }.val])))[j] =
    f as[j] (_ : p as[j])
no goals