After `set N := e`, rw with a lemma about `e` misses `N`; restate the lemma with `have` (defeq)

With set N := cross (b - a) (c - a) in context, rw [inner_cross_sub] at key (a lemma whose LHS is ⟪a, cross (b - a) (c - a)⟫) fails on ⟪a, N⟫: rw matches syntactically and does not unfold the local definition. Also, after simp only [...] at key the terms may already be in a different order than you expect, so rewriting real_inner_comm C a can fail just because key already has ⟪C, a⟫. Read the actual hypothesis in the error message. Robust fix: have hdet : ⟪a, N⟫ = ⟪a, cross b c⟫ := inner_cross_sub a b c (this typechecks by defeq), then rw [hdet] at key. Related: to swap the arguments of an inner product inside nlinarith, pass real_inner_comm N C as a hint instead of rewriting.