rw [← Real.rpow_add (by positivity)]
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ 1 * A ^ (-(3 / 4)) < C₁ / (C₂ * 2)
A C₁ C₂ : ℝ
Apos : 0 < A
C₁pos : 0 < C₁
C₂pos : 0 < C₂
hA : A ≤ 1 / 2 * (C₁ / (C₂ * 2)) ^ 4
⊢ A ^ (1 + -(3 / 4)) < C₁ / (C₂ * 2)