ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>y : β<VAR>ys : List β<GOAL>∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys ≤ levenshtein C xs (y :: ys)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>∃ xs', xs' <:+ xs ∧ levenshtein C xs' ys₂ ≤ levenshtein C xs (ys₁ ++ ys₂)
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<VAR>o : Option α<GOAL>List.foldl (List.argAux r) o l = none ↔ l = [] ∧ o = none
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<VAR>a m : α<GOAL>m ∈ List.foldl (List.argAux r) (some a) l → m ∈ a :: l
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>hr₀ : Irreflexive r<VAR>a : α<GOAL>List.argAux r (some a) a = some a
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>DecidableRel r<VAR>l : List α<VAR>hr₀ : Irreflexive r<VAR>hr₁ : Transitive r<VAR>a m : α<VAR>o : Option α<GOAL>a ∈ l → m ∈ List.foldl (List.argAux r) o l → ¬r a m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<GOAL>List.argmax f [] = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<GOAL>List.argmin f [] = none
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>a : α<GOAL>List.argmax f [a] = some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>a : α<GOAL>List.argmin f [a] = some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → m ∈ List.argmax f l → ¬f m < f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → m ∈ List.argmin f l → ¬f a < f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.argmax f (l ++ [a]) = Option.casesOn (List.argmax f l) (some a) fun c => if f c < f a then some a else some c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.argmin f (l ++ [a]) = Option.casesOn (List.argmin f l) (some a) fun c => if f a < f c then some a else some c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<VAR>m : α<GOAL>m ∈ List.argmax f l → m ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<VAR>m : α<GOAL>m ∈ List.argmin f l → m ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<GOAL>List.argmax f l = none ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Preorder β<VAR>DecidableRel fun x x_1 => x < x_1<VAR>f : α → β<VAR>l : List α<GOAL>List.argmin f l = none ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → m ∈ List.argmax f l → f a ≤ f m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → m ∈ List.argmin f l → f m ≤ f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.argmax f (a :: l) = Option.casesOn (List.argmax f l) (some a) fun c => if f a < f c then some c else some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>a : α<VAR>l : List α<GOAL>List.argmin f (a :: l) = Option.casesOn (List.argmin f l) (some a) fun c => if f c < f a then some c else some a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>DecidableEq α<VAR>l : List α<VAR>m : α<GOAL>m ∈ List.argmax f l → ∀ {a : α}, a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>DecidableEq α<VAR>l : List α<VAR>m : α<GOAL>m ∈ List.argmin f l → ∀ {a : α}, a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>m : α<VAR>DecidableEq α<GOAL>m ∈ List.argmax f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>m : α<VAR>DecidableEq α<GOAL>List.argmax f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f a ≤ f m) ∧ ∀ (a : α), a ∈ l → f m ≤ f a → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>m : α<VAR>DecidableEq α<GOAL>m ∈ List.argmin f l ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>LinearOrder β<VAR>f : α → β<VAR>l : List α<VAR>m : α<VAR>DecidableEq α<GOAL>List.argmin f l = some m ↔ m ∈ l ∧ (∀ (a : α), a ∈ l → f m ≤ f a) ∧ ∀ (a : α), a ∈ l → f a ≤ f m → List.indexOf m l ≤ List.indexOf a l
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<GOAL>[].maximum = ⊥
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<GOAL>[].minimum = ⊤
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>[a].maximum = ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>a : α<GOAL>[a].minimum = ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>m : α<GOAL>l.maximum = ↑m → m ∈ l
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>m : α<GOAL>l.minimum = ↑m → m ∈ l
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<GOAL>l.maximum = ⊥ ↔ l = []
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<GOAL>l.maximum = none ↔ l = []
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<GOAL>l.minimum = ⊤ ↔ l = []
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<GOAL>l.minimum = none ↔ l = []
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → l.maximum = ↑m → ¬m < a
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → l.minimum = ↑m → ¬a < m
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>a : α<VAR>ha : a ∈ l<GOAL>¬l.maximum < ↑a
<VAR>α : Type u_1<VAR>Preorder α<VAR>DecidableRel fun x x_1 => x < x_1<VAR>l : List α<VAR>a : α<VAR>ha : a ∈ l<GOAL>¬↑a < l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>l : List α<GOAL>(l ++ [a]).maximum = max l.maximum ↑a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → l.maximum = ↑m → a ≤ m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>a ∈ l → l.minimum = ↑m → m ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<VAR>ha : a ∈ l<GOAL>↑a ≤ l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<VAR>ha : a ∈ l<GOAL>l.minimum ≤ ↑a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>l : List α<GOAL>(l ++ [a]).minimum = min l.minimum ↑a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).maximum = max (↑a) l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>a : α<VAR>l : List α<GOAL>(a :: l).minimum = min (↑a) l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>b : WithBot α<VAR>h : ∀ (a : α), a ∈ l → ↑a ≤ b<GOAL>l.maximum ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>b : WithTop α<VAR>h : ∀ (a : α), a ∈ l → b ≤ ↑a<GOAL>b ≤ l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>m : α<GOAL>l.maximum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ m
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>m : α<GOAL>l.minimum = ↑m ↔ m ∈ l ∧ ∀ (a : α), a ∈ l → m ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<GOAL>↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<GOAL>l.minimum ≤ ↑a ↔ ∃ b, b ∈ l ∧ b ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.maximum ≠ ⊥
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.minimum ≠ ⊤
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>l.maximum ≠ ⊥
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>l.minimum ≠ ⊤
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>↑(List.maximum_of_length_pos h) = l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>↑(List.minimum_of_length_pos h) = l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>b : α<VAR>h : 0 < l.length<GOAL>b ≤ List.maximum_of_length_pos h ↔ ↑b ≤ l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>b : α<VAR>h : 0 < l.length<GOAL>List.minimum_of_length_pos h ≤ b ↔ l.minimum ≤ ↑b
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>List.maximum_of_length_pos h ∈ l
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>h : 0 < l.length<GOAL>List.minimum_of_length_pos h ∈ l
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<VAR>h : a ∈ l<VAR>w : 0 < l.length<GOAL>a ≤ List.maximum_of_length_pos w
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>a : α<VAR>h : a ∈ l<VAR>w : 0 < l.length<GOAL>List.minimum_of_length_pos w ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>i : ℕ<VAR>w : i < l.length<VAR>h : 0 < l.length := ⋯<GOAL>l[i] ≤ List.maximum_of_length_pos h
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>i : ℕ<VAR>w : i < l.length<VAR>h : 0 < l.length := ⋯<GOAL>List.minimum_of_length_pos h ≤ l[i]
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>d : α<GOAL>l.maximum?.getD d = WithBot.unbot' d l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>l : List α<VAR>d : α<GOAL>l.minimum?.getD d = WithTop.untop' d l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderBot α<VAR>l : List α<VAR>h : l ≠ []<GOAL>↑(List.foldr max ⊥ l) = l.maximum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderBot α<VAR>l : List α<VAR>a : α<VAR>h : ∀ (x : α), x ∈ l → x ≤ a<GOAL>List.foldr max ⊥ l ≤ a
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderBot α<VAR>l : List α<VAR>a x : α<VAR>hx : x ∈ l<VAR>h : a ≤ x<GOAL>a ≤ List.foldr max ⊥ l
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderTop α<VAR>l : List α<VAR>h : l ≠ []<GOAL>↑(List.foldr min ⊤ l) = l.minimum
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderTop α<VAR>l : List α<VAR>a : α<VAR>h : ∀ (x : α), x ∈ l → a ≤ x<GOAL>a ≤ List.foldr min ⊤ l
<VAR>α : Type u_1<VAR>LinearOrder α<VAR>OrderTop α<VAR>l : List α<VAR>a : α<VAR>x : α<VAR>hx : x ∈ l<VAR>h : x ≤ a<GOAL>List.foldr min ⊤ l ≤ a
<VAR>α : Type u_1<VAR>β δ : Type<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>ys : List β<VAR>self : LevenshteinEstimator' C xs ys<GOAL>self.bound = match self.pre_rev, ⋯ with | [], split => ((↑self.distances)[0], ys.length) | x, split => (List.minimum_of_length_pos ⋯, self.suff.length)
<VAR>α : Type u_1<VAR>β δ : Type<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>ys : List β<VAR>self : LevenshteinEstimator' C xs ys<GOAL>self.pre_rev.reverse ++ self.suff = ys
<VAR>α : Type u_1<VAR>β δ : Type<VAR>CanonicallyLinearOrderedAddCommMonoid δ<VAR>C : Levenshtein.Cost α β δ<VAR>xs : List α<VAR>ys : List β<VAR>self : LevenshteinEstimator' C xs ys<GOAL>self.distances = suffixLevenshtein C xs self.suff
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate (n % l.length) = l.rotate n
<VAR>α : Type u<VAR>n : ℕ<GOAL>[].rotate n = []
<VAR>α : Type u<VAR>l : List α<GOAL>l.rotate 0 = l
<VAR>α : Type u<VAR>n : ℕ<GOAL>[].rotate' n = []
<VAR>α : Type u<VAR>l : List α<GOAL>l.rotate' 0 = l
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<GOAL>(a :: l).rotate' n.succ = (l ++ [a]).rotate' n
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate' n).length = l.length
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>n ≤ l.length → l.rotate' n = List.drop n l ++ List.take n l
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<GOAL>(l.rotate' n).rotate' m = l.rotate' (n + m)
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate' (l.length * n) = l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate' (n % l.length) = l.rotate' n
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n = l.rotate' n
<VAR>α : Type u<VAR>l : List α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ l.rotate n ↔ a ∈ l
<VAR>α : Type u<VAR>a : α<VAR>n k : ℕ<GOAL>(List.replicate n a).rotate k = List.replicate n a
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>n ≤ l.length → l.rotate n = List.drop n l ++ List.take n l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n = List.drop (n % l.length) l ++ List.take (n % l.length) l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate n).Perm l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>(l.rotate n).Nodup ↔ l.Nodup
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n = [] ↔ l = []
<VAR>α : Type u<VAR>x : α<VAR>n : ℕ<GOAL>[x].rotate n = [x]
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>f : α → β → γ<VAR>l : List α<VAR>l' : List β<VAR>n : ℕ<VAR>h : l.length = l'.length<GOAL>(List.zipWith f l l').rotate n = List.zipWith f (l.rotate n) (l'.rotate n)
<VAR>α : Type u<VAR>β : Type u_1<VAR>f : α → α → β<VAR>x y : α<VAR>l : List α<GOAL>List.zipWith f (x :: y :: l) ((x :: y :: l).rotate 1) = f x y :: List.zipWith f (y :: l) (l ++ [x])
<VAR>α : Type u<VAR>l : List α<VAR>n k : ℕ<VAR>hk : k < (l.rotate n).length<GOAL>(l.rotate n).nthLe k hk = l.nthLe ((k + n) % l.length) ⋯
<VAR>α : Type u<VAR>l : List α<VAR>k : ℕ<VAR>hk : k < (l.rotate 1).length<GOAL>(l.rotate 1).nthLe k hk = l.nthLe ((k + 1) % l.length) ⋯
<VAR>α : Type u<VAR>l : List α<VAR>n k : ℕ<VAR>hk : k < l.length<GOAL>(l.rotate n).nthLe ((l.length - n % l.length + k) % l.length) ⋯ = l.nthLe k hk
<VAR>α : Type u<VAR>hα : Nonempty α<VAR>l : List α<GOAL>(∀ (n : ℕ), l.rotate n = l) ↔ ∃ a, l = List.replicate l.length a
<VAR>α : Type u<VAR>Nonempty α<VAR>l : List α<GOAL>l.rotate 1 = l ↔ ∃ a, l = List.replicate l.length a
<VAR>α : Type u<VAR>n : ℕ<GOAL>Function.Injective fun l => l.rotate n
<VAR>α : Type u<VAR>l l' : List α<VAR>n : ℕ<GOAL>l.rotate n = l'.rotate n ↔ l = l'
<VAR>α : Type u<VAR>β : Type u_1<VAR>f : α → β<VAR>l : List α<VAR>n : ℕ<GOAL>List.map f (l.rotate n) = (List.map f l).rotate n
<VAR>α : Type u<VAR>l : List α<GOAL>l ~r l
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<GOAL>l' ~r l
<VAR>α : Type u<VAR>l l' : List α<GOAL>l ~r l' ↔ l' ~r l
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<GOAL>l.rotate n ~r l
<VAR>α : Type u<VAR>l l' l'' : List α<GOAL>l ~r l' → l' ~r l'' → l ~r l''
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<GOAL>l.Perm l'
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<GOAL>l.Nodup ↔ l'.Nodup
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<VAR>a : α<GOAL>a ∈ l ↔ a ∈ l'
<VAR>α : Type u<VAR>l : List α<GOAL>l ~r [] ↔ l = []
<VAR>α : Type u<VAR>l : List α<GOAL>[] ~r l ↔ [] = l
<VAR>α : Type u<VAR>l : List α<VAR>x : α<GOAL>l ~r [x] ↔ l = [x]
<VAR>α : Type u<VAR>l : List α<VAR>x : α<GOAL>[x] ~r l ↔ [x] = l
<VAR>α : Type u<VAR>hd : α<VAR>tl : List α<GOAL>(tl ++ [hd]) ~r (hd :: tl)
<VAR>α : Type u<VAR>l l' : List α<GOAL>(l ++ l') ~r (l' ++ l)
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<GOAL>l.reverse ~r l'.reverse
<VAR>α : Type u<VAR>l l' : List α<GOAL>l.reverse ~r l' ↔ l ~r l'.reverse
<VAR>α : Type u<VAR>l l' : List α<GOAL>l.reverse ~r l'.reverse ↔ l ~r l'
<VAR>α : Type u<VAR>l l' : List α<GOAL>l ~r l' ↔ ∃ n ≤ l.length, l.rotate n = l'
<VAR>α : Type u<VAR>l l' : List α<GOAL>l ~r l' ↔ l' ∈ List.map l.rotate (List.range (l.length + 1))
<VAR>α : Type u<VAR>β : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ ~r l₂<VAR>f : α → β<GOAL>List.map f l₁ ~r List.map f l₂
<VAR>α : Type u<GOAL>[].cyclicPermutations = [[]]
<VAR>α : Type u<VAR>x : α<VAR>l : List α<GOAL>(x :: l).cyclicPermutations = (List.zipWith (fun x x_1 => x ++ x_1) (x :: l).tails (x :: l).inits).dropLast
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.cyclicPermutations = (List.zipWith (fun x x_1 => x ++ x_1) l.tails l.inits).dropLast
<VAR>α : Type u<VAR>x : α<VAR>l : List α<GOAL>(x :: l).cyclicPermutations.length = l.length + 1
<VAR>α : Type u<VAR>l : List α<VAR>h : l ≠ []<GOAL>l.cyclicPermutations.length = l.length
<VAR>α : Type u<VAR>l : List α<GOAL>l.cyclicPermutations ≠ []
<VAR>α : Type u<VAR>l : List α<VAR>n : ℕ<VAR>h : n < l.cyclicPermutations.length<GOAL>l.cyclicPermutations[n] = l.rotate n
<VAR>α : Type u<VAR>l : List α<VAR>n : Fin l.cyclicPermutations.length<GOAL>l.cyclicPermutations.get n = l.rotate ↑n
<VAR>α : Type u<VAR>l : List α<GOAL>l.cyclicPermutations.head ⋯ = l
<VAR>α : Type u<VAR>l : List α<GOAL>l.cyclicPermutations.head? = some l
<VAR>α : Type u<GOAL>Function.Injective List.cyclicPermutations
<VAR>α : Type u<VAR>l l' : List α<GOAL>l.cyclicPermutations = l'.cyclicPermutations ↔ l = l'
<VAR>α : Type u<VAR>l' : List α<VAR>l : List α<VAR>h : l' ∈ l.cyclicPermutations<GOAL>l'.length = l.length
<VAR>α : Type u<VAR>l : List α<GOAL>l ∈ l.cyclicPermutations
<VAR>α : Type u<VAR>l : List α<VAR>k : ℕ<GOAL>(l.rotate k).cyclicPermutations = l.cyclicPermutations.rotate k
<VAR>α : Type u<VAR>l l' : List α<GOAL>l ∈ l'.cyclicPermutations ↔ l ~r l'
<VAR>α : Type u<VAR>l : List α<GOAL>l.cyclicPermutations = [[]] ↔ l = []
<VAR>α : Type u<VAR>l : List α<VAR>x : α<GOAL>l.cyclicPermutations = [[x]] ↔ l = [x]
<VAR>α : Type u<VAR>l : List α<VAR>hn : l.Nodup<GOAL>l.cyclicPermutations.Nodup
<VAR>α : Type u<VAR>l l' : List α<VAR>h : l ~r l'<GOAL>l.cyclicPermutations ~r l'.cyclicPermutations
<VAR>α : Type u<VAR>l l' : List α<GOAL>l.cyclicPermutations ~r l'.cyclicPermutations ↔ l ~r l'
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.destutter' R a [] = [a]
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<GOAL>List.destutter' R a (b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<VAR>h : R b a<GOAL>List.destutter' R b (a :: l) = b :: List.destutter' R a l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<VAR>h : ¬R b a<GOAL>List.destutter' R b (a :: l) = List.destutter' R b l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<GOAL>List.destutter' R a [b] = if R a b then [a, b] else [a]
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>(List.destutter' R a l).Sublist (a :: l)
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>a ∈ List.destutter' R a l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<VAR>a b : α<GOAL>R a b → List.Chain R a (List.destutter' R b l)
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.Chain' R (List.destutter' R a l)
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<VAR>h : List.Chain R a l<GOAL>List.destutter' R a l = a :: l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.destutter' R a l = a :: l ↔ List.Chain R a l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.destutter' R a l ≠ []
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<GOAL>List.destutter R [] = []
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.destutter R (a :: l) = List.destutter' R a l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<GOAL>List.destutter R (a :: b :: l) = if R a b then a :: List.destutter' R b l else List.destutter' R a l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a : α<GOAL>List.destutter R [a] = [a]
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>a b : α<GOAL>List.destutter R [a, b] = if R a b then [a, b] else [a]
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>(List.destutter R l).Sublist l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.Chain' R (List.destutter R l)
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.Chain' R l → List.destutter R l = l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.destutter R l = l ↔ List.Chain' R l
<VAR>α : Type u_1<VAR>l : List α<VAR>R : α → α → Prop<VAR>DecidableRel R<GOAL>List.destutter R (List.destutter R l) = List.destutter R l
<VAR>α : Type u_1<VAR>R : α → α → Prop<VAR>DecidableRel R<VAR>l : List α<GOAL>List.destutter R l = [] ↔ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List β<GOAL>[] ×ˢ l = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a : α<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(a :: l₁) ×ˢ l₂ = List.map (fun b => (a, b)) l₂ ++ l₁ ×ˢ l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>l ×ˢ [] = []
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ : List α<VAR>l₂ : List β<GOAL>(l₁ ×ˢ l₂).length = l₁.length * l₂.length
<VAR>α : Type u_1<VAR>σ : α → Type u_3<VAR>l : (a : α) → List (σ a)<GOAL>[].sigma l = []
<VAR>α : Type u_1<VAR>σ : α → Type u_3<VAR>a : α<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>(a :: l₁).sigma l₂ = List.map (Sigma.mk a) (l₂ a) ++ l₁.sigma l₂
<VAR>α : Type u_1<VAR>σ : α → Type u_3<VAR>l : List α<GOAL>(l.sigma fun a => []) = []
<VAR>α : Type u_1<VAR>σ : α → Type u_3<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<VAR>a : α<VAR>b : σ a<GOAL>⟨a, b⟩ ∈ l₁.sigma l₂ ↔ a ∈ l₁ ∧ b ∈ l₂ a
<VAR>α : Type u_1<VAR>σ : α → Type u_3<VAR>l₁ : List α<VAR>l₂ : (a : α) → List (σ a)<GOAL>(l₁.sigma l₂).length = Nat.sum (List.map (fun a => (l₂ a).length) l₁)
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>(List.filter p l).length < l.length ↔ ∃ x, x ∈ l ∧ ¬p x = true
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<GOAL>List.countP (fun a => p ↑a) l.attach = List.countP p l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>DecidableEq α<VAR>DecidableEq β<VAR>l : List α<VAR>f : α → β<VAR>hf : Function.Injective f<VAR>x : α<GOAL>List.count (f x) (List.map f l) = List.count x l
<VAR>α : Type u_1<VAR>l : List α<VAR>DecidableEq α<VAR>a : { x // x ∈ l }<GOAL>List.count a l.attach = List.count (↑a) l
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<GOAL>⇑l.toFinsupp = fun x => l.getD x 0
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<VAR>i : ℕ<GOAL>l.toFinsupp i = l.getD i 0
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<GOAL>l.toFinsupp.support = Finset.filter (fun x => l.getD x 0 ≠ 0) (Finset.range l.length)
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.toFinsupp n = l.get ⟨n, hn⟩
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : Fin l.length<GOAL>l.toFinsupp ↑n = l.get n
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : ℕ<VAR>hn : n < l.length<GOAL>l.toFinsupp n = l.nthLe n hn
<VAR>M : Type u_1<VAR>Zero M<VAR>l : List M<VAR>DecidablePred fun x => l.getD x 0 ≠ 0<VAR>n : ℕ<VAR>hn : l.length ≤ n<GOAL>l.toFinsupp n = 0
<VAR>M : Type u_1<VAR>Zero M<VAR>DecidablePred fun i => [].getD i 0 ≠ 0<GOAL>[].toFinsupp = 0
<VAR>M : Type u_1<VAR>Zero M<VAR>x : M<VAR>DecidablePred fun x_1 => [x].getD x_1 0 ≠ 0<GOAL>[x].toFinsupp = Finsupp.single 0 x
<VAR>M : Type u_1<VAR>Zero M<VAR>x : M<VAR>xs : List M<VAR>DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0<GOAL>(x :: xs).toFinsupp 0 = x
<VAR>M : Type u_1<VAR>Zero M<VAR>x : M<VAR>xs : List M<VAR>n : ℕ<VAR>DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0<VAR>DecidablePred fun x => xs.getD x 0 ≠ 0<GOAL>(x :: xs).toFinsupp n.succ = xs.toFinsupp n