Theorem: rcmDeriv.det (Ray/Hartogs/FubiniBall.lean)

State before:
x : ℝ × ℝ
⊢ (rcmDeriv x).det = x.1
Tactic:
rw [ContinuousLinearMap.det, ← LinearMap.det_toMatrix (Basis.finTwoProd ℝ), ←rcmMatrix]
State after:
x : ℝ × ℝ
⊢ (rcmMatrix x).det = x.1

State before:
x : ℝ × ℝ
⊢ (rcmMatrix x).det = x.1
Tactic:
rw [Matrix.det_fin_two, rcm00, rcm01, rcm10, rcm11]
State after:
x : ℝ × ℝ
⊢ x.2.cos * (x.1 * x.2.cos) - -x.1 * x.2.sin * x.2.sin = x.1

State before:
x : ℝ × ℝ
⊢ x.2.cos * (x.1 * x.2.cos) - -x.1 * x.2.sin * x.2.sin = x.1
Tactic:
ring_nf
State after:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1

State before:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1
Tactic:
calc cos x.2 ^ 2 * x.1 + x.1 * sin x.2 ^ 2
  _ = x.1 * (cos x.2 ^ 2 + sin x.2 ^ 2) := by ring
  _ = x.1 := by simp only [Real.cos_sq_add_sin_sq, mul_one]
State after:
no goals

State before:
x : ℝ × ℝ
⊢ x.2.cos ^ 2 * x.1 + x.1 * x.2.sin ^ 2 = x.1 * (x.2.cos ^ 2 + x.2.sin ^ 2)
Tactic:
ring
State after:
no goals

State before:
x : ℝ × ℝ
⊢ x.1 * (x.2.cos ^ 2 + x.2.sin ^ 2) = x.1
Tactic:
simp only [Real.cos_sq_add_sin_sq, mul_one]
State after:
no goals