refine congrArg₂ _ ?_ rfl
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k * ‖𝓕 (fun x => x ^ n • f x) ξ‖ = ‖(2 * ↑π * I * ↑ξ) ^ k‖ * ‖𝓕 (fun x => x ^ n • f x) ξ‖
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
k n : ℕ
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ |ξ| ^ k * (2 * π) ^ k = ‖(2 * ↑π * I * ↑ξ) ^ k‖