∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] {W : Type u_3}
  [inst_6 : NormedAddCommGroup W] [inst_7 : InnerProductSpace ℝ W] [inst_8 : MeasurableSpace W] [inst_9 : BorelSpace W]
  [inst_10 : FiniteDimensional ℝ W] [inst_11 : FiniteDimensional ℝ V] (A : W ≃ₗᵢ[ℝ] V) (f : V → E) (w : W),
  FourierTransformInv.fourierInv (f ∘ ⇑A) w = FourierTransformInv.fourierInv f (A w)