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

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