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

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

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

State before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
have h0x2 : 0 < x ^ (2 : ℝ) := by positivity
State after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ 0 ≤ 1 / x ^ 2 - 1

State before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ 0 ≤ 1 / x ^ 2 - 1
Tactic:
rw [le_sub_iff_add_le, zero_add, le_div_iff h0x2, one_mul]
State after:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
h0x2 : 0 < x ^ 2
⊢ x ^ 2 ≤ 1

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

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

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

State before:
x : ℝ
h1 : 0 < x
h2 : 0 ≤ 1 - x
hx1 : x ≤ 1
h0x : 0 ≤ x
⊢ 0 < x ^ 2
Tactic:
positivity
State after:
no goals