A Harmonic replacement unique

theorem aHarmonic_replacement_unique    {Ω : Set E} (hd : 2 ≤ d)    (hΩ : IsOpen Ω) (hΩ_bdd : Bornology.IsBounded Ω)    {u h₁ h₂ : E → ℝ}    (A : EllipticCoeff d Ω)    (hu : MemW1p 2 u Ω)    (hh₁ : IsHomogeneousWeakSolution A h₁)    (hdiff₁ : MemW01p 2 (fun x => h₁ x - u x) Ω)    (hh₂ : IsHomogeneousWeakSolution A h₂)    (hdiff₂ : MemW01p 2 (fun x => h₂ x - u x) Ω) :    h₁ =ᵐ[volume.restrict Ω] h₂ := by  have hF0 : MemLp (fun _ : E => (0 : E)) 2 (volume.restrict Ω) := by    exact MeasureTheory.MemLp.zero' (p := (2 : ENNReal)) (μ := volume.restrict Ω)  have hs₁ : IsDirichletWeakSolutionOfDivergenceData A u (fun _ : E => (0 : E)) h₁ := by    refine ⟨hh₁.left, hdiff₁, ?_⟩    intro hh φ hφ hφw    simpa [divergenceRHSOfField, divergenceRHSIntegrandOfField] using hh₁.right hh φ hφ hφw  have hs₂ : IsDirichletWeakSolutionOfDivergenceData A u (fun _ : E => (0 : E)) h₂ := by    refine ⟨hh₂.left, hdiff₂, ?_⟩    intro hh φ hφ hφw    simpa [divergenceRHSOfField, divergenceRHSIntegrandOfField] using hh₂.right hh φ hφ hφw  exact dirichletProblem_unique_of_divergenceData hd hΩ hΩ_bdd A hu hF0 hs₁ hs₂