De Giorgi preiter of energy

theorem deGiorgi_preiter_of_energy    {α : Type*} [MeasurableSpace α] {μ : Measure α} [IsFiniteMeasure μ]    {d : ℕ} (hd : 0 < (d : ℝ))    {u : α → ℝ} {θ lam : ℝ}    {Ilam Iθ G Csob Cenergy : ℝ}    (hθl : θ < lam)    (hCsob : 0 ≤ Csob) (hCenergy : 0 ≤ Cenergy)    (hIθ : 0 ≤ Iθ)    (hint : Integrable (fun x => |positivePartSub u θ x| ^ 2) μ)    (hsob :      Ilam ≤ Csob * G * (μ.real {x | lam < u x}) ^ (2 / (d : ℝ)))    (henergy :      G ≤ Cenergy * Iθ)    (hIθ_bound :      ∫ x, |positivePartSub u θ x| ^ 2 ∂μ ≤ Iθ) :    Ilam ≤      Csob * Cenergy * ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ))) * Iθ := by  have hm_nonneg : 0 ≤ μ.real {x | lam < u x} := measureReal_nonneg  have hmeasure0 :      μ.real {x | lam < u x} ≤        ((lam - θ) ^ 2)⁻¹ * ∫ x, |positivePartSub u θ x| ^ 2 ∂μ :=    superlevel_measureReal_le_integral_posPart hθl hint  have hmeasure :      μ.real {x | lam < u x} ≤ ((lam - θ) ^ 2)⁻¹ * Iθ := by    calc      μ.real {x | lam < u x}          ≤ ((lam - θ) ^ 2)⁻¹ * ∫ x, |positivePartSub u θ x| ^ 2 ∂μ := hmeasure0      _ ≤ ((lam - θ) ^ 2)⁻¹ * Iθ := by        gcongr  exact deGiorgi_preiter_abstract hd hCsob hCenergy hIθ hm_nonneg hsob hmeasure henergy