simp
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x =>
      let s := -sin x;
      let c := cos x;
      sqrt
        (((fun yz =>
              let x₁ := s * yz.1;
              let x₂ := c * yz.2;
              x₁ + x₂) ∘
            fun dx => (dx * s, dx * c))
          1)) =
    1
R : Type
inst✝² : RealScalar R
inst✝¹ : MeasureSpace R
inst✝ : PlainDataType R
⊢ (fun x => sqrt (sin x * sin x + cos x * cos x)) = 1