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

State before:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ((x + y) i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]
Tactic:
dsimp
State after:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]

State before:
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ (x i + y i).soCone (![x - y, 2 • z]ᵀ i) ↔ (x i + y i).soCone ![x i - y i, 2 * z i]
Tactic:
convert Iff.rfl
State after:
case h.e'_2.h.e'_4
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2 * z i] = ![x - y, 2 • z]ᵀ i

State before:
case h.e'_2.h.e'_4
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
⊢ ![x i - y i, 2 * z i] = ![x - y, 2 • z]ᵀ i
Tactic:
funext j
State after:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2 * z i] j = ![x - y, 2 • z]ᵀ i j

State before:
case h.e'_2.h.e'_4.h
n✝ : Type ?u.71362
m : Type ?u.71359
inst✝¹ : Fintype m
inst✝ : Fintype n✝
n : ℕ
x y z : Fin n → ℝ
i : Fin n
j : Fin (Nat.succ 1)
⊢ ![x i - y i, 2 * z i] j = ![x - y, 2 • z]ᵀ i j
Tactic:
fin_cases j <;> simp
State after:
no goals