Theorem: LoVe.take_drop (LoVe/Labs/Lab4Solution.lean)

State before:
α : Type
x✝ : List α
⊢ take 0 x✝ ++ drop 0 x✝ = x✝
Tactic:
rfl
State after:
no goals

State before:
α : Type
n✝ : ℕ
⊢ take (n✝ + 1) [] ++ drop (n✝ + 1) [] = []
Tactic:
rfl
State after:
no goals

State before:
α : Type
m : ℕ
x : α
xs : List α
⊢ take (m + 1) (x :: xs) ++ drop (m + 1) (x :: xs) = x :: xs
Tactic:
simp [take, drop, take_drop m]
State after:
no goals