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

case h₂.h
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x ^ 3 ≤ x
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ abs' x ^ 4 * (5 / 96) + x ^ 3 / 6 ≤ x * (5 / 96) + x / 6
gcongr
no goals
case h₁.h
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ abs' x ^ 4 ≤ x
calc
  |x| ^ 4 ≤ |x| ^ 1 :=
    pow_le_pow_of_le_one (abs_nonneg _)
      (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]) (by decide)
  _ = x := by simp [_root_.abs_of_nonneg (le_of_lt hx0)]
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ abs' x ≤ 1
rwa [_root_.abs_of_nonneg (le_of_lt hx0)]
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 1 ≤ 4
decide
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ abs' x ^ 1 = x
simp [_root_.abs_of_nonneg (le_of_lt hx0)]
no goals
case h₂.h
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x ^ 3 ≤ x
calc
  x ^ 3 ≤ x ^ 1 := pow_le_pow_of_le_one (le_of_lt hx0) hx (by decide)
  _ = x := pow_one _
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ 1 ≤ 3
decide
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ x * (5 / 96) + x / 6 < x
linarith
no goals
x : ℝ
hx0 : 0 < x
hx : x ≤ 1
⊢ abs' x ≤ 1
rwa [_root_.abs_of_nonneg (le_of_lt hx0)]