Weak Problem RHSOf Field And Datum bound

theorem weakProblemRHSOfFieldAndDatum_bound    {Ω : Set E} (hΩ : IsOpen Ω)    (A : EllipticCoeff d Ω)    {F : E → E} (hF : MemLp F 2 (volume.restrict Ω))    {u₀ : E → ℝ} (hu₀ : MemW1pWitness 2 u₀ Ω)    (v : E → ℝ) (hv0 : MemH01 v Ω) (hv : MemW1pWitness 2 v Ω) :    |weakProblemRHSOfFieldAndDatum (A := A) (Ω := Ω) F hu₀ v| ≤      ((∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) +          A.Λ * (∫ x, ‖hu₀.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ))) *        (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) := by  let CF : ℝ :=    (∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ))  let CU : ℝ :=    A.Λ * (∫ x, ‖hu₀.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ))  let GV : ℝ :=    (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ))  rw [weakProblemRHSOfFieldAndDatum_eq_of_memH01 hΩ A hu₀ hv0 hv]  have hdiv : |divergenceRHSOfField F hv| ≤ CF * GV := by    simpa [CF, GV] using divergenceRHSOfField_bound hF hv  have hbilin : |bilinFormOfCoeff A hu₀ hv| ≤ CU * GV := by    simpa [CU, GV, mul_assoc] using bilinForm_bound A hu₀ hv  calc    |divergenceRHSOfField F hv - bilinFormOfCoeff A hu₀ hv|      = |divergenceRHSOfField F hv + (-bilinFormOfCoeff A hu₀ hv)| := by ring_nf    _ ≤ |divergenceRHSOfField F hv| + |-bilinFormOfCoeff A hu₀ hv| := abs_add_le _ _    _ = |divergenceRHSOfField F hv| + |bilinFormOfCoeff A hu₀ hv| := by simp    _ ≤ CF * GV + CU * GV := add_le_add hdiv hbilin    _ = (CF + CU) * GV := by ring    _ = ((∫ x, ‖F x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) +          A.Λ * (∫ x, ‖hu₀.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ))) *        (∫ x, ‖hv.weakGrad x‖ ^ (2 : ℝ) ∂(volume.restrict Ω)) ^ (1 / (2 : ℝ)) := by      rfl