Is Weak Solution sub Datum of dirichlet Problem

theorem isWeakSolution_subDatum_of_dirichletProblem    {Ω : Set E}    (hΩ : IsOpen Ω) (hΩ_bdd : Bornology.IsBounded Ω)    (A : EllipticCoeff d Ω)    {u₀ : E → ℝ} (hu₀ : MemW1p 2 u₀ Ω)    {F : E → E} {u : E → ℝ}    (hu : IsDirichletWeakSolutionOfDivergenceData A u₀ F u) :    IsWeakSolution (d := d)      ⟨Ω, hΩ, hΩ_bdd, A,        weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F          (DeGiorgi.MemW1p.someWitness hu₀)⟩      (fun x => u x - u₀ x) := by  let hu₀w : MemW1pWitness 2 u₀ Ω := DeGiorgi.MemW1p.someWitness hu₀  let huu : MemW1pWitness 2 u Ω := DeGiorgi.MemW1p.someWitness hu.left  let hsub_add : MemW1pWitness 2 (fun x => u x + (-1) * u₀ x) Ω :=    huu.add (hu₀w.smul (-1))  let hsub : MemW1pWitness 2 (fun x => u x - u₀ x) Ω := {    memLp := by      simpa [sub_eq_add_neg, Pi.smul_apply] using hsub_add.memLp    weakGrad := hsub_add.weakGrad    weakGrad_component_memLp := by      intro i      simpa [sub_eq_add_neg, Pi.smul_apply] using hsub_add.weakGrad_component_memLp i    isWeakGrad := by      intro i      simpa [sub_eq_add_neg, Pi.smul_apply] using hsub_add.isWeakGrad i }  refine ⟨hu.2.1, ?_⟩  intro hw' v hv0 hv  calc    bilinFormOfCoeff A hw' hv = bilinFormOfCoeff A hsub hv := by      exact bilinFormOfCoeff_eq_left hΩ A hw' hsub hv    _ = bilinFormOfCoeff A hsub_add hv := by          rfl    _ = bilinFormOfCoeff A huu hv + bilinFormOfCoeff A (hu₀w.smul (-1)) hv := by          simpa [hsub_add] using bilinFormOfCoeff_add_left A huu (hu₀w.smul (-1)) hv    _ = bilinFormOfCoeff A huu hv + (-1) * bilinFormOfCoeff A hu₀w hv := by          rw [bilinFormOfCoeff_smul_left (-1) A hu₀w hv]    _ = divergenceRHSOfField F hv + (-1) * bilinFormOfCoeff A hu₀w hv := by          rw [hu.2.2 huu v hv0 hv]    _ = divergenceRHSOfField F hv - bilinFormOfCoeff A hu₀w hv := by          ring    _ = weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w v := by          symm          exact weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hv0 hv