ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → α<VAR>a : α<VAR>L : List (List β)<GOAL>List.foldl f a L.join = List.foldl (List.foldl f) a L
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>b : β<VAR>L : List (List α)<GOAL>List.foldr f b L.join = List.foldr (fun l b => List.foldr f b l) b L
<VAR>α : Type u<VAR>l : List α<GOAL>List.foldr List.cons [] l = l
<VAR>α : Type u<VAR>l : List α<GOAL>(List.foldl (fun t h => h :: t) [] l).reverse = l
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List ι<VAR>f : α → β → γ<VAR>op₁ : α → ι → α<VAR>op₂ : β → ι → β<VAR>op₃ : γ → ι → γ<VAR>a : α<VAR>b : β<VAR>h : ∀ (a : α) (b : β) (i : ι), f (op₁ a i) (op₂ b i) = op₃ (f a b) i<GOAL>List.foldl op₃ (f a b) l = f (List.foldl op₁ a l) (List.foldl op₂ b l)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l : List ι<VAR>f : α → β → γ<VAR>op₁ : ι → α → α<VAR>op₂ : ι → β → β<VAR>op₃ : ι → γ → γ<VAR>a : α<VAR>b : β<VAR>h : ∀ (a : α) (b : β) (i : ι), f (op₁ i a) (op₂ i b) = op₃ i (f a b)<GOAL>List.foldr op₃ (f a b) l = f (List.foldr op₁ a l) (List.foldr op₂ b l)
<VAR>α : Type u<VAR>l : List (α → α)<VAR>f : α → α<VAR>hl : ∀ (f : α → α), f ∈ l → Function.Injective f<VAR>hf : Function.Injective f<GOAL>Function.Injective (List.foldl Function.comp f l)
<VAR>α : Type u<VAR>β : Type v<VAR>C : β → Sort u_2<VAR>op : α → β → β<VAR>b : β<VAR>hb : C b<VAR>hl : (b : β) → C b → (a : α) → a ∈ [] → C (op a b)<GOAL>[].foldrRecOn op b hb hl = hb
<VAR>α : Type u<VAR>β : Type v<VAR>C : β → Sort u_2<VAR>x : α<VAR>l : List α<VAR>op : α → β → β<VAR>b : β<VAR>hb : C b<VAR>hl : (b : β) → C b → (a : α) → a ∈ x :: l → C (op a b)<GOAL>(x :: l).foldrRecOn op b hb hl = hl (List.foldr op b l) (l.foldrRecOn op b hb fun b hb a ha => hl b hb a ⋯) x ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>C : β → Sort u_2<VAR>op : β → α → β<VAR>b : β<VAR>hb : C b<VAR>hl : (b : β) → C b → (a : α) → a ∈ [] → C (op b a)<GOAL>[].foldlRecOn op b hb hl = hb
<VAR>α : Type u<VAR>x₁ x₂ z₁ z₂ : List α<VAR>a₁ a₂ : α<VAR>notin_x : ¬a₂ ∈ x₁<VAR>notin_z : ¬a₂ ∈ z₁<GOAL>x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>a : β<VAR>l : List α<GOAL>(List.scanl f a l).length = l.length + 1
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<GOAL>List.scanl f b [] = [b]
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>List.scanl f b (a :: l) = [b] ++ List.scanl f (f b a) l
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<GOAL>(List.scanl f b l)[0]? = some b
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<GOAL>(List.scanl f b l).get? 0 = some b
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>h : 0 < (List.scanl f b l).length<GOAL>(List.scanl f b l)[0] = b
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>h : 0 < (List.scanl f b l).length<GOAL>(List.scanl f b l).get ⟨0, h⟩ = b
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>h : 0 < (List.scanl f b l).length<GOAL>(List.scanl f b l).nthLe 0 h = b
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>i : ℕ<GOAL>(List.scanl f b l).get? (i + 1) = ((List.scanl f b l).get? i).bind fun x => Option.map (fun y => f x y) (l.get? i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>i : ℕ<VAR>h : i + 1 < (List.scanl f b l).length<GOAL>(List.scanl f b l).nthLe (i + 1) h = f ((List.scanl f b l).nthLe i ⋯) (l.nthLe i ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → α → β<VAR>b : β<VAR>l : List α<VAR>i : ℕ<VAR>h : i + 1 < (List.scanl f b l).length<GOAL>(List.scanl f b l).get ⟨i + 1, h⟩ = f ((List.scanl f b l).get ⟨i, ⋯⟩) (l.get ⟨i, ⋯⟩)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>b : β<GOAL>List.scanr f b [] = [b]
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>b : β<VAR>a : α<VAR>l : List α<GOAL>List.scanr f b (a :: l) = List.foldr f b (a :: l) :: List.scanr f b l
<VAR>α : Type u<VAR>f : α → α → α<VAR>hassoc : Associative f<VAR>a b : α<VAR>l : List α<GOAL>List.foldl f a (l ++ [b]) = List.foldr f b (a :: l)
<VAR>α : Type u<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a b : α<VAR>l : List α<GOAL>List.foldl f a (b :: l) = f b (List.foldl f a l)
<VAR>α : Type u<VAR>f : α → α → α<VAR>hcomm : Commutative f<VAR>hassoc : Associative f<VAR>a : α<VAR>l : List α<GOAL>List.foldl f a l = List.foldr f a l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → α<VAR>hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b<VAR>a : α<VAR>b : β<VAR>l : List β<GOAL>List.foldl f a (b :: l) = f (List.foldl f a l) b
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → α<VAR>hf : ∀ (a : α) (b c : β), f (f a b) c = f (f a c) b<VAR>a : α<VAR>l : List β<GOAL>List.foldl f a l = List.foldr (flip f) a l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β → β<VAR>hf : ∀ (a b : α) (c : β), f a (f b c) = f b (f a c)<VAR>a : β<VAR>b : α<VAR>l : List α<GOAL>List.foldr f a (b :: l) = List.foldr f (f b a) l
<VAR>α : Type u<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>List.foldl op (op a₁ a₂) l = op a₁ (List.foldl op a₂ l)
<VAR>α : Type u<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>op (List.foldl op a₁ l) a₂ = op a₁ (List.foldr (fun x x_1 => op x x_1) a₂ l)
<VAR>α : Type u<VAR>op : α → α → α<VAR>ha : Std.Associative op<VAR>hc : Std.Commutative op<VAR>l : List α<VAR>a₁ a₂ : α<GOAL>List.foldl op a₂ (a₁ :: l) = op a₁ (List.foldl op a₂ l)
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type v → Type w<VAR>Monad m<VAR>LawfulMonad m<VAR>f : α → β → m β<VAR>b : β<VAR>l : List α<GOAL>List.foldrM f b l = List.foldr (fun a mb => mb >>= f a) (pure b) l
<VAR>α : Type u<VAR>β : Type v<VAR>m : Type v → Type w<VAR>Monad m<VAR>LawfulMonad m<VAR>f : β → α → m β<VAR>b : β<VAR>l : List α<GOAL>List.foldlM f b l = List.foldl (fun mb a => do let b ← mb f b a) (pure b) l
<VAR>α : Type u<VAR>a b : α<GOAL>List.intersperse a [b] = [b]
<VAR>α : Type u<VAR>a b c : α<VAR>tl : List α<GOAL>List.intersperse a (b :: c :: tl) = b :: a :: List.intersperse a (c :: tl)
<VAR>α : Type u<VAR>n : ℕ<VAR>l xs : List α<VAR>acc : Array α<GOAL>List.splitAt.go l xs n acc = if n < xs.length then (acc.toList ++ List.take n xs, List.drop n xs) else (l, [])
<VAR>α : Type u<VAR>n : ℕ<VAR>l : List α<GOAL>List.splitAt n l = (List.take n l, List.drop n l)
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<GOAL>List.splitOn a [] = [[]]
<VAR>α : Type u<VAR>p : α → Bool<GOAL>List.splitOnP p [] = [[]]
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs acc : List α<GOAL>List.splitOnP.go p xs acc ≠ []
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs acc : List α<GOAL>List.splitOnP.go p xs acc = List.modifyHead (fun x => acc.reverse ++ x) (List.splitOnP p xs)
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<GOAL>List.splitOnP p xs ≠ []
<VAR>α : Type u<VAR>p : α → Bool<VAR>x : α<VAR>xs : List α<GOAL>List.splitOnP p (x :: xs) = if p x = true then [] :: List.splitOnP p xs else List.modifyHead (List.cons x) (List.splitOnP p xs)
<VAR>α : Type u<VAR>xs ys : List (List α)<VAR>a : α<VAR>hxs : xs ≠ []<VAR>hys : ys ≠ []<GOAL>(List.zipWith (fun x x_1 => x ++ x_1) (List.modifyHead (List.cons a) xs) ys).join = a :: (List.zipWith (fun x x_1 => x ++ x_1) xs ys).join
<VAR>α : Type u<VAR>p : α → Bool<VAR>as : List α<GOAL>(List.zipWith (fun x x_1 => x ++ x_1) (List.splitOnP p as) (List.map (fun x => [x]) (List.filter p as) ++ [[]])).join = as
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>h : ∀ (x : α), x ∈ xs → ¬p x = true<GOAL>List.splitOnP p xs = [xs]
<VAR>α : Type u<VAR>p : α → Bool<VAR>xs : List α<VAR>h : ∀ (x : α), x ∈ xs → ¬p x = true<VAR>sep : α<VAR>hsep : p sep = true<VAR>as : List α<GOAL>List.splitOnP p (xs ++ sep :: as) = xs :: List.splitOnP p as
<VAR>α : Type u<VAR>xs : List α<VAR>x : α<VAR>DecidableEq α<GOAL>[x].intercalate (List.splitOn x xs) = xs
<VAR>α : Type u<VAR>ls : List (List α)<VAR>DecidableEq α<VAR>x : α<VAR>hx : ∀ (l : List α), l ∈ ls → ¬x ∈ l<VAR>hls : ls ≠ []<GOAL>List.splitOn x ([x].intercalate ls) = ls
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<VAR>tl : List α<VAR>r : Array α<GOAL>List.modifyLast.go f (tl ++ [a]) r = r.toListAppend (List.modifyLast.go f (tl ++ [a]) #[])
<VAR>α : Type u<VAR>f : α → α<VAR>a : α<VAR>l : List α<GOAL>List.modifyLast f (l ++ [a]) = l ++ [f a]
<VAR>α : Type u<VAR>f : α → α<VAR>l₁ l₂ : List α<GOAL>l₂ ≠ [] → List.modifyLast f (l₁ ++ l₂) = l₁ ++ List.modifyLast f l₂
<VAR>α : Type u<VAR>SizeOf α<VAR>x : α<VAR>l : List α<VAR>hx : x ∈ l<GOAL>sizeOf x < sizeOf l
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : α → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>List.pmap (fun a x => f a) l H = List.map f l
<VAR>α : Type u<VAR>β : Type v<VAR>p q : α → Prop<VAR>f : (a : α) → p a → β<VAR>g : (a : α) → q a → β<VAR>l : List α<VAR>H₁ : ∀ (a : α), a ∈ l → p a<VAR>H₂ : ∀ (a : α), a ∈ l → q a<VAR>h : ∀ (a : α), a ∈ l → ∀ (h₁ : p a) (h₂ : q a), f a h₁ = g a h₂<GOAL>List.pmap f l H₁ = List.pmap g l H₂
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>p : α → Prop<VAR>g : β → γ<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>List.map g (List.pmap f l H) = List.pmap (fun a h => g (f a h)) l H
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>p : β → Prop<VAR>g : (b : β) → p b → γ<VAR>f : α → β<VAR>l : List α<VAR>H : ∀ (a : β), a ∈ List.map f l → p a<GOAL>List.pmap g (List.map f l) H = List.pmap (fun a h => g (f a) h) l ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>List.pmap f l H = List.map (fun x => f ↑x ⋯) l.attach
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>f : α → β<GOAL>List.map (fun i => f ↑i) l.attach = List.map f l
<VAR>α : Type u<VAR>l : List α<GOAL>List.map Subtype.val l.attach = l
<VAR>α : Type u<VAR>l : List α<VAR>x : { x // x ∈ l }<GOAL>x ∈ l.attach
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<VAR>b : β<GOAL>b ∈ List.pmap f l H ↔ ∃ a h, f a ⋯ = b
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>(List.pmap f l H).length = l.length
<VAR>α : Type u<VAR>L : List α<GOAL>L.attach.length = L.length
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → p a<GOAL>List.pmap f l H = [] ↔ l = []
<VAR>α : Type u<VAR>l : List α<GOAL>l.attach = [] ↔ l = []
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>hl₁ : ∀ (a : α), a ∈ l → p a<VAR>hl₂ : l ≠ []<GOAL>(List.pmap f l hl₁).getLast ⋯ = f (l.getLast hl₂) ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<GOAL>(List.pmap f l h)[n]? = Option.pmap f l[n]? ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<GOAL>(List.pmap f l h).get? n = Option.pmap f (l.get? n) ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<VAR>hn : n < (List.pmap f l h).length<GOAL>(List.pmap f l h)[n] = f l[n] ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<VAR>hn : n < (List.pmap f l h).length<GOAL>(List.pmap f l h).get ⟨n, hn⟩ = f (l.get ⟨n, ⋯⟩) ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<VAR>hn : n < (List.pmap f l h).length<GOAL>(List.pmap f l h).nthLe n hn = f (l.nthLe n ⋯) ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>p : ι → Prop<VAR>f : (a : ι) → p a → α<VAR>l₁ l₂ : List ι<VAR>h : ∀ (a : ι), a ∈ l₁ ++ l₂ → p a<GOAL>List.pmap f (l₁ ++ l₂) h = List.pmap f l₁ ⋯ ++ List.pmap f l₂ ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l₁ l₂ : List α<VAR>h₁ : ∀ (a : α), a ∈ l₁ → p a<VAR>h₂ : ∀ (a : α), a ∈ l₂ → p a<GOAL>List.pmap f (l₁ ++ l₂) ⋯ = List.pmap f l₁ h₁ ++ List.pmap f l₂ h₂
<VAR>α : Type u<VAR>f : α → Option α<VAR>l : List α<VAR>acc : Array α<GOAL>List.lookmap.go f l acc = acc.toListAppend (List.lookmap f l)
<VAR>α : Type u<VAR>f : α → Option α<GOAL>List.lookmap f [] = []
<VAR>α : Type u<VAR>f : α → Option α<VAR>a : α<VAR>l : List α<VAR>h : f a = none<GOAL>List.lookmap f (a :: l) = a :: List.lookmap f l
<VAR>α : Type u<VAR>f : α → Option α<VAR>a b : α<VAR>l : List α<VAR>h : f a = some b<GOAL>List.lookmap f (a :: l) = b :: l
<VAR>α : Type u<VAR>l : List α<GOAL>List.lookmap some l = l
<VAR>α : Type u<VAR>l : List α<GOAL>List.lookmap (fun x => none) l = l
<VAR>α : Type u<VAR>f g : α → Option α<VAR>l : List α<GOAL>(∀ (a : α), a ∈ l → f a = g a) → List.lookmap f l = List.lookmap g l
<VAR>α : Type u<VAR>f : α → Option α<VAR>l : List α<VAR>H : ∀ (a : α), a ∈ l → f a = none<GOAL>List.lookmap f l = l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Option α<VAR>g : α → β<VAR>h : ∀ (a b : α), b ∈ f a → g a = g b<VAR>l : List α<GOAL>List.map g (List.lookmap f l) = List.map g l
<VAR>α : Type u<VAR>f : α → Option α<VAR>h : ∀ (a b : α), b ∈ f a → a = b<VAR>l : List α<GOAL>List.lookmap f l = l
<VAR>α : Type u<VAR>f : α → Option α<VAR>l : List α<GOAL>(List.lookmap f l).length = l.length
<VAR>α : Type u<VAR>l : List α<VAR>f : α → Bool<GOAL>l.length = (List.filter f l).length + (List.filter (fun x => !f x) l).length
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>l₁ l₂ : List α<VAR>s : l₁.Sublist l₂<GOAL>(List.map f l₁).Sublist (List.map f l₂)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Option β<VAR>l : List α<GOAL>List.filterMap f l = l.bind fun a => (f a).toList
<VAR>α : Type u<VAR>β : Type v<VAR>f g : α → Option β<VAR>l : List α<VAR>h : ∀ (x : α), x ∈ l → f x = g x<GOAL>List.filterMap f l = List.filterMap g l
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → Option β<VAR>g : α → β<VAR>l : List α<GOAL>List.filterMap f l = List.map g l ↔ ∀ (x : α), x ∈ l → f x = some (g x)
<VAR>α : Type u<VAR>p : α → Bool<VAR>a : α<GOAL>List.filter p [a] = bif p a then [a] else []
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.filter p l = List.foldr (fun a out => bif p a then a :: out else out) [] l
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.filter p l ⊆ l
<VAR>α : Type u<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : a ∈ List.filter p l<GOAL>p a = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h : a ∈ List.filter p l<GOAL>a ∈ l
<VAR>α : Type u<VAR>p : α → Bool<VAR>a : α<VAR>l : List α<VAR>h₁ : a ∈ l<VAR>h₂ : p a = true<GOAL>a ∈ List.filter p l
<VAR>α : Type u<VAR>p : α → Bool<VAR>l l' : List α<VAR>h : l ⊆ l'<GOAL>List.filter p l ⊆ List.filter p l'
<VAR>α : Type u<VAR>l : List α<VAR>p q : α → Bool<VAR>h : ∀ (a : α), p a = true → q a = true<GOAL>(List.filter p l).Sublist (List.filter q l)
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Bool<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>l : List α<VAR>DecidablePred fun b => ∃ a, p a = true ∧ f a = b<GOAL>List.map f (List.filter p l) = List.filter (fun b => decide (∃ a, p a = true ∧ f a = b)) (List.map f l)
<VAR>α : Type u<VAR>l : List α<VAR>p : { a // a ∈ l } → Bool<VAR>DecidableEq α<GOAL>List.filter p l.attach = List.map (Subtype.map id ⋯) (List.filter (fun x => decide (∃ h, p ⟨x, h⟩ = true)) l).attach
<VAR>α : Type u<VAR>l : List α<VAR>p : α → Bool<GOAL>List.filter (fun x => p ↑x) l.attach = List.map (Subtype.map id ⋯) (List.filter p l).attach
<VAR>α : Type u<VAR>p q : α → Bool<VAR>l : List α<GOAL>List.filter p (List.filter q l) = List.filter q (List.filter p l)
<VAR>α : Type u<VAR>l : List α<GOAL>List.filter (fun x => true) l = l
<VAR>α : Type u<VAR>l : List α<GOAL>List.filter (fun x => false) l = []
<VAR>α : Type u<VAR>p : α → Bool<VAR>l₁ l₂ : List α<GOAL>List.span.loop p l₁ l₂ = (l₂.reverse ++ List.takeWhile p l₁, List.dropWhile p l₁)
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.span p l = (List.takeWhile p l, List.dropWhile p l)
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>hl : 0 < (List.dropWhile p l).length<GOAL>¬p ((List.dropWhile p l).nthLe 0 hl) = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.dropWhile p l = [] ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : p x = true<GOAL>List.takeWhile p (x :: l) = x :: List.takeWhile p l
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>h : ¬p x = true<GOAL>List.takeWhile p (x :: l) = []
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.takeWhile p l = l ↔ ∀ (x : α), x ∈ l → p x = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.takeWhile p l = [] ↔ ∀ (hl : 0 < l.length), ¬p (l.nthLe 0 hl) = true
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>x : α<VAR>hx : x ∈ List.takeWhile p l<GOAL>p x = true
<VAR>α : Type u<VAR>p q : α → Bool<VAR>l : List α<GOAL>List.takeWhile p (List.takeWhile q l) = List.takeWhile (fun a => decide (p a = true ∧ q a = true)) l
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<GOAL>List.takeWhile p (List.takeWhile p l) = List.takeWhile p l
<VAR>α : Type u<VAR>p : α → Bool<VAR>l : List α<VAR>a : α<VAR>al : a ∈ l<VAR>pa : p a = true<GOAL>(List.eraseP p l).length + 1 = l.length
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l : List α<VAR>h : a ∈ l<GOAL>(l.erase a).length + 1 = l.length
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>finj : Function.Injective f<VAR>a : α<VAR>l : List α<GOAL>List.map f (l.erase a) = (List.map f l).erase (f a)
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>finj : Function.Injective f<VAR>l₁ l₂ : List α<GOAL>List.map f (List.foldl List.erase l₁ l₂) = List.foldl (fun l a => l.erase (f a)) (List.map f l₁) l₂
<VAR>ι : Type u_1<VAR>DecidableEq ι<VAR>l : List ι<VAR>i : Fin l.length<GOAL>(l.erase (l.get i)).Perm (l.eraseIdx ↑i)
<VAR>ι : Type u_1<VAR>l : List ι<VAR>i : ℕ<VAR>h : i < l.length<GOAL>(l.eraseIdx i).length + 1 = l.length
<VAR>α : Type u<VAR>β : Type v<VAR>DecidableEq α<VAR>DecidableEq β<VAR>f : α → β<VAR>finj : Function.Injective f<VAR>l₁ l₂ : List α<GOAL>List.map f (l₁.diff l₂) = (List.map f l₁).diff (List.map f l₂)
<VAR>α : Type u<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List α<GOAL>l₁.Sublist l₂ → ((l₂.erase a).diff (l₁.erase a)).Sublist (l₂.diff l₁)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<VAR>hp : ∃ a, a ∈ l ∧ p a<GOAL>List.choose p l hp ∈ l ∧ p (List.choose p l hp)
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<VAR>hp : ∃ a, a ∈ l ∧ p a<GOAL>List.choose p l hp ∈ l
<VAR>α : Type u<VAR>p : α → Prop<VAR>DecidablePred p<VAR>l : List α<VAR>hp : ∃ a, a ∈ l ∧ p a<GOAL>p (List.choose p l hp)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Option β → γ<VAR>as : List α<GOAL>List.map₂Left' f as [] = (List.map (fun a => f a none) as, [])
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>bs : List β<GOAL>List.map₂Right' f [] bs = (List.map (f none) bs, [])
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>as : List α<GOAL>List.map₂Right' f as [] = ([], as)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>b : β<VAR>bs : List β<GOAL>List.map₂Right' f [] (b :: bs) = (f none b :: List.map (f none) bs, [])
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>List.map₂Right' f (a :: as) (b :: bs) = let r := List.map₂Right' f as bs; (f (some a) b :: r.1, r.2)
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<GOAL>as.zipLeft' [] = (List.map (fun a => (a, none)) as, [])
<VAR>α : Type u<VAR>β : Type v<VAR>bs : List β<GOAL>[].zipLeft' bs = ([], bs)
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<GOAL>(a :: as).zipLeft' [] = ((a, none) :: List.map (fun a => (a, none)) as, [])
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>(a :: as).zipLeft' (b :: bs) = let r := as.zipLeft' bs; ((a, some b) :: r.1, r.2)
<VAR>α : Type u<VAR>β : Type v<VAR>bs : List β<GOAL>[].zipRight' bs = (List.map (fun b => (none, b)) bs, [])
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<GOAL>as.zipRight' [] = ([], as)
<VAR>α : Type u<VAR>β : Type v<VAR>b : β<VAR>bs : List β<GOAL>[].zipRight' (b :: bs) = ((none, b) :: List.map (fun b => (none, b)) bs, [])
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>(a :: as).zipRight' (b :: bs) = let r := as.zipRight' bs; ((some a, b) :: r.1, r.2)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Option β → γ<VAR>as : List α<GOAL>List.map₂Left f as [] = List.map (fun a => f a none) as
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<GOAL>List.map₂Left f as bs = (List.map₂Left' f as bs).1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : α → Option β → γ<VAR>as : List α<VAR>bs : List β<GOAL>as.length ≤ bs.length → List.map₂Left f as bs = List.zipWith (fun a b => f a (some b)) as bs
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>bs : List β<GOAL>List.map₂Right f [] bs = List.map (f none) bs
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>as : List α<GOAL>List.map₂Right f as [] = []
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>b : β<VAR>bs : List β<GOAL>List.map₂Right f [] (b :: bs) = f none b :: List.map (f none) bs
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>List.map₂Right f (a :: as) (b :: bs) = f (some a) b :: List.map₂Right f as bs
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>as : List α<VAR>bs : List β<GOAL>List.map₂Right f as bs = (List.map₂Right' f as bs).1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : Option α → β → γ<VAR>as : List α<VAR>bs : List β<VAR>h : bs.length ≤ as.length<GOAL>List.map₂Right f as bs = List.zipWith (fun a b => f (some a) b) as bs
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<GOAL>as.zipLeft [] = List.map (fun a => (a, none)) as
<VAR>α : Type u<VAR>β : Type v<VAR>bs : List β<GOAL>[].zipLeft bs = []
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<GOAL>(a :: as).zipLeft [] = (a, none) :: List.map (fun a => (a, none)) as
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>(a :: as).zipLeft (b :: bs) = (a, some b) :: as.zipLeft bs
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<VAR>bs : List β<GOAL>as.zipLeft bs = (as.zipLeft' bs).1
<VAR>α : Type u<VAR>β : Type v<VAR>bs : List β<GOAL>[].zipRight bs = List.map (fun b => (none, b)) bs
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<GOAL>as.zipRight [] = []
<VAR>α : Type u<VAR>β : Type v<VAR>b : β<VAR>bs : List β<GOAL>[].zipRight (b :: bs) = (none, b) :: List.map (fun b => (none, b)) bs
<VAR>α : Type u<VAR>β : Type v<VAR>a : α<VAR>as : List α<VAR>b : β<VAR>bs : List β<GOAL>(a :: as).zipRight (b :: bs) = (some a, b) :: as.zipRight bs
<VAR>α : Type u<VAR>β : Type v<VAR>as : List α<VAR>bs : List β<GOAL>as.zipRight bs = (as.zipRight' bs).1
<VAR>α : Type u<VAR>p : α → Prop<VAR>x : α<VAR>l : List α<GOAL>List.Forall p (x :: l) ↔ p x ∧ List.Forall p l
<VAR>α : Type u<VAR>p : α → Prop<VAR>l : List α<GOAL>List.Forall p l ↔ ∀ (x : α), x ∈ l → p x
<VAR>α : Type u<VAR>p q : α → Prop<VAR>h : ∀ (x : α), p x → q x<VAR>l : List α<GOAL>List.Forall p l → List.Forall q l
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>p : β → Prop<VAR>f : α → β<GOAL>List.Forall p (List.map f l) ↔ List.Forall (p ∘ f) l
<VAR>α : Type u<VAR>l : List α<VAR>hl : l.reverse ≠ []<VAR>hl' : 0 < l.length := ⋯<GOAL>l.reverse.getLast hl = l.get ⟨0, hl'⟩
<VAR>α : Type u<VAR>L : List α<VAR>i : ℕ<VAR>h : i < L.attach.length<GOAL>↑L.attach[i] = L[i]
<VAR>α : Type u<VAR>L : List α<VAR>i : Fin L.attach.length<GOAL>↑(L.attach.get i) = L.get ⟨↑i, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>x : α<VAR>y : β<VAR>xs : List (α × β)<GOAL>(y, x) ∈ List.map Prod.swap xs ↔ (x, y) ∈ xs
<VAR>α : Type u<VAR>xs : List α<VAR>n m : ℕ<GOAL>List.dropSlice n m xs = List.take n xs ++ List.drop (n + m) xs
<VAR>α : Type u<VAR>i j : ℕ<VAR>xs : List α<GOAL>(List.dropSlice i j xs).length = xs.length - min j (xs.length - i)