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

State before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y
Tactic:
have hxy := add_nonneg hx hy
State after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y

State before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (x + y).soCone ![x - y, 2 * z] ↔ z ^ 2 ≤ x * y
Tactic:
conv => lhs; unfold soCone; simp [sqrt_le_left hxy, ← le_sub_iff_add_le']
State after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (2 * z) ^ 2 ≤ (x + y) ^ 2 - (x - y) ^ 2 ↔ z ^ 2 ≤ x * y

State before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ (2 * z) ^ 2 ≤ (x + y) ^ 2 - (x - y) ^ 2 ↔ z ^ 2 ≤ x * y
Tactic:
ring_nf
State after:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ z ^ 2 * 4 ≤ x * y * 4 ↔ z ^ 2 ≤ x * y

State before:
n : Type ?u.52431
m : Type ?u.52428
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
hxy : 0 ≤ x + y
⊢ z ^ 2 * 4 ≤ x * y * 4 ↔ z ^ 2 ≤ x * y
Tactic:
simp
State after:
no goals