-- Module: Mathlib.Analysis.Complex.Poisson
Goal:
R φ θ r : ℝ
⊢ (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) - 0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) +
          (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1))) *
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) -
        ((r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0))) *
              (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) +
          (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1))) *
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))))) =
      (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
              (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
            (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
              (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) /
          ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
            (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) +
        (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) +
              (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
            (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
              (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) /
          ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
            (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) ∧
    (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) -
          (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0))) *
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (R * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (r * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) -
        ((r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1))) *
              (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1))))) -
          (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0))) *
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                  0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                    0 * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)))) +
              (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))) *
                (r * (0 + (Real.sin θ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos θ + (Real.sin θ * 0 - HMul.hMul (α := ℝ) 0 1)) -
                  (R * (0 + (Real.sin φ * 1 + HMul.hMul (α := ℝ) 0 0)) +
                    0 * (Real.cos φ + (Real.sin φ * 0 - HMul.hMul (α := ℝ) 0 1)))))) =
      0

Tactic:
grind [Real.sin_sq]

Premises used: Real.sin_sq