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