Theorem: Real.soCone_add_sub_two_of_nonneg (CvxLean/Lib/Cones/SOCone.lean)

State before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
have h := soCone_add_sub_two_mul_of_nonneg 1 hx hy
State after:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2 * 1] ↔ 1 ^ 2 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y

State before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2 * 1] ↔ 1 ^ 2 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
rw [mul_one, one_rpow] at h
State after:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y

State before:
n : Type ?u.62790
m : Type ?u.62787
inst✝¹ : Fintype m
inst✝ : Fintype n
x y : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h : (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
⊢ (x + y).soCone ![x - y, 2] ↔ 1 ≤ x * y
Tactic:
exact h
State after:
no goals