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

State before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ match v.unrotateSoCone w x with
  | (t, x) => t.soCone x
Tactic:
simp [soCone, unrotateSoCone]
State after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2

State before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : v.rotatedSoCone w x
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Tactic:
replace ⟨h, hv, hw⟩ := h
State after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2

State before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2).sqrt ≤ (v + w) / √2
Tactic:
rw [sqrt_le_iff]
State after:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2 ∧ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2

State before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2 ∧ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
split_ands
State after:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2

case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2

State before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2

case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
{ simp [le_div_iff]; linarith }
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
{ rw [Fin.sum_univ_succ]
  simp [Matrix.vecCons]
  rw [add_comm, ← le_sub_iff_add_le]
  field_simp
  have hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2 := by norm_cast; ring
  norm_cast at hrw h
  rwa [hrw] }
State after:
no goals

State before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ (v + w) / √2
Tactic:
simp [le_div_iff]
State after:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ v + w

State before:
case refine_1
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ 0 ≤ v + w
Tactic:
linarith
State after:
no goals

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin (n + 1), Matrix.vecCons ((v - w) / √2) x x_1 ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
rw [Fin.sum_univ_succ]
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ Matrix.vecCons ((v - w) / √2) x 0 ^ 2 + ∑ i : Fin n, Matrix.vecCons ((v - w) / √2) x i.succ ^ 2 ≤ ((v + w) / √2) ^ 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ Matrix.vecCons ((v - w) / √2) x 0 ^ 2 + ∑ i : Fin n, Matrix.vecCons ((v - w) / √2) x i.succ ^ 2 ≤ ((v + w) / √2) ^ 2
Tactic:
simp [Matrix.vecCons]
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (v - w) ^ 2 / 2 + ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ (v - w) ^ 2 / 2 + ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2
Tactic:
rw [add_comm, ← le_sub_iff_add_le]
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2 - (v - w) ^ 2 / 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ (v + w) ^ 2 / 2 - (v - w) ^ 2 / 2
Tactic:
field_simp
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
have hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2 := by norm_cast; ring
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
norm_cast at hrw h
State after:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
h : ∑ x_1 : Fin n, x x_1 ^ 2 ≤ v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2

State before:
case refine_2
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
hv : 0 ≤ v
hw : 0 ≤ w
hrw : ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
h : ∑ x_1 : Fin n, x x_1 ^ 2 ≤ v * w * 2
⊢ ∑ x_1 : Fin n, x x_1 ^ 2 ≤ ((v + w) ^ 2 - (v - w) ^ 2) / 2
Tactic:
rwa [hrw]
State after:
no goals

State before:
n✝ : Type ?u.32056
m : Type ?u.32053
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
v w : ℝ
x : Fin n → ℝ
h : ∑ i : Fin n, x i ^ 2 ≤ v * w * 2
hv : 0 ≤ v
hw : 0 ≤ w
⊢ ((v + w) ^ 2 - (v - w) ^ 2) / 2 = v * w * 2
Tactic:
ring
State after:
no goals