Smooth1Properties_above_aux2

lemma Smooth1Properties_above_aux2 {x y ε : ℝ} (hε : ε ∈ Ioo 0 1) (hy : y ∈ Ioc 0 1)  (hx2 : 2 ^ ε < x) :    2 < (x / y) ^ (1 / ε) := by  obtain ⟨εpos, ε1⟩ := hε  obtain ⟨ypos, y1⟩ := hy  calc    _ > (2 ^ ε / y) ^ (1 / ε) := ?_    _ = 2 / y ^ (1 / ε) := ?_    _ ≥ 2 / y := ?_    _ ≥ 2 := ?_  · rw [gt_iff_lt, div_rpow, div_rpow, lt_div_iff₀, mul_comm_div, div_self, mul_one]    <;> try positivity    · exact rpow_lt_rpow (by positivity) hx2 (by positivity)    · exact LT.lt.le <| lt_trans (by positivity) hx2  · rw [div_rpow, ← rpow_mul, mul_div_cancel₀ 1 <| ne_of_gt εpos, rpow_one] <;> positivity  · have : y ^ (1 / ε) ≤ y := by      nth_rewrite 2 [← rpow_one y]      exact rpow_le_rpow_of_exponent_ge ypos y1 (by linarith [one_lt_one_div εpos ε1])    have pos : 0 < y ^ (1 / ε) := rpow_pos_of_pos ypos _    rw [ge_iff_le, div_le_iff₀, div_mul_eq_mul_div, le_div_iff₀', mul_comm] <;> try linarith  · rw [ge_iff_le, le_div_iff₀ <| ypos]; exact (mul_le_iff_le_one_right zero_lt_two).mpr y1