induction i with
| head =>
  rw [sublist_pos_head]
  rw [unsublist_pos_head]
| @tail xs x i ih =>
  by_cases p x with
  | isTrue hh =>
    rw [sublist_pos_tail hh]
    rw [unsublist_pos_tail hh]
    rw [ih]
  | isFalse hh =>
    rw [sublist_neg_tail hh]
    rw [unsublist_neg_tail hh]
    rw [ih]
α : Type u_1
p✝ : α → Prop
inst✝¹ : DecidablePred p✝
p : α → Prop
inst✝ : DecidablePred p
xs : List α
i : xs.Index
hi : p i.val
⊢ unsublist p (sublist p i hi) = i
no goals