Tensor Product localcomponent apply

lemma TensorProduct.localcomponent_apply    (φ : FiniteAdeleRing R K ⊗[K] V →L[FiniteAdeleRing R K] FiniteAdeleRing R K ⊗[K] V)    (x : FiniteAdeleRing R K ⊗[K] V) (p : HeightOneSpectrum R) :    (ContinuousLinearMap.rTensor' V      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) (φ x) =    TensorProduct.localcomponent R K V p φ ((ContinuousLinearMap.rTensor' V      (evalContinuousAlgebraMap R K p).toContinuousLinearMap) x) := by  dsimp [localcomponent]  rw [← ContinuousLinearMap.rTensor'_comp_apply]  change (LinearMap.rTensor V _) (φ x) = (LinearMap.rTensor V _) (φ ((LinearMap.rTensor V _) x))  rw [singleContinuousAlgebraMap_comp_evalContinuousLinearMap]  let f := (LinearMap.lsmul    (FiniteAdeleRing R K) (FiniteAdeleRing R K) (localIdempotent R K p)).restrictScalars K  have hf : LinearMap.rTensor V f x = (localIdempotent R K p) • x := by    induction x with    | zero => simp    | tmul x y => exact LinearMap.rTensor_tmul _ _ _ _    | add x y _ _ => simp_all  rw [hf, ContinuousLinearMap.map_smul]  change (AlgHom.rTensor V ((evalContinuousAlgebraMap R K p).toAlgHom)) (φ x) =    (AlgHom.rTensor V ((evalContinuousAlgebraMap R K p).toAlgHom)) (localIdempotent R K p • φ x)  simp [eval_localIdempotent]