have h1 : 0 < b * a := Real.mul_pos hb ha
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
⊢ 2 ≤ (a * a + b * b) / (b * a)
case mk.mk
a : ℝ
ha : 0 < a
b : ℝ
hb : 0 < b
h1 : 0 < b * a
⊢ 2 ≤ (a * a + b * b) / (b * a)