chore(analysis/inner_product_space): split slow proof (#15271)
This proof times out in the kernel at about 90 000 out of 100 000 heartbeats, and #14894 pushed it over the edge of timing out (except #15251 upped the timeout limits so everything sitll builds at the moment). I don't know enough about the kernel to debug why it doesn't like this proof, but splitting it into a `rw` part and a part that uses defeq seems to fix the timeout (moving it back down to about 60 000 out of 100 000 heartbeats).
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Timeout.20in.20the.20kernel/near/289294804
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
