∀ {𝕜 : Type u_4} [inst : NontriviallyNormedField 𝕜] {E : Type u_1} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_3} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {F' : Type u_2} [inst_6 : NormedAddCommGroup F']
  [inst_7 : NormedSpace ℝ F'] [inst_8 : NormedSpace 𝕜 F'] {n : ℕ∞} [inst_9 : Algebra ℝ 𝕜]
  [inst_10 : IsScalarTower ℝ 𝕜 F] [inst_11 : IsScalarTower ℝ 𝕜 F'] (T : F →L[𝕜] F') (x : TopologicalSpace.Compacts E)
  (x_1 : ↑x ⊆ ↑Ω) (x_2 : ContDiffMapSupportedIn E F n x),
  (fun f => { toFun := ⇑T ∘ ⇑f, contDiff' := ⋯, hasCompactSupport' := ⋯, tsupport_subset' := ⋯ })
      (TestFunction.ofSupportedIn x_1 x_2) =
    ((fun K K_sub_Ω => (TestFunction.ofSupportedInCLM 𝕜 K_sub_Ω).comp (ContDiffMapSupportedIn.postcompCLM T)) x x_1) x_2