Weak Problem unique

theorem weakProblem_unique    (hd : 2 ≤ d)    {P : WeakProblem (d := d)}    {u v : E → ℝ}    (hu : IsWeakSolution P u)    (hv : IsWeakSolution P v) :    u =ᵐ[volume.restrict P.Ω] v := by  have hu0 : MemH01 u P.Ω := hu.left  have hv0 : MemH01 v P.Ω := hv.left  have hdiff0 : MemH01 (fun x => u x - v x) P.Ω := MemW01p.sub hu0 hv0  let hwu : MemW1pWitness 2 u P.Ω :=    DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hu0)  let hwv : MemW1pWitness 2 v P.Ω :=    DeGiorgi.MemW1p.someWitness (MemW01p.memW1p hv0)  let hdiff_add : MemW1pWitness 2 (fun x => u x + (-1) * v x) P.Ω :=    hwu.add (hwv.smul (-1))  let hdiff : MemW1pWitness 2 (fun x => u x - v x) P.Ω := {    memLp := by      simpa [sub_eq_add_neg, Pi.smul_apply] using hdiff_add.memLp    weakGrad := hdiff_add.weakGrad    weakGrad_component_memLp := by      intro i      simpa [sub_eq_add_neg, Pi.smul_apply] using hdiff_add.weakGrad_component_memLp i    isWeakGrad := by      intro i      simpa [sub_eq_add_neg, Pi.smul_apply] using hdiff_add.isWeakGrad i }  have hzero_test :      ∀ (φ : E → ℝ), MemH01 φ P.Ω →        ∀ (hφ : MemW1pWitness 2 φ P.Ω),          bilinFormOfCoeff P.coeff hdiff hφ = 0 := by    intro φ hφ0 hφ    calc      bilinFormOfCoeff P.coeff hdiff hφ          = bilinFormOfCoeff P.coeff hdiff_add hφ := by              rfl      _ = bilinFormOfCoeff P.coeff hwu hφ +            bilinFormOfCoeff P.coeff (hwv.smul (-1)) hφ := by              simpa [hdiff_add] using bilinFormOfCoeff_add_left P.coeff hwu (hwv.smul (-1)) hφ      _ = bilinFormOfCoeff P.coeff hwu hφ + (-1) * bilinFormOfCoeff P.coeff hwv hφ := by            rw [bilinFormOfCoeff_smul_left (-1) P.coeff hwv hφ]      _ = P.rhs φ + (-1) * P.rhs φ := by rw [hu.right hwu φ hφ0 hφ, hv.right hwv φ hφ0 hφ]      _ = 0 := by ring  have h_ws : bilinFormOfCoeff P.coeff hdiff hdiff = (0 : ℝ) := hzero_test _ hdiff0 hdiff  have hstab :      (∫ x, ‖hdiff.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict P.Ω)) ^ (1 / (2 : ℝ)) ≤        P.coeff.lam⁻¹ * (0 : ℝ) := by    simpa using weakSolution_stability P.coeff hdiff0 hdiff      (rhs := fun _ : E → ℝ => (0 : ℝ)) (C_F := 0) (by norm_num)      (by intro φ hφ0 hφ; simp) h_ws  have hseminorm_zero :      (∫ x, ‖hdiff.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict P.Ω)) ^ (1 / (2 : ℝ)) = 0 := by    refine le_antisymm ?_ ?_    · simpa using hstab    · positivity  have hgrad_zero : gradLpOfWitness hdiff = 0 := by    apply norm_eq_zero.mp    simpa [norm_gradLpOfWitness_eq hdiff] using hseminorm_zero  have hdiff_ae_zero :      (fun x => u x - v x) =ᵐ[volume.restrict P.Ω] 0 := by    exact ae_eq_zero_of_memH01_of_gradLpOfWitness_eq_zero hd P.hΩ P.hΩ_bdd hdiff0 hdiff hgrad_zero  filter_upwards [hdiff_ae_zero] with x hx  simpa [sub_eq_zero] using hx