-- Lean 4 proof step from Mathlib.Analysis.Complex.Poisson (goal)
Goal:
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 :
      ℂ)
have simp : (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: 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]