Theorem: LoVe.Vector.add.comm (LoVe/Labs/Lab8Solution.lean)

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

State before:
case a
n : ℕ
u v : Vector ℤ n
⊢ ↑(add u v) = ↑(add v u)
Tactic:
simp [Vector.add]
State after:
case a
n : ℕ
u v : Vector ℤ n
⊢ List.add ↑u ↑v = List.add ↑v ↑u

State before:
case a
n : ℕ
u v : Vector ℤ n
⊢ List.add ↑u ↑v = List.add ↑v ↑u
Tactic:
apply List.add.comm
State after:
no goals