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

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