doc: fix example

This commit is contained in:
Sebastian Ullrich 2021-04-17 18:48:58 +02:00
parent 8175003707
commit 52a4f535d8

View file

@ -244,7 +244,7 @@ theorem mem_split {a : α} {as : List α} (h : a ∈ as) : ∃ s t, as = s ++ a
| cons b bs ih => cases h with
| head a bs => exact ⟨[], ⟨bs, rfl⟩⟩
| tail a b bs h =>
match bs, ih h with
match (generalizing := false) bs, ih h with
| _, ⟨s, ⟨t, rfl⟩⟩ =>
exists b::s; exists t
rw [List.cons_append]