Dirichlet Problem exists of divergence Data

theorem dirichletProblem_exists_of_divergenceData    {Ω : Set E}    (hd : 2 ≤ d)    (hΩ : IsOpen Ω) (hΩ_bdd : Bornology.IsBounded Ω)    (A : EllipticCoeff d Ω)    {u₀ : E → ℝ} (hu₀ : MemW1p 2 u₀ Ω)    {F : E → E} (hF : MemLp F 2 (volume.restrict Ω)) :    ∃ u : E → ℝ,      MemW1p 2 u Ω ∧      MemW01p 2 (fun x => u x - u₀ x) Ω ∧      ∀ (hu : MemW1pWitness 2 u Ω) (v : E → ℝ), MemH01 v Ω →        ∀ (hv : MemW1pWitness 2 v Ω),          bilinFormOfCoeff A hu hv = divergenceRHSOfField F hv := by  let hu₀w : MemW1pWitness 2 u₀ Ω := DeGiorgi.MemW1p.someWitness hu₀  let rhs := weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w  obtain ⟨w, hwsol⟩ :=    weakProblem_exists hd hΩ hΩ_bdd A rhs      (by        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          rhs (fun x => u x + v x)              = divergenceRHSOfField F huv - bilinFormOfCoeff A hu₀w huv := by                  exact weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w huv0 huv          _ = (divergenceRHSOfField F hu + divergenceRHSOfField F hv) -                (bilinFormOfCoeff A hu₀w hu + bilinFormOfCoeff A hu₀w hv) := by                  rw [divergenceRHSOfField_add hF hu hv, bilinFormOfCoeff_add_right A hu₀w hu hv]          _ = weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w u +                weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w v := by                  rw [weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hu0 hu,                    weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hv0 hv]                  ring          _ = rhs u + rhs v := by rfl)      (by        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          rhs (fun x => c * u x)              = divergenceRHSOfField F hcu - bilinFormOfCoeff A hu₀w hcu := by                  exact weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hcu0 hcu          _ = c * divergenceRHSOfField F hu - c * bilinFormOfCoeff A hu₀w hu := by                rw [divergenceRHSOfField_smul c hu, bilinFormOfCoeff_smul_right c A hu₀w hu]          _ = c * weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w u := by                rw [weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hu0 hu]                ring          _ = c * rhs u := by rfl)      <| by        have hCF_nonneg :            0 ≤ (∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) := by          positivity        have hCU_nonneg :            0 ≤ A.Λ * (∫ x, ‖hu₀w.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^              (1 / (2 : ℝ)) := by          refine mul_nonneg A.Λ_nonneg ?_          positivity        refine ⟨((∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) +            A.Λ * (∫ x, ‖hu₀w.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^              (1 / (2 : ℝ))), add_nonneg hCF_nonneg hCU_nonneg, ?_⟩        intro v hv0 hv        simpa [rhs] using weakProblemRHSOfFieldAndDatum_bound hΩ A hF hu₀w v hv0 hv  have hw0 : MemH01 w Ω := hwsol.left  let hw : MemW1pWitness 2 w Ω :=    DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hw0)  let u : E → ℝ := fun x => w x + u₀ x  let hu : MemW1pWitness 2 u Ω := hw.add hu₀w  refine ⟨u, hu.memW1p, ?_, ?_⟩  · simpa [u] using hw0  · intro hu' v hv0 hv    calc      bilinFormOfCoeff A hu' hv = bilinFormOfCoeff A hu hv := by        exact bilinFormOfCoeff_eq_left hΩ A hu' hu hv      _ = bilinFormOfCoeff A hw hv + bilinFormOfCoeff A hu₀w hv := by        simpa [hu] using bilinFormOfCoeff_add_left A hw hu₀w hv      _ = rhs v + bilinFormOfCoeff A hu₀w hv := by        rw [hwsol.right hw v hv0 hv]      _ = weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀w v +            bilinFormOfCoeff A hu₀w hv := by        rfl      _ = divergenceRHSOfField F hv := by        rw [weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀w hv0 hv]        ring