Weak Problem exists of divergence Data

theorem weakProblem_exists_of_divergenceData    {Ω : Set E}    (hd : 2 ≤ d)    (hΩ : IsOpen Ω) (hΩ_bdd : Bornology.IsBounded Ω)    (A : EllipticCoeff d Ω)    {F : E → E} (hF : MemLp F 2 (volume.restrict Ω)) :    ∃ u : E → ℝ,      IsWeakSolution (d := d)        ⟨Ω, hΩ, hΩ_bdd, A, weakProblemRHSOfField (Ω := Ω) F⟩ u := by  refine weakProblem_exists hd hΩ hΩ_bdd A (weakProblemRHSOfField (Ω := Ω) F) ?_ ?_ ?_  · intro u v hu0 hv0    let hu : MemW1pWitness 2 u Ω :=      DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hu0)    let hv : MemW1pWitness 2 v Ω :=      DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hv0)    have huv0 : MemH01 (fun x => u x + v x) Ω := MemW01p.add hu0 hv0    let huv : MemW1pWitness 2 (fun x => u x + v x) Ω := hu.add hv    calc      weakProblemRHSOfField (Ω := Ω) F (fun x => u x + v x)          = divergenceRHSOfField F huv := by              exact weakProblemRHSOfField_eq_of_memH01 hΩ huv0 huv      _ = divergenceRHSOfField F hu + divergenceRHSOfField F hv := by            exact divergenceRHSOfField_add hF hu hv      _ = weakProblemRHSOfField (Ω := Ω) F u + weakProblemRHSOfField (Ω := Ω) F v := by            rw [weakProblemRHSOfField_eq_of_memH01 hΩ hu0 hu,              weakProblemRHSOfField_eq_of_memH01 hΩ hv0 hv]  · intro c u hu0    let hu : MemW1pWitness 2 u Ω :=      DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hu0)    have hcu0 : MemH01 (fun x => c * u x) Ω := by      simpa [Pi.smul_apply, smul_eq_mul] using (MemW01p.smul c hu0)    let hcu : MemW1pWitness 2 (fun x => c * u x) Ω := hu.smul c    calc      weakProblemRHSOfField (Ω := Ω) F (fun x => c * u x)          = divergenceRHSOfField F hcu := by              exact weakProblemRHSOfField_eq_of_memH01 hΩ hcu0 hcu      _ = c * divergenceRHSOfField F hu := by            exact divergenceRHSOfField_smul c hu      _ = c * weakProblemRHSOfField (Ω := Ω) F u := by            rw [weakProblemRHSOfField_eq_of_memH01 hΩ hu0 hu]  · refine ⟨(∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)), by positivity, ?_⟩    intro v hv0 hv    exact weakProblemRHSOfField_bound hΩ hF v hv0 hv