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

State before:
⊢ add [] [] = add [] []
Tactic:
rfl
State after:
no goals

State before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add (x :: xs) (y :: ys) = add (y :: ys) (x :: xs)
Tactic:
simp [List.add, add_comm]
State after:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add xs ys = add ys xs

State before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ add xs ys = add ys xs
Tactic:
exact List.add.comm xs ys
State after:
no goals

State before:
y : ℤ
ys : List ℤ
⊢ add [] (y :: ys) = add (y :: ys) []
Tactic:
rfl
State after:
no goals

State before:
x : ℤ
xs : List ℤ
⊢ add (x :: xs) [] = add [] (x :: xs)
Tactic:
rfl
State after:
no goals