Theorem: Mathlib.Meta.Positivity.Real.one_sub_sq_nonneg_of_le_one (CvxLean/Tactic/Arith/PositivityExt.lean)

State before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
⊢ 0 ≤ 1 - x ^ 2
Tactic:
have hx1 : x ≤ 1 := by linarith
State after:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 - x ^ 2

State before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ 0 ≤ 1 - x ^ 2
Tactic:
rw [le_sub_iff_add_le, zero_add]
State after:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ x ^ 2 ≤ 1

State before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
⊢ x ^ 2 ≤ 1
Tactic:
simpa [abs_eq_self.mpr h1]
State after:
no goals

State before:
x : ℝ
h1 : 0 ≤ x
h2 : 0 ≤ 1 - x
⊢ x ≤ 1
Tactic:
linarith
State after:
no goals