Theorem: rcm01 (Ray/Hartogs/FubiniBall.lean)

State before:
x : ℝ × ℝ
⊢ rcmMatrix x 0 1 = -x.1 * x.2.sin
Tactic:
simp [rcmMatrix, rcmDeriv, toMatrix_apply, d1, d2]
State after:
no goals