-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.HurwitzZetaEven (goal)
Goal:
x : ℝ
hx : 0 < x
a : ℝ
h1 : I * (↑(1 / x) : ℂ) = -1 / (I * (↑x : ℂ))
hx' : I * (↑x : ℂ) ≠ 0
h2 : (↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ)) = (↑a : ℂ)
h3 : 1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) = 1 / (↑(x ^ (1 / 2)) : ℂ)
h4 :
  -(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ)) =
    -(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))
inr :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₁ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₂ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₃ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
        jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₄ :
  cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
        (1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₅ :
  1 / (↑(x ^ (1 / 2)) : ℂ) * cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
        cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₆ :
  1 / (↑(x ^ (1 / 2)) : ℂ) *
        (cexp (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
          cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ))) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
inr₇ :
  1 / (↑(x ^ (1 / 2)) : ℂ) *
        cexp
          (-(-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) +
            -(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
⊢ cexp (-(↑π : ℂ) * HPow.hPow (β := ℕ) (↑a : ℂ) 2 * (↑x : ℂ)) *
      (1 / (-I * (I * (↑x : ℂ))) ^ (1 / 2) *
          cexp (-(↑π : ℂ) * I * HPow.hPow (β := ℕ) ((↑a : ℂ) * I * (↑x : ℂ)) 2 / (I * (↑x : ℂ))) *
        jacobiTheta₂ ((↑a : ℂ) * I * (↑x : ℂ) / (I * (↑x : ℂ))) (-1 / (I * (↑x : ℂ)))) =
    (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (I * (↑(1 / x) : ℂ))
have inr₈ : 1 / (↑(x ^ (1 / 2)) : ℂ) * cexp 0 * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ))) =
  (↑(1 / x ^ (1 / 2)) : ℂ) * jacobiTheta₂ (↑a : ℂ) (-1 / (I * (↑x : ℂ)))
Tactic: rw [h1, h2, h3, h4, ← mul_assoc, mul_comm (cexp _), mul_assoc _ (cexp _) (cexp _),
    ← Complex.exp_add, neg_add_cancel, Complex.exp_zero, mul_one, ofReal_div, ofReal_one]