FKS2.two_mul_sqrt_div_le_quarter

lemma two_mul_sqrt_div_le_quarter (t : ℝ) (ht : t ≥ 1000) :    2 * Real.sqrt (t / 5.5666305) ≤ t / 4 := by  -- Suggested proof:  -- 1) note `t > 0` and `0 < (5.5666305:ℝ)`.  -- 2) square both sides using `Real.mul_self_le_mul_self_iff` (or `sq_le_sq`),  --    reducing to `4*(t/5.5666305) ≤ (t/4)^2`.  -- 3) simplify to `t ≥ 64/5.5666305`, then use `ht` and `norm_num`.  have ht0 : 0 ≤ t := by linarith  have hdiv_nonneg : 0 ≤ t / 5.5666305 := by positivity  have hright_nonneg : 0 ≤ t / 4 := by positivity  have h64 : (64 / 5.5666305 : ℝ) ≤ t := by    have hnum : (64 / 5.5666305 : ℝ) < 1000 := by norm_num    linarith  have hmain : 4 * (t / 5.5666305) ≤ (t / 4) ^ 2 := by    have hmul : (64 / 5.5666305 : ℝ) * t ≤ t * t := by      exact mul_le_mul_of_nonneg_right h64 ht0    have hdiv16 : ((64 / 5.5666305 : ℝ) * t) / 16 ≤ (t * t) / 16 :=      div_le_div_of_nonneg_right hmul (by norm_num)    norm_num [pow_two, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] at hdiv16 ⊢    exact hdiv16  have hsq : (2 * Real.sqrt (t / 5.5666305)) * (2 * Real.sqrt (t / 5.5666305)) ≤ (t / 4) * (t / 4) := by    have hsqrt_sq : (Real.sqrt (t / 5.5666305)) ^ 2 = t / 5.5666305 := Real.sq_sqrt hdiv_nonneg    calc      (2 * Real.sqrt (t / 5.5666305)) * (2 * Real.sqrt (t / 5.5666305))          = 4 * (Real.sqrt (t / 5.5666305)) ^ 2 := by ring      _ = 4 * (t / 5.5666305) := by rw [hsqrt_sq]      _ ≤ (t / 4) ^ 2 := hmain      _ = (t / 4) * (t / 4) := by ring  have hnonneg_left : 0 ≤ 2 * Real.sqrt (t / 5.5666305) := by positivity  exact (mul_self_le_mul_self_iff hnonneg_left hright_nonneg).2 hsq