Theorem: LoVe.List.length_add (LoVe/Labs/Lab8Solution.lean)

State before:
⊢ List.length [] = List.length [] → List.length (add [] []) = List.length []
Tactic:
simp [List.add]
State after:
no goals

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

State before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
⊢ List.length xs = List.length ys → List.length (add xs ys) = List.length xs
Tactic:
intro hsame
State after:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
hsame : List.length xs = List.length ys
⊢ List.length (add xs ys) = List.length xs

State before:
x : ℤ
xs : List ℤ
y : ℤ
ys : List ℤ
hsame : List.length xs = List.length ys
⊢ List.length (add xs ys) = List.length xs
Tactic:
rw [List.length_add xs ys hsame]
State after:
no goals

State before:
y : ℤ
ys : List ℤ
⊢ List.length [] = List.length (y :: ys) → List.length (add [] (y :: ys)) = List.length []
Tactic:
intro hsame
State after:
y : ℤ
ys : List ℤ
hsame : List.length [] = List.length (y :: ys)
⊢ List.length (add [] (y :: ys)) = List.length []

State before:
y : ℤ
ys : List ℤ
hsame : List.length [] = List.length (y :: ys)
⊢ List.length (add [] (y :: ys)) = List.length []
Tactic:
cases hsame
State after:
no goals

State before:
x : ℤ
xs : List ℤ
⊢ List.length (x :: xs) = List.length [] → List.length (add (x :: xs) []) = List.length (x :: xs)
Tactic:
intro hsame
State after:
x : ℤ
xs : List ℤ
hsame : List.length (x :: xs) = List.length []
⊢ List.length (add (x :: xs) []) = List.length (x :: xs)

State before:
x : ℤ
xs : List ℤ
hsame : List.length (x :: xs) = List.length []
⊢ List.length (add (x :: xs) []) = List.length (x :: xs)
Tactic:
cases hsame
State after:
no goals