rewrite and oangles interacting oddly

Stream: new members

[Riley Riles]

Hi! My proofstate currently has
```calceq : ↑π + 2 • ∡ C S K = 2 • ∡ C S B + ↑π
calc1 : 2 • ∡ C S B + ↑π = ↑π + 2 • ∡ C S B

and I attempted to run
```rewrite [calc1] at calceq```
but get the error message "tactic 'rewrite' failed, did not find instance of the pattern in the target expression
2 • ∡ C S B + ↑π." I am confused as to why this is; what am I missing?

Thank you in advance!

[Aaron Liu]

Can you provide a #mwe?

[Riley Riles]

When attempting to provide a minimum working example, the code spontaneously started working again. I'm not really sure why that happened but I guess I'll take it?

[Aaron Liu]

It might have been the types. Try doing set_option pp.numericTypes true