calc _ ≤ ((|t| / ↑⌊|t|⌋₊) ^ (2 : ℝ)) := by gcongr; exact h₁
     _ ≤ (2 : ℝ) ^ (2 : ℝ) := by gcongr
     _ = 4 := by norm_num
case intro
σ t : ℝ
t_ge : 3 < |t|
σ_le : σ ≤ 2
h₁ : 1 ≤ |t| / ↑⌊|t|⌋₊
h₂ : |t| / ↑⌊|t|⌋₊ ≤ 2
⊢ (|t| / ↑⌊|t|⌋₊) ^ σ ≤ 4
no goals