`change angle (vec _ - vec _) ...` with underscores picks a different syntactic form; spell the terms out

Proving facts about a concrete structure instance (Q := D.toPolyhedron hv, with fields defined via D), I used change angle (vec _ - vec _) (vec _ - vec _) = _ to expose the vectors. The holes were filled with Q.V (Q.F ...) forms, so later rw [e1] with hypotheses phrased via D.V (D.cidx ...) failed: 'did not find pattern; target not type-correct at implicit transparency'. The fix is to write the change target fully in the same vocabulary as the hypotheses (vec (D.V (D.cidx p.1 (prevIdx (D.n p.1) p.2))) - ...). After that, rw [← vec_subV] and rw [e1] match syntactically. Also: in this Mathlib, if_pos/if_neg are deprecated in favour of ite_eq_left/ite_eq_right as term proofs.