ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>p : β → Bool<VAR>l : List α<GOAL>List.filter p (List.filterMap f l) = List.filterMap (fun x => Option.filter p (f x)) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>p : α → Bool<VAR>f : α → Option β<VAR>l : List α<GOAL>List.filterMap f (List.filter p l) = List.filterMap (fun x => if p x = true then f x else none) l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>l : List α<VAR>b : β<GOAL>b ∈ List.filterMap f l ↔ ∃ a, a ∈ l ∧ f a = some b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l l' : List α<VAR>f : α → Option β<GOAL>List.filterMap f (l ++ l') = List.filterMap f l ++ List.filterMap f l'
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>L : List (List α)<GOAL>List.filterMap f L.join = (List.map (List.filterMap f) L).join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → Option β<VAR>g : β → α<VAR>H : ∀ (x : α), Option.map g (f x) = some x<VAR>l : List α<GOAL>List.map g (List.filterMap f l) = l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<GOAL>l₁.length ≤ n → (l₁ ++ l₂)[n]? = l₂[n - l₁.length]?
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : l₁.length ≤ n<GOAL>(l₁ ++ l₂).get? n = l₂.get? (n - l₁.length)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h₁ : l₁.length ≤ n<VAR>h₂ : n < (l₁ ++ l₂).length<GOAL>(l₁ ++ l₂)[n] = l₂[n - l₁.length]
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h₁ : l₁.length ≤ n<VAR>h₂ : n < (l₁ ++ l₂).length<GOAL>n - l₁.length < l₂.length
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h₁ : l₁.length ≤ n<VAR>h₂ : n < (l₁ ++ l₂).length<GOAL>(l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, ⋯⟩
<VAR>α : Type u_1<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<VAR>n : Nat<VAR>l : List α<VAR>eq : l = l₁ ++ a :: l₂<VAR>h : l₁.length = n<GOAL>l[n] = a
<VAR>α : Type u_1<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<VAR>n : Nat<VAR>l : List α<VAR>eq : l = l₁ ++ a :: l₂<VAR>h : l₁.length = n<GOAL>n < l.length
<VAR>α : Type u_1<VAR>l₁ : List α<VAR>a : α<VAR>l₂ : List α<VAR>n : Nat<VAR>l : List α<VAR>eq : l = l₁ ++ a :: l₂<VAR>h : l₁.length = n<GOAL>l.get ⟨n, ⋯⟩ = a
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l → ∃ s t, l = s ++ a :: t
<GOAL>∀ {α : Type u_1} {x : α} {l : List α}, [x] ++ l = x :: l
<VAR>α : Type u_1<VAR>s₁ s₂ t₁ t₂ : List α<GOAL>s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂ ∧ t₁ = t₂
<GOAL>∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → t₁ = t₂
<GOAL>∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → s₁.length = s₂.length → s₁ = s₂
<GOAL>∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂ ∧ t₁ = t₂
<GOAL>∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → t₁ = t₂
<GOAL>∀ {α : Type u_1} {s₁ t₁ s₂ t₂ : List α}, s₁ ++ t₁ = s₂ ++ t₂ → t₁.length = t₂.length → s₁ = s₂
<VAR>α : Type u_1<VAR>t₁ t₂ : List α<VAR>s : List α<GOAL>s ++ t₁ = s ++ t₂ ↔ t₁ = t₂
<VAR>α : Type u_1<VAR>s₁ s₂ : List α<VAR>t : List α<GOAL>s₁ ++ t = s₂ ++ t ↔ s₁ = s₂
<GOAL>∀ {α : Type u_1} {p q : List α}, p ++ q = [] ↔ p = [] ∧ q = []
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<VAR>h : l ++ [a] ≠ []<GOAL>(l ++ [a]).getLast h = a
<GOAL>∀ {α : Type u_1} {l : List α} {a : α} {h : l.concat a ≠ []}, (l.concat a).getLast h = a
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : n < l₁.length<GOAL>(l₁ ++ l₂)[n] = l₁[n]
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : n < l₁.length<GOAL>(l₁ ++ l₂).get ⟨n, ⋯⟩ = l₁.get ⟨n, h⟩
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : List α<VAR>h : i < as.length<VAR>h' : i < (as ++ bs).length<GOAL>(as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩
<VAR>α : Type u_1<VAR>i : Nat<VAR>as bs : List α<VAR>h : ¬i < as.length<VAR>h' : i < (as ++ bs).length<VAR>h'' : i - as.length < bs.length<GOAL>(as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>hn : n < l₁.length<GOAL>(l₁ ++ l₂)[n]? = l₁[n]?
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>hn : n < l₁.length<GOAL>(l₁ ++ l₂).get? n = l₁.get? n
<GOAL>∀ {α : Type u_1} {l₁ l₂ : List α}, l₁.append l₂ = l₁ ++ l₂
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s ≠ [] → s ++ t ≠ []
<VAR>α : Type u_1<VAR>s t : List α<GOAL>t ≠ [] → s ++ t ≠ []
<GOAL>∀ {α : Type u_1} {a b : List α}, [] = a ++ b ↔ a = [] ∧ b = []
<VAR>α : Type u_1<VAR>a b : List α<VAR>h0 : a ≠ []<GOAL>a ++ b ≠ []
<GOAL>∀ {α : Type u_1} {a b : List α} {x : α} {c : List α}, a ++ b = x :: c ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b
<GOAL>∀ {α : Type u_1} {x : α} {c a b : List α}, x :: c = a ++ b ↔ a = [] ∧ b = x :: c ∨ ∃ a', a = x :: a' ∧ c = a' ++ b
<VAR>α : Type u_1<VAR>a b c d : List α<GOAL>a ++ b = c ++ d ↔ (∃ a', c = a ++ a' ∧ b = a' ++ d) ∨ ∃ c', a = c ++ c' ∧ d = c' ++ b
<VAR>α : Type u_1<VAR>a : α<VAR>s t : List α<GOAL>a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t
<VAR>α : Type u_1<VAR>a : α<VAR>s t : List α<VAR>h₁ : ¬a ∈ s<VAR>h₂ : ¬a ∈ t<GOAL>¬a ∈ s ++ t
<VAR>α : Type u_1<VAR>a : α<VAR>s t : List α<GOAL>(a ∈ s ++ t) = (a ∈ s ∨ a ∈ t)
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ : List α<VAR>l₂ : List α<VAR>h : a ∈ l₁<GOAL>a ∈ l₁ ++ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ : List α<VAR>l₂ : List α<VAR>h : a ∈ l₂<GOAL>a ∈ l₁ ++ l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>a ∈ l ↔ ∃ s t, l = s ++ a :: t
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>l₁ l₂ : List α<GOAL>(∀ (x : α), x ∈ l₁ ++ l₂ → p x) ↔ (∀ (x : α), x ∈ l₁ → p x) ∧ ∀ (x : α), x ∈ l₂ → p x
<VAR>α : Type u_1<VAR>a : α<GOAL>[].concat a = [a]
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>(a :: l).concat b = a :: l.concat b
<VAR>α : Type u_1<VAR>a b : α<VAR>l₁ l₂ : List α<GOAL>l₁.concat a = l₂.concat b → l₁ = l₂
<VAR>α : Type u_1<VAR>a b : α<VAR>l₁ l₂ : List α<GOAL>l₁.concat a = l₂.concat b → a = b
<VAR>α : Type u_1<VAR>l l' : List α<VAR>a : α<GOAL>l.concat a = l'.concat a ↔ l = l'
<VAR>α : Type u_1<VAR>l l' : List α<VAR>a b : α<GOAL>l.concat a = l'.concat b ↔ l = l' ∧ a = b
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>l.concat a ≠ []
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁.concat a ++ l₂ = l₁ ++ a :: l₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.map f (l.concat a) = (List.map f l).concat (f a)
<VAR>α : Type u_1<VAR>l : List α<GOAL>l = [] ∨ ∃ L b, l = L.concat b
<VAR>α : Type u_1<VAR>a : α<VAR>L : List (List α)<GOAL>a ∈ L.join ↔ ∃ l, l ∈ L ∧ a ∈ l
<GOAL>∀ {α : Type u_1} {a : α} {L : List (List α)}, a ∈ L.join → ∃ l, l ∈ L ∧ a ∈ l
<GOAL>∀ {α : Type u_1} {l : List α} {L : List (List α)} {a : α}, l ∈ L → a ∈ l → a ∈ L.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>L : List (List α)<GOAL>List.map f L.join = (List.map (List.map f) L).join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>xs ys : List α<VAR>f : α → List β<GOAL>(xs ++ ys).bind f = xs.bind f ++ ys.bind f
<VAR>α : Type u_1<VAR>l : List (List α)<GOAL>l.bind id = l.join
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → List β<VAR>b : β<VAR>l : List α<GOAL>b ∈ l.bind f ↔ ∃ a, a ∈ l ∧ b ∈ f a
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>b : β<VAR>l : List α<VAR>f : α → List β<GOAL>b ∈ l.bind f → ∃ a, a ∈ l ∧ b ∈ f a
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>b : β<VAR>l : List α<VAR>f : α → List β<VAR>a : α<VAR>al : a ∈ l<VAR>h : b ∈ f a<GOAL>b ∈ l.bind f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → List β<VAR>x : α<GOAL>[x].bind f = f x
<VAR>α : Type u_1<VAR>l : List α<GOAL>(l.bind fun x => [x]) = l
<VAR>γ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : List α<VAR>f : α → List β<VAR>g : β → List γ<GOAL>(l.bind f).bind g = l.bind fun x => (f x).bind g
<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>α : Type u_3<VAR>f : β → γ<VAR>g : α → List β<VAR>l : List α<GOAL>List.map f (l.bind g) = l.bind fun a => List.map f (g a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>g : β → List γ<VAR>l : List α<GOAL>(List.map f l).bind g = l.bind fun a => g (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l = l.bind fun x => [f x]
<GOAL>∀ {α : Type u_1} {a : α}, List.replicate 1 a = [a]
<VAR>α : Type u_1<VAR>BEq α<VAR>n : Nat<VAR>a b : α<GOAL>(List.replicate n b).contains a = (a == b && !n == 0)
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>n : Nat<GOAL>decide (b ∈ List.replicate n a) = (decide ¬(n == 0) = true && b == a)
<VAR>α : Type u_1<VAR>a b : α<VAR>n : Nat<GOAL>b ∈ List.replicate n a ↔ n ≠ 0 ∧ b = a
<VAR>α : Type u_1<VAR>a b : α<VAR>n : Nat<VAR>h : b ∈ List.replicate n a<GOAL>b = a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>List.replicate (n + 1) a ≠ []
<VAR>α : Type u_1<VAR>a : α<VAR>n m : Nat<VAR>h : m < (List.replicate n a).length<GOAL>(List.replicate n a)[m] = a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>m : Fin (List.replicate n a).length<GOAL>(List.replicate n a).get m = a
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {m : Nat}, (List.replicate n a)[m]? = if m < n then some a else none
<GOAL>∀ {α : Type u_1} {a : α} {n m : Nat}, m < n → (List.replicate n a)[m]? = some a
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {m : Nat} {b : α}, List.replicate n a = List.replicate m b ↔ n = m ∧ (n = 0 ∨ a = b)
<VAR>α : Type u_1<VAR>a : α<VAR>l : List α<GOAL>(∀ (b : α), b ∈ l → b = a) → l = List.replicate l.length a
<VAR>α : Type u_1<VAR>a : α<VAR>n : Nat<VAR>l : List α<GOAL>l = List.replicate n a ↔ l.length = n ∧ ∀ (b : α), b ∈ l → b = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<VAR>b : β<GOAL>List.map f l = List.replicate l.length b ↔ ∀ (x : α), x ∈ l → f x = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>b : β<GOAL>List.map (Function.const α b) l = List.replicate l.length b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>b : β<GOAL>List.map (fun x => b) l = List.replicate l.length b
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {m : Nat}, List.replicate n a ++ List.replicate m a = List.replicate (n + m) a
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {α_1 : Type u_2} {f : α → α_1}, List.map f (List.replicate n a) = List.replicate n (f a)
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α} {p : α → Bool}, List.filter p (List.replicate n a) = if p a = true then List.replicate n a else []
<GOAL>∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, p a = true → List.filter p (List.replicate n a) = List.replicate n a
<GOAL>∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, ¬p a = true → List.filter p (List.replicate n a) = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : Nat<VAR>a : α<VAR>f : α → Option β<GOAL>List.filterMap f (List.replicate n a) = match f a with | none => [] | some b => List.replicate n b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>b : β<VAR>n : Nat<VAR>f : α → Option β<VAR>h : f a = some b<GOAL>List.filterMap f (List.replicate n a) = List.replicate n b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>n : Nat<VAR>f : α → Option β<VAR>h : (f a).isSome = true<GOAL>List.filterMap f (List.replicate n a) = List.replicate n ((f a).get h)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>n : Nat<VAR>f : α → Option β<VAR>h : f a = none<GOAL>List.filterMap f (List.replicate n a) = []
<VAR>n : Nat<VAR>α : Type u_1<GOAL>(List.replicate n []).join = []
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α}, (List.replicate n [a]).join = List.replicate n a
<VAR>n m : Nat<GOAL>∀ {α : Type u_1} {a : α}, (List.replicate n (List.replicate m a)).join = List.replicate (n * m) a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>β : Type u_2<VAR>f : α → List β<GOAL>(List.replicate n a).bind f = (List.replicate n (f a)).join
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {a : α}, (List.replicate n a).isEmpty = decide (n = 0)
<VAR>α : Type u_1<VAR>as : List α<GOAL>as.reverse.length = as.length
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<GOAL>i + j + 1 = l.length → l.reverse[i]? = l[j]?
<VAR>α : Type u_1<VAR>l : List α<VAR>i j : Nat<VAR>h : i + j + 1 = l.length<GOAL>l.reverse.get? i = l.get? j
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>h : i < l.length<GOAL>l.reverse[i]? = l[l.length - 1 - i]?
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>h : i < l.length<GOAL>l.reverse.get? i = l.get? (l.length - 1 - i)
<VAR>α : Type u_1<VAR>as bs : List α<GOAL>(as.reverseAux bs).reverseAux [] = bs.reverseAux as
<VAR>α : Type u_1<VAR>as : List α<GOAL>as.reverse.reverse = as
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse.getLast? = l.head?
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.reverse.head? = l.getLast?
<VAR>α : Type u_1<VAR>as bs : List α<GOAL>(as ++ bs).reverse = bs.reverse ++ as.reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l.reverse = (List.map f l).reverse
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>(List.map f l).reverse = List.map f l.reverse
<VAR>α : Type u_1<VAR>xs : List α<GOAL>xs.reverse = [] ↔ xs = []
<VAR>α : Type u_1<VAR>x : α<VAR>as bs : List α<GOAL>x ∈ as.reverseAux bs ↔ x ∈ as ∨ x ∈ bs
<VAR>α : Type u_1<VAR>x : α<VAR>as : List α<GOAL>x ∈ as.reverse ↔ x ∈ as
<VAR>α : Type u_1<VAR>as bs : List α<GOAL>as.reverseAux bs = as.reverse ++ bs
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>Monad m<VAR>l : List α<VAR>f : α → β → m β<VAR>b : β<GOAL>List.foldrM f b l.reverse = List.foldlM (fun x y => f y x) b l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : β → α → β<VAR>b : β<GOAL>List.foldl f b l.reverse = List.foldr (fun x y => f y x) b l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β → β<VAR>b : β<GOAL>List.foldr f b l.reverse = List.foldl (fun x y => f y x) b l
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>(List.replicate n a).reverse = List.replicate n a
<VAR>α : Type u_1<VAR>as : List α<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<GOAL>List.elem a (a :: as) = true
<VAR>α : Type u_1<VAR>a : α<VAR>as : List α<VAR>x : α<VAR>BEq α<GOAL>(a :: as).contains x = (x == a || as.contains x)
<VAR>α : Type u_1<VAR>BEq α<VAR>l : List α<VAR>a : α<GOAL>l.contains a = l.any fun x => a == x
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<GOAL>List.take n l ++ List.drop n l = l
<VAR>α : Type u_1<VAR>i : Nat<VAR>l : List α<GOAL>(List.drop i l).length = l.length - i
<VAR>α : Type u_1<VAR>i : Nat<VAR>l : List α<VAR>h : l.length ≤ i<GOAL>List.drop i l = []
<VAR>α : Type u_1<VAR>i : Nat<VAR>l : List α<VAR>h : l.length ≤ i<GOAL>List.take i l = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.drop l.length l = []
<VAR>α : Type u_1<VAR>l : List α<GOAL>List.take l.length l = l
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>h : i < l.length<GOAL>(List.take i l).concat l[i] = List.take (i + 1) l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>(l.concat a).reverse = a :: l.reverse
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>h : l.length ≤ n<GOAL>List.take n l = l
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>List.take l₁.length (l₁ ++ l₂) = l₁
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : l₁.length = n<GOAL>List.take n (l₁ ++ l₂) = l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>L : List α<VAR>i : Nat<GOAL>List.map f (List.take i L) = List.take i (List.map f L)
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<VAR>h : m < n<GOAL>(List.take n l)[m]? = l[m]?
<VAR>α : Type u_1<VAR>l : List α<VAR>n m : Nat<VAR>h : m < n<GOAL>(List.take n l).get? m = l.get? m
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>(List.take (n + 1) l)[n]? = l[n]?
<VAR>α : Type u_1<VAR>l : List α<VAR>n : Nat<GOAL>List.take (n + 1) l = List.take n l ++ l[n]?.toList
<VAR>α : Type u_1<VAR>l : List α<VAR>k : Nat<GOAL>List.take k l = [] ↔ l = [] ∨ k = 0
<VAR>α : Type u_1<VAR>as : List α<VAR>i : Nat<GOAL>as = [] → List.take i as = []
<VAR>α : Type u_1<VAR>as : List α<VAR>i : Nat<VAR>h : List.take i as ≠ []<GOAL>as ≠ []
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.dropLast = List.take l.length.pred l
<VAR>α : Type u_1<VAR>l : List α<VAR>k : Nat<GOAL>List.drop k l = [] ↔ l.length ≤ k
<VAR>α : Type u_1<VAR>SizeOf α<VAR>l : List α<VAR>n : Nat<GOAL>sizeOf (List.drop n l) ≤ sizeOf l
<VAR>α : Type u_1<VAR>n m : Nat<VAR>l : List α<GOAL>List.drop n (List.drop m l) = List.drop (n + m) l
<VAR>α : Type u_1<VAR>m n : Nat<VAR>l : List α<GOAL>List.take n (List.drop m l) = List.drop m (List.take (m + n) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>L : List α<VAR>i : Nat<GOAL>List.map f (List.drop i L) = List.drop i (List.map f L)
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Nat<VAR>h : i < l.length<GOAL>l[i] :: List.drop (i + 1) l = List.drop i l
<VAR>α : Type u_1<VAR>l : List α<VAR>i : Fin l.length<GOAL>l.get i :: List.drop (↑i + 1) l = List.drop (↑i) l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>List.drop n l = l[n] :: List.drop (n + 1) l
<VAR>α : Type u_1<VAR>n : Nat<VAR>l : List α<VAR>h : n < l.length<GOAL>List.drop n l = l.get ⟨n, h⟩ :: List.drop (n + 1) l
<VAR>α : Type u_1<VAR>as : List α<VAR>i : Nat<GOAL>as = [] → List.drop i as = []
<VAR>α : Type u_1<VAR>as : List α<VAR>i : Nat<VAR>h : List.drop i as ≠ []<GOAL>as ≠ []
<VAR>α : Type u_1<VAR>m n : Nat<VAR>l : List α<GOAL>List.drop (m + n) l = List.drop m (List.drop n l)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>List.drop l₁.length (l₁ ++ l₂) = l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>n : Nat<VAR>h : l₁.length = n<GOAL>List.drop n (l₁ ++ l₂) = l₂
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<GOAL>List.takeWhile p (a :: l) = if p a = true then a :: List.takeWhile p l else []
<VAR>α : Type u_1<VAR>x : α<VAR>xs : List α<VAR>p : α → Bool<GOAL>List.dropWhile p (x :: xs) = if p x = true then List.dropWhile p xs else x :: xs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : β → Bool<VAR>l : List α<GOAL>List.takeWhile p (List.map f l) = List.map f (List.takeWhile (p ∘ f) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>p : β → Bool<VAR>l : List α<GOAL>List.dropWhile p (List.map f l) = List.map f (List.dropWhile (p ∘ f) l)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.takeWhile p l ++ List.dropWhile p l = l
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>xs ys : List α<GOAL>List.dropWhile p (xs ++ ys) = if (List.dropWhile p xs).isEmpty = true then List.dropWhile p ys else List.dropWhile p xs ++ ys
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>p : α → Bool<GOAL>List.takeWhile p (List.replicate n a) = List.filter p (List.replicate n a)
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>p : α → Bool<GOAL>List.takeWhile p (List.replicate n a) = if p a = true then List.replicate n a else []
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>p : α → Bool<GOAL>List.dropWhile p (List.replicate n a) = List.filter (fun a => !p a) (List.replicate n a)
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<VAR>p : α → Bool<GOAL>List.dropWhile p (List.replicate n a) = if p a = true then [] else List.replicate n a
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>as bs : List α<GOAL>List.partition.loop p l (as, bs) = (as.reverse ++ List.filter p l, bs.reverse ++ List.filter (not ∘ p) l)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.partition p l = (List.filter p l, List.filter (not ∘ p) l)
<VAR>α : Type u_1<VAR>xs : List α<GOAL>xs.dropLast.length = xs.length - 1
<VAR>α : Type u_1<VAR>xs : List α<VAR>i : Nat<VAR>h : i < xs.dropLast.length<GOAL>xs.dropLast[i] = xs[i]
<VAR>α : Type u_1<VAR>xs : List α<VAR>i : Fin xs.dropLast.length<GOAL>xs.dropLast.get i = xs.get ⟨↑i, ⋯⟩
<VAR>α : Type u<VAR>x : α<VAR>l : List α<VAR>h : l ≠ []<GOAL>(x :: l).dropLast = x :: l.dropLast
<VAR>α : Type u<VAR>l : List α<VAR>l' : List α<GOAL>l ≠ [] → (l' ++ l).dropLast = l' ++ l.dropLast
<GOAL>∀ {α : Type u_1} {l₁ : List α} {b : α} {l₂ : List α}, (l₁ ++ b :: l₂).dropLast = l₁ ++ (b :: l₂).dropLast
<GOAL>∀ {α : Type u_1} {l₁ : List α} {b : α}, (l₁ ++ [b]).dropLast = l₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>l : List α<GOAL>List.map f l.dropLast = (List.map f l).dropLast
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>(List.replicate n a).dropLast = List.replicate (n - 1) a
<VAR>α : Type u_1<VAR>n : Nat<VAR>a : α<GOAL>(a :: List.replicate n a).dropLast = List.replicate n a
<VAR>α : Type u_1<VAR>BEq α<VAR>as bs : List α<VAR>LawfulBEq α<VAR>a : α<GOAL>(a :: as).isPrefixOf (a :: bs) = as.isPrefixOf bs
<VAR>α : Type u_1<VAR>BEq α<VAR>L : List α<VAR>h : 0 < L.length<GOAL>L.isPrefixOf [] = false
<VAR>α : Type u_1<VAR>BEq α<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.isPrefixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun x => x == a)
<VAR>α : Type u_1<VAR>BEq α<VAR>a : α<VAR>as : List α<GOAL>(a :: as).isSuffixOf [] = false
<VAR>α : Type u_1<VAR>BEq α<VAR>l : List α<VAR>n : Nat<VAR>a : α<GOAL>l.isSuffixOf (List.replicate n a) = (decide (l.length ≤ n) && l.all fun x => x == a)
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.rotateLeft 0 = l
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.rotateRight 0 = l
<VAR>α : Type u_1<VAR>BEq α<VAR>as : List α<VAR>b : α<VAR>LawfulBEq α<VAR>a : α<GOAL>(a :: as).replace a b = b :: as
<VAR>α : Type u_1<VAR>BEq α<VAR>a b : α<VAR>l : List α<VAR>h : (!List.elem a l) = true<GOAL>l.replace a b = l
<VAR>α : Type u_1<VAR>BEq α<VAR>n : Nat<VAR>b : α<VAR>LawfulBEq α<VAR>a : α<VAR>h : 0 < n<GOAL>(List.replicate n a).replace a b = b :: List.replicate (n - 1) a
<VAR>α : Type u_1<VAR>BEq α<VAR>n : Nat<VAR>a b c : α<VAR>h : (!b == a) = true<GOAL>(List.replicate n a).replace b c = List.replicate n a
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<GOAL>List.insert a [] = [a]
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>List.insert a l = l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : ¬a ∈ l<GOAL>List.insert a l = a :: l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>l : List α<GOAL>a ∈ List.insert b l ↔ a = b ∨ a ∈ l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<GOAL>a ∈ List.insert a l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>a ∈ List.insert b l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a b : α<VAR>l : List α<VAR>h : a ∈ List.insert b l<GOAL>a = b ∨ a ∈ l
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(List.insert a l).length = l.length
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<VAR>h : ¬a ∈ l<GOAL>(List.insert a l).length = l.length + 1
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<VAR>a : α<VAR>h : 0 < n<GOAL>List.insert a (List.replicate n a) = List.replicate n a
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>n : Nat<VAR>a b : α<VAR>h : (!b == a) = true<GOAL>List.insert b (List.replicate n a) = b :: List.replicate n a
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).erase a = l
<VAR>α : Type u_1<VAR>BEq α<VAR>a b : α<VAR>l : List α<VAR>h : ¬(b == a) = true<GOAL>(b :: l).erase a = b :: l.erase a
<VAR>α : Type u_1<VAR>BEq α<VAR>LawfulBEq α<VAR>a : α<VAR>l : List α<GOAL>¬a ∈ l → l.erase a = l
<VAR>α : Type u_1<VAR>BEq α<VAR>n : Nat<VAR>LawfulBEq α<VAR>a : α<GOAL>(List.replicate n a).erase a = List.replicate (n - 1) a
<VAR>α : Type u_1<VAR>BEq α<VAR>n : Nat<VAR>LawfulBEq α<VAR>a b : α<VAR>h : (!b == a) = true<GOAL>(List.replicate n a).erase b = List.replicate n a
<GOAL>∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), p a = true → List.find? p (a :: l) = some a
<GOAL>∀ {α : Type u_1} {p : α → Bool} {a : α} (l : List α), ¬p a = true → List.find? p (a :: l) = List.find? p l
<GOAL>∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.find? p l = none ↔ ∀ (x : α), x ∈ l → ¬p x = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → p a = true
<GOAL>∀ {α : Type u_1} {p : α → Bool} {a : α} {l : List α}, List.find? p l = some a → a ∈ l
<VAR>β : Type u_1<VAR>α : Type u_2<VAR>p : α → Bool<VAR>f : β → α<VAR>l : List β<GOAL>List.find? p (List.map f l) = Option.map f (List.find? (p ∘ f) l)
<GOAL>∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, List.find? p (List.replicate n a) = if n = 0 then none else if p a = true then some a else none
<VAR>n : Nat<GOAL>∀ {α : Type u_1} {p : α → Bool} {a : α}, 0 < n → List.find? p (List.replicate n a) = if p a = true then some a else none
<GOAL>∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, p a = true → List.find? p (List.replicate n a) = if n = 0 then none else some a
<GOAL>∀ {α : Type u_1} {p : α → Bool} {n : Nat} {a : α}, ¬p a = true → List.find? p (List.replicate n a) = none
<GOAL>∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {a : α} (l : List α), (f a).isSome = true → List.findSome? f (a :: l) = f a