Theorem: LoVe.Vector.neg_neg (LoVe/Lectures/LoVe12_LogicalFoundationsOfMathematics_Demo.lean)

State before:
n : ℕ
v : Vector ℤ n
⊢ neg (neg v) = v
Tactic:
apply Subtype.eq
State after:
case a
n : ℕ
v : Vector ℤ n
⊢ ↑(neg (neg v)) = ↑v

State before:
case a
n : ℕ
v : Vector ℤ n
⊢ ↑(neg (neg v)) = ↑v
Tactic:
simp [Vector.neg]
State after:
no goals