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

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

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

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

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