Has Weak Partial Deriv mul smooth

theorem HasWeakPartialDeriv.mul_smooth {Ω : Set E} (hΩ : IsOpen Ω)    {i : Fin d} {g f η : E → ℝ}    (hf : HasWeakPartialDeriv i g f Ω)    (hη : ContDiff ℝ (⊤ : ℕ∞) η)    (hf_int : LocallyIntegrable f (volume.restrict Ω))    (hg_int : LocallyIntegrable g (volume.restrict Ω)) :    HasWeakPartialDeriv i      (fun x => η x * g x + (fderiv ℝ η x) (EuclideanSpace.single i 1) * f x)      (fun x => η x * f x) Ω := by  let _ := hΩ  intro φ hφ_smooth hφ_supp hφ_sub  have hηφ_smooth : ContDiff ℝ (⊤ : ℕ∞) (fun x => η x * φ x) := hη.mul hφ_smooth  have hηφ_supp : HasCompactSupport (fun x => η x * φ x) := hφ_supp.mul_left  have hηφ_tsub : tsupport (fun x => η x * φ x) ⊆ Ω :=    (tsupport_smul_subset_right η φ).trans hφ_sub  have hη_diff : Differentiable ℝ η := hη.differentiable (by simp)  have hφ_diff : Differentiable ℝ φ := hφ_smooth.differentiable (by simp)  let ei : E := EuclideanSpace.single i (1 : ℝ)  have fderiv_prod : ∀ x : E, (fderiv ℝ (fun y => η y * φ y) x) ei =      η x * (fderiv ℝ φ x) ei + φ x * (fderiv ℝ η x) ei := by    intro x    rw [fderiv_fun_mul hη_diff.differentiableAt hφ_diff.differentiableAt]    simp [ContinuousLinearMap.add_apply, ContinuousLinearMap.smul_apply, smul_eq_mul]  have key :      ∫ x in Ω, f x * (η x * (fderiv ℝ φ x) ei + φ x * (fderiv ℝ η x) ei) =        -∫ x in Ω, g x * (η x * φ x) := by    simpa [fderiv_prod, ei] using hf (fun x => η x * φ x) hηφ_smooth hηφ_supp hηφ_tsub  have hη_deriv_cont : Continuous (fun x => (fderiv ℝ η x) ei) :=    (hη.continuous_fderiv (by simp)).clm_apply continuous_const  have hφ_deriv_cont : Continuous (fun x => (fderiv ℝ φ x) ei) :=    (hφ_smooth.continuous_fderiv (by simp)).clm_apply continuous_const  have hφ_deriv_supp : HasCompactSupport (fun x => (fderiv ℝ φ x) ei) :=    hφ_supp.fderiv_apply (𝕜 := ℝ) ei  have int_f_φ_dη :      Integrable (fun x => f x * (φ x * (fderiv ℝ η x) ei)) (volume.restrict Ω) := by    have h := hf_int.integrable_smul_right_of_hasCompactSupport      (hφ_smooth.continuous.mul hη_deriv_cont) hφ_supp.smul_right    simpa [smul_eq_mul] using h  have int_f_η_dφ :      Integrable (fun x => f x * (η x * (fderiv ℝ φ x) ei)) (volume.restrict Ω) := by    have h := hf_int.integrable_smul_right_of_hasCompactSupport      (hη.continuous.mul hφ_deriv_cont) hφ_deriv_supp.mul_left    simpa [smul_eq_mul] using h  have int_g_ηφ : Integrable (fun x => g x * (η x * φ x)) (volume.restrict Ω) := by    have h := hg_int.integrable_smul_right_of_hasCompactSupport      (hη.continuous.mul hφ_smooth.continuous) hηφ_supp    simpa [smul_eq_mul] using h  have key2 :      ∫ x in Ω, f x * (η x * (fderiv ℝ φ x) ei) + f x * (φ x * (fderiv ℝ η x) ei) =        -∫ x in Ω, g x * (η x * φ x) := by    simp_rw [← mul_add] at key ⊢    exact key  rw [integral_add int_f_η_dφ int_f_φ_dη] at key2  show ∫ x in Ω, η x * f x * (fderiv ℝ φ x) ei =    -∫ x in Ω, (η x * g x + (fderiv ℝ η x) ei * f x) * φ x  have goal_rhs_conv :      (fun x => (η x * g x + (fderiv ℝ η x) ei * f x) * φ x) =        (fun x => g x * (η x * φ x) + f x * (φ x * (fderiv ℝ η x) ei)) := by    ext x    ring  simp_rw [goal_rhs_conv]  rw [integral_add int_g_ηφ int_f_φ_dη, neg_add]  have goal_lhs_conv :      (fun x => η x * f x * (fderiv ℝ φ x) ei) =        (fun x => f x * (η x * (fderiv ℝ φ x) ei)) := by    ext x    ring  simp_rw [goal_lhs_conv]  linarith