Module: Mathlib.Analysis.Complex.Poisson

Goal state before:
pp: R φ θ r : ℝ
⊢ ↑R * cexp (↑θ * I) / (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I)) -
      ↑r * cexp (↑θ * I) / (↑r * cexp (↑θ * I) - ↑R * cexp (↑φ * I)) =
    ↑((↑R * cexp (↑θ * I) + ↑r * cexp (↑φ * I)) / (↑R * cexp (↑θ * I) - ↑r * cexp (↑φ * I))).re

Tactic:
simp only [Complex.ext_iff, exp_ofReal_mul_I, add_re, sub_re, mul_re, div_re, ofReal_re,
    I_re, I_im, add_im, sub_im, mul_im, div_im, ofReal_im, normSq_apply]

Goal state after:
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