Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R φ θ r : ℝ
⊢ (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) +
          (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1))) *
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) -
        ((r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0))) *
              (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) +
          (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1))) *
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))))) =
      (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) +
              (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
            (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
              (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) /
          ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
            (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) +
        (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) +
              (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
            (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
              (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) /
          ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
            (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) ∧
    (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1))) *
              (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) -
          (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0))) *
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) /
            ((R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (R * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (r * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (R * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (r * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) -
        ((r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1))) *
              (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1))))) -
          (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0))) *
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) /
            ((r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) *
                (r * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) - 0 * (0 + (Real.sin θ * 1 + 0 * 0)) -
                  (R * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)) - 0 * (0 + (Real.sin φ * 1 + 0 * 0)))) +
              (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))) *
                (r * (0 + (Real.sin θ * 1 + 0 * 0)) + 0 * (Real.cos θ + (Real.sin θ * 0 - 0 * 1)) -
                  (R * (0 + (Real.sin φ * 1 + 0 * 0)) + 0 * (Real.cos φ + (Real.sin φ * 0 - 0 * 1)))))) =
      0

Tactic:
grind [Real.sin_sq]

Goal state after: