ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>Infinite α<VAR>s : Finset α<GOAL>∃ x, x ∉ s
<VAR>α : Type u_4<VAR>Infinite α<GOAL>Nonempty α
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Infinite β<VAR>f : β → α<VAR>hf : Function.Injective f<GOAL>Infinite α
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Infinite β<VAR>f : α → β<VAR>hf : Function.Surjective f<GOAL>Infinite α
<VAR>α : Type u_4<VAR>Infinite α<GOAL>Function.Injective (Infinite.natEmbeddingAux α)
<VAR>α : Type u_4<VAR>Infinite α<VAR>n : ℕ<GOAL>∃ s, s.card = n
<VAR>α : Type u_1<VAR>Infinite α<VAR>s : Finset α<VAR>n : ℕ<VAR>hn : s.card ≤ n<GOAL>∃ t, s ⊆ t ∧ t.card = n
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Infinite α<VAR>Finite β<VAR>f : α → β<GOAL>¬Function.Injective f
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Infinite α<VAR>Finite β<VAR>f : α → β<GOAL>∃ x y, x ≠ y ∧ f x = f y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Infinite α<VAR>Finite β<VAR>f : α → β<GOAL>∃ y, Infinite ↑(f ⁻¹' {y})
<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>Finite α<VAR>Infinite β<VAR>f : α → β<GOAL>¬Function.Surjective f
<VAR>α : Type u_4<VAR>Fintype α<VAR>c : List ℕ<VAR>hc : c.sum ≤ Fintype.card α<GOAL>∃ o, List.map List.length o = c ∧ (∀ s ∈ o, s.Nodup) ∧ List.Pairwise List.Disjoint o
<VAR>P : (α : Type u_4) → [inst : Fintype α] → Prop<VAR>α : Type u_4<VAR>Fintype α<VAR>hbase : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Subsingleton α], P α<VAR>hstep : ∀ (α : Type u_4) [inst : Fintype α] [inst_1 : Nontrivial α], (∀ (β : Type u_4) [inst_2 : Fintype β], Fintype.card β < Fintype.card α → P β) → P α<GOAL>P α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : ℕ<VAR>f : Fin m → α → β<VAR>v : Fin m → α<GOAL>FinVec.seq f v = fun i => f i (v i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>m : ℕ<VAR>v : Fin m → α<GOAL>FinVec.map f v = f ∘ v
<VAR>α : Type u_1<VAR>m : ℕ<VAR>v : Fin m → α<GOAL>FinVec.etaExpand v = v
<VAR>α : Type u_1<VAR>m : ℕ<VAR>P : (Fin m → α) → Prop<GOAL>FinVec.Forall P ↔ ∀ (x : Fin m → α), P x
<VAR>α : Type u_1<VAR>m : ℕ<VAR>P : (Fin m → α) → Prop<GOAL>FinVec.Exists P ↔ ∃ x, P x
<VAR>α : Type u_1<VAR>AddCommMonoid α<VAR>m : ℕ<VAR>a : Fin m → α<GOAL>FinVec.sum a = ∑ i : Fin m, a i
<VAR>n : ℕ<VAR>α : Type u<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>f : Function.FromTypes (Matrix.vecCons α p) τ<VAR>a : α<VAR>args : (i : Fin n) → p i<GOAL>f.uncurry (Fin.cons a args) = (f a).uncurry args
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>f : Function.FromTypes p τ<VAR>args : (i : Fin (n + 1)) → p i<GOAL>f.uncurry args = (f (args 0)).uncurry (Fin.tail args)
<VAR>n : ℕ<VAR>α : Type u<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>f : ((i : Fin (n + 1)) → Matrix.vecCons α p i) → τ<VAR>a : α<GOAL>Function.FromTypes.curry f a = Function.FromTypes.curry ((fun {x} => f) ∘' Fin.cons a)
<VAR>n : ℕ<VAR>p : Fin (n + 1) → Type u<VAR>τ : Type u<VAR>f : ((i : Fin (n + 1)) → p i) → τ<VAR>a : p 0<GOAL>Function.FromTypes.curry f a = Function.FromTypes.curry (f ∘ Fin.cons a)
<VAR>n : ℕ<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>f : Function.FromTypes p τ<GOAL>Function.FromTypes.curry f.uncurry = f
<VAR>n : ℕ<VAR>p : Fin n → Type u<VAR>τ : Type u<VAR>f : ((i : Fin n) → p i) → τ<GOAL>(Function.FromTypes.curry f).uncurry = f
<VAR>n : ℕ<VAR>τ : Type u<VAR>p : Fin n → Type u<VAR>f : Function.FromTypes p τ<GOAL>∀ (a : (i : Fin n) → p i), (Function.FromTypes.curryEquiv p).symm f a = f.uncurry a
<VAR>n : ℕ<VAR>τ : Type u<VAR>p : Fin n → Type u<GOAL>∀ (a : ((i : Fin n) → p i) → τ), (Function.FromTypes.curryEquiv p) a = Function.FromTypes.curry a
<VAR>p : Fin 2 → Type u<VAR>τ : Type u<VAR>f : ((i : Fin 2) → p i) → τ<GOAL>Function.FromTypes.curry f = Function.curry (f ∘ ⇑(piFinTwoEquiv p).symm)
<VAR>p : Fin 2 → Type u<VAR>τ : Type u<VAR>f : Function.FromTypes p τ<GOAL>f.uncurry = Function.uncurry f ∘ ⇑(piFinTwoEquiv p)
<VAR>α β : Type u<VAR>n : ℕ<VAR>f : Function.OfArity α β n<GOAL>Function.OfArity.curry f.uncurry = f
<VAR>α β : Type u<VAR>n : ℕ<VAR>f : (Fin n → α) → β<GOAL>(Function.OfArity.curry f).uncurry = f
<VAR>α β : Type u<VAR>n : ℕ<VAR>f : Function.FromTypes (fun a => α) β<GOAL>∀ (a : Fin n → α), (Function.OfArity.curryEquiv n).symm f a = f.uncurry a
<VAR>α β : Type u<VAR>n : ℕ<GOAL>∀ (a : (Fin n → α) → β), (Function.OfArity.curryEquiv n) a = Function.FromTypes.curry a
<VAR>α β : Type u<VAR>f : (Fin 2 → α) → β<GOAL>Function.OfArity.curry f = Function.curry (f ∘ ⇑(finTwoArrowEquiv α).symm)
<VAR>α β : Type u<VAR>f : Function.OfArity α β 2<GOAL>f.uncurry = Function.uncurry f ∘ ⇑(finTwoArrowEquiv α)
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>h : Set.InjOn f s<VAR>Finite ↑(f '' s)<GOAL>Finite ↑s
<VAR>α : Type u<VAR>ι : Sort w<VAR>f : ι → α<VAR>hf : Function.Injective f<VAR>Finite ↑(Set.range f)<GOAL>Finite ι
<VAR>α : Sort u_3<GOAL>Finite α ↔ ∃ n, Nonempty (α ≃ Fin n)
<VAR>α : Sort u_3<VAR>h : Finite α<GOAL>∃ n, Nonempty (α ≃ Fin n)
<VAR>β : Sort u_2<VAR>α : Sort u_3<VAR>h : Finite α<VAR>f : α ≃ β<GOAL>Finite β
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α ≃ β<GOAL>Finite α ↔ Finite β
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>f : α → β<VAR>h : Function.Bijective f<GOAL>Finite α ↔ Finite β
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>Finite α<VAR>f : α → β<VAR>h : Function.Bijective f<GOAL>Finite β
<VAR>α : Sort u_3<VAR>self : Infinite α<GOAL>¬Finite α
<VAR>α : Sort u_1<GOAL>¬Finite α ↔ Infinite α
<VAR>α : Sort u_1<GOAL>¬Infinite α ↔ Finite α
<VAR>α : Sort u_1<VAR>β : Sort u_2<VAR>e : α ≃ β<GOAL>Infinite α ↔ Infinite β
<VAR>α : Sort u_3<GOAL>Finite α ∨ Infinite α
<VAR>α : Sort u_3<VAR>Infinite α<VAR>Finite α<GOAL>False
<VAR>α : Sort u_1<VAR>Infinite α<GOAL>Finite α → False
<VAR>α : Sort u_1<VAR>Finite α<GOAL>Infinite α → False
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Finite (α × β)<VAR>Nonempty β<GOAL>Finite α
<VAR>β : Type u_2<VAR>α : Type u_4<VAR>Finite (α × β)<VAR>Nonempty α<GOAL>Finite β
<VAR>α : Type u_1<VAR>β : Type u_4<VAR>Finite (α ⊕ β)<GOAL>Finite α
<VAR>β : Type u_2<VAR>α : Type u_4<VAR>Finite (α ⊕ β)<GOAL>Finite β
<VAR>α : Type u_2<VAR>One α<GOAL>↑1 = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>↑0 = 0
<VAR>α : Type u_2<VAR>One α<VAR>s : Finset α<GOAL>↑s = 1 ↔ s = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset α<GOAL>↑s = 0 ↔ s = 0
<VAR>α : Type u_2<VAR>One α<VAR>s : Finset α<GOAL>1 ⊆ s ↔ 1 ∈ s
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset α<GOAL>0 ⊆ s ↔ 0 ∈ s
<VAR>α : Type u_2<VAR>One α<GOAL>Finset.Nonempty 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>Finset.Nonempty 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>f : α ↪ β<GOAL>Finset.map f 0 = {f 0}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>f : α ↪ β<GOAL>Finset.map f 1 = {f 1}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>DecidableEq β<VAR>f : α → β<GOAL>Finset.image f 0 = {f 0}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>DecidableEq β<VAR>f : α → β<GOAL>Finset.image f 1 = {f 1}
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset α<GOAL>s ⊆ 0 ↔ s = ∅ ∨ s = 0
<VAR>α : Type u_2<VAR>One α<VAR>s : Finset α<GOAL>s ⊆ 1 ↔ s = ∅ ∨ s = 1
<VAR>α : Type u_2<VAR>One α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s ⊆ 1 ↔ s = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>s ⊆ 0 ↔ s = 0
<VAR>α : Type u_2<VAR>One α<GOAL>Finset.card 1 = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>Finset.card 0 = 1
<VAR>α : Type u_2<VAR>Zero α<GOAL>⇑Finset.singletonZeroHom = singleton
<VAR>α : Type u_2<VAR>One α<GOAL>⇑Finset.singletonOneHom = singleton
<VAR>α : Type u_2<VAR>One α<VAR>a : α<GOAL>Finset.singletonOneHom a = {a}
<VAR>α : Type u_2<VAR>Zero α<VAR>a : α<GOAL>Finset.singletonZeroHom a = {a}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>DecidableEq β<VAR>Zero β<VAR>FunLike F α β<VAR>ZeroHomClass F α β<VAR>f : F<VAR>s : Finset α<GOAL>(Finset.imageZeroHom f) s = Finset.image (⇑f) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>DecidableEq β<VAR>One β<VAR>FunLike F α β<VAR>OneHomClass F α β<VAR>f : F<VAR>s : Finset α<GOAL>(Finset.imageOneHom f) s = Finset.image (⇑f) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f : α → β<GOAL>Finset.sup 1 f = f 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>f : α → β<GOAL>Finset.sup 0 f = f 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>SemilatticeSup β<VAR>f : α → β<GOAL>Finset.sup' 1 ⋯ f = f 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>SemilatticeSup β<VAR>f : α → β<GOAL>Finset.sup' 0 ⋯ f = f 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f : α → β<GOAL>Finset.inf 0 f = f 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>f : α → β<GOAL>Finset.inf 1 f = f 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>One α<VAR>SemilatticeInf β<VAR>f : α → β<GOAL>Finset.inf' 1 ⋯ f = f 1
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>SemilatticeInf β<VAR>f : α → β<GOAL>Finset.inf' 0 ⋯ f = f 0
<VAR>α : Type u_2<VAR>Zero α<VAR>LinearOrder α<GOAL>Finset.max 0 = 0
<VAR>α : Type u_2<VAR>One α<VAR>LinearOrder α<GOAL>Finset.max 1 = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>LinearOrder α<GOAL>Finset.min 0 = 0
<VAR>α : Type u_2<VAR>One α<VAR>LinearOrder α<GOAL>Finset.min 1 = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>LinearOrder α<GOAL>Finset.max' 0 ⋯ = 0
<VAR>α : Type u_2<VAR>One α<VAR>LinearOrder α<GOAL>Finset.max' 1 ⋯ = 1
<VAR>α : Type u_2<VAR>One α<VAR>LinearOrder α<GOAL>Finset.min' 1 ⋯ = 1
<VAR>α : Type u_2<VAR>Zero α<VAR>LinearOrder α<GOAL>Finset.min' 0 ⋯ = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>s⁻¹ = Finset.image (fun x => x⁻¹) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>-s = Finset.image (fun x => -x) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>Finset.image (fun x => -x) s = -s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>Finset.image (fun x => x⁻¹) s = s⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ -s ↔ ∃ y ∈ s, -y = x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<VAR>x : α<GOAL>x ∈ s⁻¹ ↔ ∃ y ∈ s, y⁻¹ = x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>-a ∈ -s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<GOAL>a⁻¹ ∈ s⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>s⁻¹.card ≤ s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>(-s).card ≤ s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<GOAL>∅⁻¹ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<GOAL>-∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>(-s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>s⁻¹.Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>-s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>s⁻¹ = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>s⁻¹ ⊆ t⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s t : Finset α<VAR>h : s ⊆ t<GOAL>-s ⊆ -t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>a : α<GOAL>{a}⁻¹ = {a⁻¹}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>a : α<GOAL>-{a} = {-a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>a : α<VAR>s : Finset α<GOAL>-insert a s = insert (-a) (-s)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>a : α<VAR>s : Finset α<GOAL>(insert a s)⁻¹ = insert a⁻¹ s⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Inv α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s : Finset α<VAR>f : α → β<GOAL>s⁻¹.sup f = s.sup fun x => f x⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Neg α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s : Finset α<VAR>f : α → β<GOAL>(-s).sup f = s.sup fun x => f (-x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Inv α<VAR>SemilatticeSup β<VAR>s : Finset α<VAR>hs : s⁻¹.Nonempty<VAR>f : α → β<GOAL>s⁻¹.sup' hs f = s.sup' ⋯ fun x => f x⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Neg α<VAR>SemilatticeSup β<VAR>s : Finset α<VAR>hs : (-s).Nonempty<VAR>f : α → β<GOAL>(-s).sup' hs f = s.sup' ⋯ fun x => f (-x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Inv α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s : Finset α<VAR>f : α → β<GOAL>s⁻¹.inf f = s.inf fun x => f x⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Neg α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s : Finset α<VAR>f : α → β<GOAL>(-s).inf f = s.inf fun x => f (-x)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Inv α<VAR>SemilatticeInf β<VAR>s : Finset α<VAR>hs : s⁻¹.Nonempty<VAR>f : α → β<GOAL>s⁻¹.inf' hs f = s.inf' ⋯ fun x => f x⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Neg α<VAR>SemilatticeInf β<VAR>s : Finset α<VAR>hs : (-s).Nonempty<VAR>f : α → β<GOAL>(-s).inf' hs f = s.inf' ⋯ fun x => f (-x)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Inv α<VAR>s : Finset α<GOAL>Finset.image MulOpposite.op s⁻¹ = (Finset.image MulOpposite.op s)⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Neg α<VAR>s : Finset α<GOAL>Finset.image AddOpposite.op (-s) = -Finset.image AddOpposite.op s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ s⁻¹ ↔ a⁻¹ ∈ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>s : Finset α<VAR>a : α<GOAL>a ∈ -s ↔ -a ∈ s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>s : Finset α<GOAL>↑(-s) = -↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>s : Finset α<GOAL>↑s⁻¹ = (↑s)⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>s : Finset α<GOAL>(-s).card = s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>s : Finset α<GOAL>s⁻¹.card = s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>s : Finset α<GOAL>s.preimage (fun x => x⁻¹) ⋯ = s⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>s : Finset α<GOAL>s.preimage (fun x => -x) ⋯ = -s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>Fintype α<GOAL>Finset.univ⁻¹ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>Fintype α<GOAL>-Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveNeg α<VAR>s t : Finset α<GOAL>-(s ∩ t) = -s ∩ -t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>InvolutiveInv α<VAR>s t : Finset α<GOAL>(s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s + t = Finset.image (fun p => p.1 + p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s * t = Finset.image (fun p => p.1 * p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>Finset.image (fun x => x.1 + x.2) (s ×ˢ t) = s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>Finset.image (fun x => x.1 * x.2) (s ×ˢ t) = s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<VAR>x : α<GOAL>x ∈ s * t ↔ ∃ y ∈ s, ∃ z ∈ t, y * z = x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<VAR>x : α<GOAL>x ∈ s + t ↔ ∃ y ∈ s, ∃ z ∈ t, y + z = x
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>↑(s + t) = ↑s + ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>↑(s * t) = ↑s * ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a * b ∈ s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a + b ∈ s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>(s * t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>(s + t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>(s + t).card = s.card * t.card ↔ Set.InjOn (fun p => p.1 + p.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>(s * t).card = s.card * t.card ↔ Set.InjOn (fun p => p.1 * p.2) (↑s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s : Finset α<GOAL>∅ + s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s : Finset α<GOAL>∅ * s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s : Finset α<GOAL>s + ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s : Finset α<GOAL>s * ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s * t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s + t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>(s + t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>(s * t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s * t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s + t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>(s * t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>(s + t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t : Finset α<GOAL>(s * t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t : Finset α<GOAL>(s + t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s : Finset α<VAR>a : α<GOAL>s + {a} = Finset.image (fun x => x + a) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s : Finset α<VAR>a : α<GOAL>s * {a} = Finset.image (fun x => x * a) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s : Finset α<VAR>a : α<GOAL>{a} + s = Finset.image (fun x => a + x) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s : Finset α<VAR>a : α<GOAL>{a} * s = Finset.image (fun x => a * x) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>a b : α<GOAL>{a} * {b} = {a * b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>a b : α<GOAL>{a} + {b} = {a + b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ * t₁ ⊆ s₂ * t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ + t₁ ⊆ s₂ + t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s * t₁ ⊆ s * t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s + t₁ ⊆ s + t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ * t ⊆ s₂ * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ + t ⊆ s₂ + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t u : Finset α<GOAL>s * t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x * y ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t u : Finset α<GOAL>s + t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x + y ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂) * t = s₁ * t ∪ s₂ * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∪ s₂ + t = s₁ + t ∪ (s₂ + t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t₁ t₂ : Finset α<GOAL>s + (t₁ ∪ t₂) = s + t₁ ∪ (s + t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t₁ t₂ : Finset α<GOAL>s * (t₁ ∪ t₂) = s * t₁ ∪ s * t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∩ s₂ + t ⊆ (s₁ + t) ∩ (s₂ + t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∩ s₂ * t ⊆ s₁ * t ∩ (s₂ * t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s t₁ t₂ : Finset α<GOAL>s + t₁ ∩ t₂ ⊆ (s + t₁) ∩ (s + t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s t₁ t₂ : Finset α<GOAL>s * (t₁ ∩ t₂) ⊆ s * t₁ ∩ (s * t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∩ s₂ * (t₁ ∪ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∩ s₂ + (t₁ ∪ t₂) ⊆ s₁ + t₁ ∪ (s₂ + t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∪ s₂ + t₁ ∩ t₂ ⊆ s₁ + t₁ ∪ (s₂ + t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>(s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>u : Finset α<VAR>s t : Set α<GOAL>↑u ⊆ s + t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' + t'
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>u : Finset α<VAR>s t : Set α<GOAL>↑u ⊆ s * t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' * t'
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>f : F<VAR>s t : Finset α<GOAL>Finset.image (⇑f) (s * t) = Finset.image (⇑f) s * Finset.image (⇑f) t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>f : F<VAR>s t : Finset α<GOAL>Finset.image (⇑f) (s + t) = Finset.image (⇑f) s + Finset.image (⇑f) t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<GOAL>⇑Finset.singletonMulHom = singleton
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<GOAL>⇑Finset.singletonAddHom = singleton
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Mul α<VAR>a : α<GOAL>Finset.singletonMulHom a = {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Add α<VAR>a : α<GOAL>Finset.singletonAddHom a = {a}
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Mul α<VAR>Mul β<VAR>FunLike F α β<VAR>MulHomClass F α β<VAR>f : F<VAR>s : Finset α<GOAL>(Finset.imageMulHom f) s = Finset.image (⇑f) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Add α<VAR>Add β<VAR>FunLike F α β<VAR>AddHomClass F α β<VAR>f : F<VAR>s : Finset α<GOAL>(Finset.imageAddHom f) s = Finset.image (⇑f) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<VAR>a : β<GOAL>(s * t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x * y) ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<VAR>a : β<GOAL>(s + t).sup f ≤ a ↔ ∀ x ∈ s, ∀ y ∈ t, f (x + y) ≤ a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s + t).sup f = s.sup fun x => t.sup fun x_1 => f (x + x_1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s * t).sup f = s.sup fun x => t.sup fun x_1 => f (x * x_1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s * t).sup f = t.sup fun y => s.sup fun x => f (x * y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeSup β<VAR>OrderBot β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s + t).sup f = t.sup fun y => s.sup fun x => f (x + y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<VAR>a : β<GOAL>a ≤ (s + t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x + y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<VAR>a : β<GOAL>a ≤ (s * t).inf f ↔ ∀ x ∈ s, ∀ y ∈ t, a ≤ f (x * y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s + t).inf f = s.inf fun x => t.inf fun x_1 => f (x + x_1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s * t).inf f = s.inf fun x => t.inf fun x_1 => f (x * x_1)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Add α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s + t).inf f = t.inf fun y => s.inf fun x => f (x + y)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>Mul α<VAR>SemilatticeInf β<VAR>OrderTop β<VAR>s t : Finset α<VAR>f : α → β<GOAL>(s * t).inf f = t.inf fun y => s.inf fun x => f (x * y)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>s / t = Finset.image (fun p => p.1 / p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>s - t = Finset.image (fun p => p.1 - p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>Finset.image (fun x => x.1 - x.2) (s ×ˢ t) = s - t