Has Weak Partial Deriv of cont Diff

theorem HasWeakPartialDeriv.of_contDiff {Ω : Set E} (hΩ : IsOpen Ω)    {i : Fin d} {f : E → ℝ} (hf : ContDiff ℝ 1 f) :    HasWeakPartialDeriv i (fun x => (fderiv ℝ f x) (EuclideanSpace.single i 1)) f Ω := by  let _ := hΩ  intro φ hφ hφ_supp hφ_sub  let v := EuclideanSpace.single i (1 : ℝ)  have h_fderiv_supp : tsupport (fun x => (fderiv ℝ φ x) v) ⊆ Ω :=    (tsupport_fderiv_apply_subset ℝ v).trans hφ_sub  have hf_diff : Differentiable ℝ f := hf.differentiable one_ne_zero  have hφ_diff : Differentiable ℝ φ := hφ.differentiable (by simp)  have hf_cont : Continuous f := hf_diff.continuous  have hφ_cont : Continuous φ := hφ_diff.continuous  have hfderiv_φ_cont : Continuous (fun x => (fderiv ℝ φ x) v) :=    (hφ.continuous_fderiv (by simp)).clm_apply continuous_const  have hfderiv_f_cont : Continuous (fun x => (fderiv ℝ f x) v) :=    (hf.continuous_fderiv one_ne_zero).clm_apply continuous_const  have hφ_fderiv_supp : HasCompactSupport (fun x => (fderiv ℝ φ x) v) :=    hφ_supp.fderiv_apply (𝕜 := ℝ) v  rw [setIntegral_eq_integral_of_forall_compl_eq_zero, setIntegral_eq_integral_of_forall_compl_eq_zero]  ·    exact integral_mul_fderiv_eq_neg_fderiv_mul_of_integrable      ((hfderiv_f_cont.mul hφ_cont).integrable_of_hasCompactSupport hφ_supp.mul_left)      ((hf_cont.mul hfderiv_φ_cont).integrable_of_hasCompactSupport hφ_fderiv_supp.mul_left)      ((hf_cont.mul hφ_cont).integrable_of_hasCompactSupport hφ_supp.mul_left)      (fun x _ => hf_diff x) (fun x _ => hφ_diff x)  ·    intro x hx    have : x ∉ tsupport φ := fun h => hx (hφ_sub h)    simp only [mul_eq_zero]    right    by_contra hf'    exact this (subset_tsupport φ (mem_support.mpr hf'))  ·    intro x hx    have : x ∉ tsupport (fun x => (fderiv ℝ φ x) v) := fun h => hx (h_fderiv_supp h)    simp only [mul_eq_zero]    right    by_contra hf'    exact this (subset_tsupport _ (mem_support.mpr hf'))