ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>List.kinsert a b l = ⟨a, b⟩ :: List.kerase a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b' : β a'<VAR>l : List (Sigma β)<GOAL>a ∈ (List.kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<VAR>nd : l.NodupKeys<GOAL>(List.kinsert a b l).NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<VAR>nd₁ : l₁.NodupKeys<VAR>p : l₁.Perm l₂<GOAL>(List.kinsert a b l₁).Perm (List.kinsert a b l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l : List (Sigma β)<GOAL>List.dlookup a (List.kinsert a b l) = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a a' : α<VAR>b' : β a'<VAR>l : List (Sigma β)<VAR>h : a ≠ a'<GOAL>List.dlookup a (List.kinsert a' b' l) = List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>List.kextract a l = (List.dlookup a l, List.kerase a l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>x : Sigma β<VAR>l : List (Sigma β)<GOAL>(x :: l).dedupKeys = List.kinsert x.fst x.snd l.dedupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<GOAL>l.dedupKeys.NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l : List (Sigma β)<GOAL>List.dlookup a l.dedupKeys = List.dlookup a l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>SizeOf (Sigma β)<VAR>xs : List (Sigma β)<GOAL>sizeOf xs.dedupKeys ≤ sizeOf xs
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<GOAL>[].kunion l = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<GOAL>l.kunion [] = l
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>s : Sigma β<VAR>l₁ l₂ : List (Sigma β)<GOAL>(s :: l₁).kunion l₂ = s :: l₁.kunion (List.kerase s.fst l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<GOAL>a ∈ (l₁.kunion l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<GOAL>(List.kerase a l₁).kunion (List.kerase a l₂) = List.kerase a (l₁.kunion l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>l₁ l₂ : List (Sigma β)<VAR>DecidableEq α<VAR>nd₁ : l₁.NodupKeys<VAR>nd₂ : l₂.NodupKeys<GOAL>(l₁.kunion l₂).NodupKeys
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l₁ l₂ : List (Sigma β)<VAR>p : l₁.Perm l₂<VAR>l : List (Sigma β)<GOAL>(l₁.kunion l).Perm (l₂.kunion l)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l : List (Sigma β)<VAR>l₁ l₂ : List (Sigma β)<GOAL>l₁.NodupKeys → l₁.Perm l₂ → (l.kunion l₁).Perm (l.kunion l₂)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>l₁ l₂ l₃ l₄ : List (Sigma β)<VAR>nd₃ : l₃.NodupKeys<VAR>p₁₂ : l₁.Perm l₂<VAR>p₃₄ : l₃.Perm l₄<GOAL>(l₁.kunion l₃).Perm (l₂.kunion l₄)
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>h : a ∈ l₁.keys<GOAL>List.dlookup a (l₁.kunion l₂) = List.dlookup a l₁
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>l₁ l₂ : List (Sigma β)<VAR>h : a ∉ l₁.keys<GOAL>List.dlookup a (l₁.kunion l₂) = List.dlookup a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<GOAL>b ∈ List.dlookup a (l₁.kunion l₂) ↔ b ∈ List.dlookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ List.dlookup a l₂
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ : List (Sigma β)<GOAL>List.dlookup a (l₁.kunion l₂) = some b ↔ List.dlookup a l₁ = some b ∨ a ∉ l₁.keys ∧ List.dlookup a l₂ = some b
<VAR>α : Type u<VAR>β : α → Type v<VAR>DecidableEq α<VAR>a : α<VAR>b : β a<VAR>l₁ l₂ l₃ : List (Sigma β)<VAR>h₁ : b ∈ List.dlookup a (l₁.kunion l₃)<VAR>h₂ : a ∉ l₂.keys<GOAL>b ∈ List.dlookup a ((l₁.kunion l₂).kunion l₃)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>AddMonoid α<VAR>AddMonoid β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>l : List (Set α)<GOAL>⇑f '' l.sum = (List.map (fun s => ⇑f '' s) l).sum
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>Monoid α<VAR>Monoid β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>l : List (Set α)<GOAL>⇑f '' l.prod = (List.map (fun s => ⇑f '' s) l).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>CommMonoid α<VAR>CommMonoid β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>m : Multiset (Set α)<GOAL>⇑f '' m.prod = (Multiset.map (fun s => ⇑f '' s) m).prod
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>m : Multiset (Set α)<GOAL>⇑f '' m.sum = (Multiset.map (fun s => ⇑f '' s) m).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>CommMonoid α<VAR>CommMonoid β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>m : Finset ι<VAR>s : ι → Set α<GOAL>⇑f '' ∏ i ∈ m, s i = ∏ i ∈ m, ⇑f '' s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>F : Type u_4<VAR>FunLike F α β<VAR>AddCommMonoid α<VAR>AddCommMonoid β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>m : Finset ι<VAR>s : ι → Set α<GOAL>⇑f '' ∑ i ∈ m, s i = ∑ i ∈ m, ⇑f '' s i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : Finset ι<VAR>f : ι → Set α<VAR>a : α<GOAL>a ∈ ∏ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∏ i ∈ t, g i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : Finset ι<VAR>f : ι → Set α<VAR>a : α<GOAL>a ∈ ∑ i ∈ t, f i ↔ ∃ g, ∃ (_ : ∀ {i : ι}, i ∈ t → g i ∈ f i), ∑ i ∈ t, g i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>Fintype ι<VAR>f : ι → Set α<VAR>a : α<GOAL>a ∈ ∑ i : ι, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∑ i : ι, g i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>Fintype ι<VAR>f : ι → Set α<VAR>a : α<GOAL>a ∈ ∏ i : ι, f i ↔ ∃ g, ∃ (_ : ∀ (i : ι), g i ∈ f i), ∏ i : ι, g i = a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : List ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>(List.map g t).sum ∈ (List.map f t).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : List ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>(List.map g t).prod ∈ (List.map f t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : List ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>(List.map f₁ t).sum ⊆ (List.map f₂ t).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : List ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>(List.map f₁ t).prod ⊆ (List.map f₂ t).prod
<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : List M<GOAL>(List.map (fun i => {i}) s).sum = {s.sum}
<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : List M<GOAL>(List.map (fun i => {i}) s).prod = {s.prod}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : Multiset ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>(Multiset.map g t).sum ∈ (Multiset.map f t).sum
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : Multiset ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>(Multiset.map g t).prod ∈ (Multiset.map f t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : Multiset ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>(Multiset.map f₁ t).prod ⊆ (Multiset.map f₂ t).prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : Multiset ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>(Multiset.map f₁ t).sum ⊆ (Multiset.map f₂ t).sum
<VAR>M : Type u_5<VAR>AddCommMonoid M<VAR>s : Multiset M<GOAL>(Multiset.map (fun i => {i}) s).sum = {s.sum}
<VAR>M : Type u_5<VAR>CommMonoid M<VAR>s : Multiset M<GOAL>(Multiset.map (fun i => {i}) s).prod = {s.prod}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : Finset ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>∏ i ∈ t, g i ∈ ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : Finset ι<VAR>f : ι → Set α<VAR>g : ι → α<VAR>hg : ∀ i ∈ t, g i ∈ f i<GOAL>∑ i ∈ t, g i ∈ ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>t : Finset ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>∏ i ∈ t, f₁ i ⊆ ∏ i ∈ t, f₂ i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>t : Finset ι<VAR>f₁ f₂ : ι → Set α<VAR>hf : ∀ i ∈ t, f₁ i ⊆ f₂ i<GOAL>∑ i ∈ t, f₁ i ⊆ ∑ i ∈ t, f₂ i
<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>AddCommMonoid M<VAR>s : Finset ι<VAR>I : ι → M<GOAL>∑ i ∈ s, {I i} = {∑ i ∈ s, I i}
<VAR>M : Type u_5<VAR>ι : Type u_6<VAR>CommMonoid M<VAR>s : Finset ι<VAR>I : ι → M<GOAL>∏ i ∈ s, {I i} = {∏ i ∈ s, I i}
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>l : Finset ι<VAR>S : ι → Set α<GOAL>(fun f => ∏ i ∈ l, f i) '' (↑l).pi S = ∏ i ∈ l, S i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>l : Finset ι<VAR>S : ι → Set α<GOAL>(fun f => ∑ i ∈ l, f i) '' (↑l).pi S = ∑ i ∈ l, S i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>AddCommMonoid α<VAR>Fintype ι<VAR>S : ι → Set α<GOAL>(fun f => ∑ i : ι, f i) '' Set.univ.pi S = ∑ i : ι, S i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>CommMonoid α<VAR>Fintype ι<VAR>S : ι → Set α<GOAL>(fun f => ∏ i : ι, f i) '' Set.univ.pi S = ∏ i : ι, S i
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.Perm l
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<VAR>h : l₁.Perm l₂<GOAL>l₁ ⊆ l₃ ↔ l₂ ⊆ l₃
<VAR>α : Type u_1<VAR>l₁ l₂ l₃ : List α<VAR>h : l₁.Perm l₂<GOAL>l₃ ⊆ l₁ ↔ l₃ ⊆ l₂
<VAR>α : Type u_1<GOAL>Relation.Comp List.Perm List.Perm = List.Perm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>l u : List α<VAR>v : List β<VAR>hlu : l.Perm u<VAR>huv : List.Forall₂ r u v<GOAL>Relation.Comp (List.Forall₂ r) List.Perm l v
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<GOAL>Relation.Comp (List.Forall₂ r) List.Perm = Relation.Comp List.Perm (List.Forall₂ r)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>hr : Relator.RightUnique r<GOAL>(List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun x x_1 => x → x_1) List.Perm List.Perm
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r : α → β → Prop<VAR>hr : Relator.BiUnique r<GOAL>(List.Forall₂ r ⇒ List.Forall₂ r ⇒ fun x x_1 => x ↔ x_1) List.Perm List.Perm
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<GOAL>l₁.Subperm l₂ ↔ ∃ l, l.Perm l₂ ∧ l₁.Sublist l
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>l.Subperm [a] ↔ l = [] ∨ l = [a]
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.Subperm [] ↔ l = []
<VAR>α : Type u_1<VAR>l : List α<VAR>a : α<GOAL>l.Subperm (a :: l)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>P : α → Prop<VAR>DecidablePred P<VAR>l : List α<VAR>a : α<GOAL>List.count a l = List.count a (List.filter (fun b => decide (P b)) l) + List.count a (List.filter (fun x => decide ¬P x) l)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : β → α → β<VAR>l₁ l₂ : List α<VAR>rcomm : RightCommutative f<VAR>p : l₁.Perm l₂<VAR>b : β<GOAL>List.foldl f b l₁ = List.foldl f b l₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β → β<VAR>l₁ l₂ : List α<VAR>lcomm : LeftCommutative f<VAR>p : l₁.Perm l₂<VAR>b : β<GOAL>List.foldr f b l₁ = List.foldr f b l₂
<VAR>α : Type u_1<VAR>op : α → α → α<VAR>IA : Std.Associative op<VAR>IC : Std.Commutative op<VAR>l₁ l₂ : List α<VAR>a : α<VAR>h : l₁.Perm l₂<GOAL>List.foldl op a l₁ = List.foldl op a l₂
<VAR>α : Type u_1<VAR>o₁ o₂ : Option α<GOAL>o₁.toList.Perm o₂.toList ↔ o₁ = o₂
<VAR>α : Type u_1<VAR>a : α<VAR>l₁ l₂ : List α<VAR>d₁ : l₁.Nodup<VAR>h₁ : a ∉ l₁<VAR>h₂ : a ∈ l₂<VAR>s : l₁.Subperm l₂<GOAL>(a :: l₁).Subperm l₂
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>d : l₁.Nodup<VAR>H : l₁ ⊆ l₂<GOAL>l₁.Subperm l₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>t : List α<VAR>h : l₁.Perm l₂<GOAL>(l₁.bagInter t).Perm (l₂.bagInter t)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>t₁ t₂ : List α<VAR>p : t₁.Perm t₂<GOAL>l.bagInter t₁ = l.bagInter t₂
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ t₁ t₂ : List α<VAR>hl : l₁.Perm l₂<VAR>ht : t₁.Perm t₂<GOAL>(l₁.bagInter t₁).Perm (l₂.bagInter t₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>a b : α<VAR>m n : ℕ<VAR>h : a ≠ b<GOAL>l.Perm (List.replicate m a ++ List.replicate n b) ↔ List.count a l = m ∧ List.count b l = n ∧ l ⊆ [a, b]
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l₁ l₂ : List α<VAR>p : l₁.Perm l₂<GOAL>l₁.dedup.Perm l₂.dedup
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l t₁ t₂ : List α<VAR>h : t₁.Disjoint t₂<GOAL>(l ∩ (t₁ ++ t₂)).Perm (l ∩ t₁ ++ l ∩ t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f g : α → List β<VAR>h : ∀ a ∈ l, (f a).Perm (g a)<GOAL>(l.bind f).Perm (l.bind g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f g : α → List β<GOAL>(l.bind f ++ l.bind g).Perm (l.bind fun x => f x ++ g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>f : α → β<VAR>g : α → List β<GOAL>(List.map f l ++ l.bind g).Perm (l.bind fun x => f x :: g x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>t₁ : List β<VAR>p : l₁.Perm l₂<GOAL>(l₁.product t₁).Perm (l₂.product t₁)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>t₁ t₂ : List β<VAR>p : t₁.Perm t₂<GOAL>(l.product t₁).Perm (l.product t₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l₁ l₂ : List α<VAR>t₁ t₂ : List β<VAR>p₁ : l₁.Perm l₂<VAR>p₂ : t₁.Perm t₂<GOAL>(l₁.product t₁).Perm (l₂.product t₂)
<VAR>α : Type u_1<VAR>f : α → Option α<VAR>l₁ l₂ : List α<VAR>H : List.Pairwise (fun a b => ∀ c ∈ f a, ∀ d ∈ f b, a = b ∧ c = d) l₁<VAR>p : l₁.Perm l₂<GOAL>(List.lookmap f l₁).Perm (List.lookmap f l₂)
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>n : ℕ<VAR>h : xs.Perm ys<VAR>h' : ys.Nodup<GOAL>(List.take n xs).Perm (ys.inter (List.take n xs))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>n : ℕ<VAR>h : xs.Perm ys<VAR>h' : ys.Nodup<GOAL>(List.drop n xs).Perm (ys.inter (List.drop n xs))
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>xs ys : List α<VAR>n m : ℕ<VAR>h : xs.Perm ys<VAR>h' : ys.Nodup<GOAL>(List.dropSlice n m xs).Perm (ys ∩ List.dropSlice n m xs)
<VAR>α : Type u_1<VAR>ts is l : List α<GOAL>l ∈ ts.permutationsAux is → l.Perm (ts ++ is)
<VAR>α : Type u_1<VAR>l₁ l₂ : List α<VAR>h : l₁ ∈ l₂.permutations<GOAL>l₁.Perm l₂
<VAR>α : Type u_1<VAR>ts is : List α<GOAL>(ts.permutationsAux is).length + is.length ! = (ts.length + is.length)!
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.permutations.length = l.length !
<VAR>α : Type u_1<VAR>is l : List α<VAR>H : l.Perm ([] ++ is) → (∃ ts', ∃ (_ : ts'.Perm []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []<GOAL>l.Perm is → l ∈ is.permutations
<VAR>α : Type u_1<VAR>ts is l : List α<GOAL>l.Perm (is ++ ts) → (∃ is', ∃ (_ : is'.Perm is), l = is' ++ ts) ∨ l ∈ ts.permutationsAux is
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s ∈ t.permutations ↔ s.Perm t
<VAR>α : Type u_1<VAR>DecidableEq α<GOAL>List.instBEq = instBEqOfDecidableEq
<VAR>α : Type u_1<VAR>a b : α<VAR>l : List α<GOAL>((List.permutations'Aux a l).bind (List.permutations'Aux b)).Perm ((List.permutations'Aux b l).bind (List.permutations'Aux a))
<VAR>α : Type u_1<VAR>s t : List α<VAR>p : s.Perm t<GOAL>s.permutations'.Perm t.permutations'
<VAR>α : Type u_1<VAR>ts : List α<GOAL>ts.permutations.Perm ts.permutations'
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s ∈ t.permutations' ↔ s.Perm t
<VAR>α : Type u_1<VAR>s t : List α<VAR>h : s.Perm t<GOAL>s.permutations.Perm t.permutations
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s.permutations.Perm t.permutations ↔ s.Perm t
<VAR>α : Type u_1<VAR>s t : List α<GOAL>s.permutations'.Perm t.permutations' ↔ s.Perm t
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (List.permutations'Aux x s).length<GOAL>(List.permutations'Aux x s)[n] = List.insertNth n x s
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (List.permutations'Aux x s).length<GOAL>(List.permutations'Aux x s).get ⟨n, hn⟩ = List.insertNth n x s
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<VAR>n : ℕ<VAR>hn : n < (List.permutations'Aux x s).length<GOAL>(List.permutations'Aux x s).nthLe n hn = List.insertNth n x s
<VAR>α : Type u_1<VAR>DecidableEq α<VAR>l : List α<VAR>x : α<GOAL>List.count (x :: l) (List.permutations'Aux x l) = (List.takeWhile (fun x_1 => decide (x = x_1)) l).length + 1
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<GOAL>(List.permutations'Aux x s).length = s.length + 1
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<VAR>hn : 0 < (List.permutations'Aux x s).length := ⋯<GOAL>(List.permutations'Aux x s).get ⟨0, hn⟩ = x :: s
<VAR>α : Type u_1<VAR>x : α<GOAL>Function.Injective (List.permutations'Aux x)
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<VAR>hx : x ∉ s<GOAL>(List.permutations'Aux x s).Nodup
<VAR>α : Type u_1<VAR>s : List α<VAR>x : α<GOAL>(List.permutations'Aux x s).Nodup ↔ x ∉ s
<VAR>α : Type u_1<VAR>s : List α<VAR>hs : s.Nodup<GOAL>s.permutations.Nodup
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : αᵒᵖ<GOAL>a ∈ s.op ↔ Opposite.unop a ∈ s
<VAR>α : Type u_1<VAR>s : Set α<VAR>a : α<GOAL>Opposite.op a ∈ s.op ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Set αᵒᵖ<VAR>a : α<GOAL>a ∈ s.unop ↔ Opposite.op a ∈ s
<VAR>α : Type u_1<VAR>s : Set αᵒᵖ<VAR>a : αᵒᵖ<GOAL>Opposite.unop a ∈ s.unop ↔ a ∈ s
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.op.unop = s
<VAR>α : Type u_1<VAR>s : Set αᵒᵖ<GOAL>s.unop.op = s
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : ↑s.op<GOAL>↑(s.opEquiv_self x) = Opposite.unop ↑x
<VAR>α : Type u_1<VAR>s : Set α<VAR>x : ↑s<GOAL>↑(s.opEquiv_self.symm x) = Opposite.op ↑x
<VAR>α : Type u_1<VAR>s : Set αᵒᵖ<GOAL>Set.opEquiv.symm s = s.unop
<VAR>α : Type u_1<VAR>s : Set α<GOAL>Set.opEquiv s = s.op
<VAR>α : Type u_1<VAR>x : α<GOAL>{x}.op = {Opposite.op x}
<VAR>α : Type u_1<VAR>x : αᵒᵖ<GOAL>{x}.unop = {Opposite.unop x}
<VAR>α : Type u_1<VAR>x : α<GOAL>{Opposite.op x}.unop = {x}
<VAR>α : Type u_1<VAR>x : αᵒᵖ<GOAL>{Opposite.unop x}.op = {x}
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations R ↑x<VAR>hf : AlgebraicGeometry.StructureSheaf.IsFraction f<GOAL>∃ r s, ∀ (x : ↥U), ∃ (hs : s ∉ (↑x).asIdeal), f x = IsLocalization.mk' (Localization.AtPrime (↑x).asIdeal) r ⟨s, hs⟩
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>f : (x : ↥U) → AlgebraicGeometry.StructureSheaf.Localizations R ↑x<GOAL>(AlgebraicGeometry.StructureSheaf.isLocallyFraction R).pred f = ∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i r s, ∀ (y : ↥V), s ∉ (↑y).asIdeal ∧ f ((fun x => ⟨↑x, ⋯⟩) y) * (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ↑((fun x => ⟨↑x, ⋯⟩) y))) s = (algebraMap R (AlgebraicGeometry.StructureSheaf.Localizations R ↑((fun x => ⟨↑x, ⋯⟩) y))) r
<VAR>R : Type u<VAR>CommRing R<VAR>U V : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ<VAR>i : U ⟶ V<GOAL>∀ (a : (AlgebraicGeometry.structureSheafInType R).val.obj U), ((AlgebraicGeometry.structurePresheafInCommRing R).map i) a = (AlgebraicGeometry.structureSheafInType R).val.map i a
<VAR>R : Type u<VAR>CommRing R<VAR>U : (TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))ᵒᵖ<GOAL>(AlgebraicGeometry.structurePresheafInCommRing R).obj U = CommRingCat.of ((AlgebraicGeometry.structureSheafInType R).val.obj U)
<VAR>R : Type u<VAR>CommRing R<VAR>U V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>i : V ⟶ U<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<VAR>x : ↥V<GOAL>↑(((AlgebraicGeometry.Spec.structureSheaf R).val.map i.op) s) x = ↑s ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl<VAR>x : ↥U<GOAL>↑(AlgebraicGeometry.StructureSheaf.const R f g U hu) x = IsLocalization.mk' (AlgebraicGeometry.StructureSheaf.Localizations R ↑x) f ⟨g, ⋯⟩
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl<VAR>x : ↥U<VAR>hx : g ∈ (↑x).asIdeal.primeCompl<GOAL>↑(AlgebraicGeometry.StructureSheaf.const R f g U hu) x = IsLocalization.mk' (AlgebraicGeometry.StructureSheaf.Localizations R ↑x) f ⟨g, hx⟩
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>s : ↑((AlgebraicGeometry.Spec.structureSheaf R).val.obj (Opposite.op U))<VAR>x : ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hx : x ∈ U<GOAL>∃ V, ∃ (_ : x ∈ V), ∃ i f g, ∃ (hg : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl), AlgebraicGeometry.StructureSheaf.const R f g V hg = ((AlgebraicGeometry.Spec.structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hv : ∀ x ∈ V, g ∈ x.asIdeal.primeCompl<VAR>i : Opposite.op U ⟶ Opposite.op V<GOAL>((AlgebraicGeometry.Spec.structureSheaf R).val.map i) (AlgebraicGeometry.StructureSheaf.const R f g U hu) = AlgebraicGeometry.StructureSheaf.const R f g V hv
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R<VAR>V : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hv : V ≤ PrimeSpectrum.basicOpen g<GOAL>((AlgebraicGeometry.Spec.structureSheaf R).val.map (CategoryTheory.homOfLE hv).op) (AlgebraicGeometry.StructureSheaf.const R f g (PrimeSpectrum.basicOpen g) ⋯) = AlgebraicGeometry.StructureSheaf.const R f g V hv
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R 0 f U hu = 0
<VAR>R : Type u<VAR>CommRing R<VAR>f : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R f f U hu = 1
<VAR>R : Type u<VAR>CommRing R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<GOAL>AlgebraicGeometry.StructureSheaf.const R 1 1 U ⋯ = 1
<VAR>R : Type u<VAR>CommRing R<VAR>f₁ f₂ g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R f₁ g₁ U hu₁ + AlgebraicGeometry.StructureSheaf.const R f₂ g₂ U hu₂ = AlgebraicGeometry.StructureSheaf.const R (f₁ * g₂ + f₂ * g₁) (g₁ * g₂) U ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f₁ f₂ g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R f₁ g₁ U hu₁ * AlgebraicGeometry.StructureSheaf.const R f₂ g₂ U hu₂ = AlgebraicGeometry.StructureSheaf.const R (f₁ * f₂) (g₁ * g₂) U ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f₁ f₂ g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<VAR>h : f₁ * g₂ = f₂ * g₁<GOAL>AlgebraicGeometry.StructureSheaf.const R f₁ g₁ U hu₁ = AlgebraicGeometry.StructureSheaf.const R f₂ g₂ U hu₂
<VAR>R : Type u<VAR>CommRing R<VAR>f₁ f₂ g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hf : f₁ = f₂<VAR>hg : g₁ = g₂<GOAL>AlgebraicGeometry.StructureSheaf.const R f₁ g₁ U hu = AlgebraicGeometry.StructureSheaf.const R f₂ g₂ U ⋯
<VAR>R : Type u<VAR>CommRing R<VAR>f g : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, f ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R f g U hu₁ * AlgebraicGeometry.StructureSheaf.const R g f U hu₂ = 1
<VAR>R : Type u<VAR>CommRing R<VAR>f g₁ g₂ : R<VAR>U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R)<VAR>hu₁ : ∀ x ∈ U, g₁ ∈ x.asIdeal.primeCompl<VAR>hu₂ : ∀ x ∈ U, g₂ ∈ x.asIdeal.primeCompl<GOAL>AlgebraicGeometry.StructureSheaf.const R f g₁ U hu₁ * AlgebraicGeometry.StructureSheaf.const R g₁ g₂ U hu₂ = AlgebraicGeometry.StructureSheaf.const R f g₂ U hu₂