Dirichlet Problem unique of divergence Data

theorem dirichletProblem_unique_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 v : E → ℝ}    (hu : IsDirichletWeakSolutionOfDivergenceData A u₀ F u)    (hv : IsDirichletWeakSolutionOfDivergenceData A u₀ F v) :    u =ᵐ[volume.restrict Ω] v := by  let P : WeakProblem (d := d) :=    ⟨Ω, hΩ, hΩ_bdd, A,      weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F        (DeGiorgi.MemW1p.someWitness hu₀)⟩  have hu_shift :      IsWeakSolution P (fun x => u x - u₀ x) := by    exact isWeakSolution_subDatum_of_dirichletProblem (Ω := Ω) hΩ hΩ_bdd A hu₀ hu  have hv_shift :      IsWeakSolution P (fun x => v x - u₀ x) := by    exact isWeakSolution_subDatum_of_dirichletProblem (Ω := Ω) hΩ hΩ_bdd A hu₀ hv  have hshift_eq :      (fun x => u x - u₀ x) =ᵐ[volume.restrict Ω] (fun x => v x - u₀ x) := by    simpa [P] using weakProblem_unique hd hu_shift hv_shift  filter_upwards [hshift_eq] with x hx  linarith