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

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have ha : 0 ≤ a := by linarith
State after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
⊢ 0 < (a * x) ^ 2 - x ^ 2

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have ha1 : 1 < a := by linarith
State after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
⊢ 0 < (a * x) ^ 2 - x ^ 2

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have hx : 0 ≤ x := by linarith
State after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < (a * x) ^ 2 - x ^ 2

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
have hx2 : 0 < x ^ (2 : ℝ) := by positivity
State after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 0 < (a * x) ^ 2 - x ^ 2

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 0 < (a * x) ^ 2 - x ^ 2
Tactic:
rw [sub_pos, Real.mul_rpow ha hx, ← div_lt_iff hx2, div_self (ne_of_gt hx2)]
State after:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 1 < a ^ 2

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
hx2 : 0 < x ^ 2
⊢ 1 < a ^ 2
Tactic:
simp [ha1, abs_eq_self.mpr ha]
State after:
no goals

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

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

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

State before:
a x : ℝ
h1 : 0 < a - 1
h2 : 0 < x
ha : 0 ≤ a
ha1 : 1 < a
hx : 0 ≤ x
⊢ 0 < x ^ 2
Tactic:
positivity
State after:
no goals