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

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

State before:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ∧ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ y ≤ x ∧ z ^ 2 ≤ -(x * y)
Tactic:
apply Iff.and
State after:
case h₁
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ↔ y ≤ x

case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ z ^ 2 ≤ -(x * y)

State before:
case h₁
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ y ≤ x ↔ y ≤ x
Tactic:
rfl
State after:
no goals

State before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ (2 * z) ^ 2 ≤ (x - y) ^ 2 - (x + y) ^ 2 ↔ z ^ 2 ≤ -(x * y)
Tactic:
ring_nf!
State after:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 ≤ -(x * y * 4) ↔ z ^ 2 ≤ -(x * y)

State before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 ≤ -(x * y * 4) ↔ z ^ 2 ≤ -(x * y)
Tactic:
rw [← neg_mul, ← div_le_iff (by norm_num)]
State after:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 / 4 ≤ -(x * y) ↔ z ^ 2 ≤ -(x * y)

State before:
case h₂
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ z ^ 2 * 4 / 4 ≤ -(x * y) ↔ z ^ 2 ≤ -(x * y)
Tactic:
simp
State after:
no goals

State before:
n : Type ?u.63307
m : Type ?u.63304
inst✝¹ : Fintype m
inst✝ : Fintype n
x y z : ℝ
⊢ 0 < 4
Tactic:
norm_num
State after:
no goals