case h₁.h
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x ^ 4 ≤ 1

case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ x ^ 2 ≤ 1
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x ^ 4 * (5 / 96) + x ^ 2 / 2 ≤ 1 * (5 / 96) + 1 / 2
gcongr
no goals
case h₁.h
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x ^ 4 ≤ 1
exact pow_le_one _ (abs_nonneg _) hx
case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x * abs' x ≤ 1
case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ x ^ 2 ≤ 1
rw [sq, ← abs_mul_self, abs_mul]
no goals
case h₂.h
x : ℝ
hx : abs' x ≤ 1
⊢ abs' x * abs' x ≤ 1
exact mul_le_one hx (abs_nonneg _) hx
no goals
x : ℝ
hx : abs' x ≤ 1
⊢ 1 * (5 / 96) + 1 / 2 < 1
norm_num