De Giorgi preiter abstract

theorem deGiorgi_preiter_abstract    {d : ℕ} (hd : 0 < (d : ℝ))    {Ilam Iθ G m Csob Cenergy θ lam : ℝ}    (hCsob : 0 ≤ Csob) (hCenergy : 0 ≤ Cenergy)    (hIθ : 0 ≤ Iθ) (hm : 0 ≤ m)    (hsob : Ilam ≤ Csob * G * m ^ (2 / (d : ℝ)))    (hmeasure : m ≤ ((lam - θ) ^ 2)⁻¹ * Iθ)    (henergy : G ≤ Cenergy * Iθ) :    Ilam ≤      Csob * Cenergy * ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ))) * Iθ := by  have hexp_nonneg : 0 ≤ 2 / (d : ℝ) := by positivity  have hm_pow :      m ^ (2 / (d : ℝ)) ≤ ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ))) := by    exact Real.rpow_le_rpow hm hmeasure hexp_nonneg  have hGI :      G * m ^ (2 / (d : ℝ)) ≤        (Cenergy * Iθ) * ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ))) := by    exact mul_le_mul henergy hm_pow (by positivity) (by positivity)  calc    Ilam ≤ Csob * (G * m ^ (2 / (d : ℝ))) := by      simpa [mul_assoc] using hsob    _ ≤ Csob * ((Cenergy * Iθ) * ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ)))) := by      exact mul_le_mul_of_nonneg_left hGI hCsob    _ = Csob * Cenergy * ((((lam - θ) ^ 2)⁻¹ * Iθ) ^ (2 / (d : ℝ))) * Iθ := by      ring