calc
  _ = (f n * (cexp ((2 * π * -(y * (1 / (2 * π) * Real.log (n / x)))) * I) / ↑((n : ℝ) ^ σ'))) • ψ y := by
    have : ((↑n : ℂ) ^ (σ' : ℂ) : ℂ) = ((↑n : ℝ) ^ (σ' : ℝ) : ℝ) := by
      rw [Complex.cpow_def_of_ne_zero (by simp [hn]), Real.rpow_def_of_nonneg (Nat.cast_nonneg n)]
      simp [hn]
    simp [Real.fourierChar, expMapCircle, smul_eq_mul, mul_assoc, this] ; ring
  _ = (f n * (x ^ (y * I) / n ^ (σ' + y * I))) • ψ y := by
    congr 2
    have l1 : 0 < (n : ℝ) := by simpa using Nat.pos_iff_ne_zero.mpr hn
    have l2 : (x : ℂ) ≠ 0 := by simp [hx.ne.symm]
    have l3 : (n : ℂ) ≠ 0 := by simp [hn]
    rw [Real.rpow_def_of_pos l1, Complex.cpow_def_of_ne_zero l2, Complex.cpow_def_of_ne_zero l3]
    push_cast
    simp_rw [← Complex.exp_sub]
    congr 1
    rw [first_fourier_aux2a, Real.log_div l1.ne.symm hx.ne.symm]
    push_cast
    rw [Complex.ofReal_log hx.le]
    ring
  _ = _ := by simp ; group
case neg
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hx : 0 < x
n : ℕ
hn : ¬n = 0
⊢ f n / ↑n ^ ↑σ' * 𝐞 (-(y * (1 / (2 * π) * (↑n / x).log))) • ψ y = (f n / ↑n ^ (↑σ' + ↑y * I)) • (ψ y * ↑x ^ (↑y * I))
no goals