ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>Finset.image (fun x => x.1 / x.2) (s ×ˢ t) = s / t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s / t ↔ ∃ b ∈ s, ∃ c ∈ t, b / c = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ s - t ↔ ∃ b ∈ s, ∃ c ∈ t, b - c = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>↑(s - t) = ↑s - ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>↑(s / t) = ↑s / ↑t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a - b ∈ s - t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<VAR>a b : α<GOAL>a ∈ s → b ∈ t → a / b ∈ s / t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>(s - t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>(s / t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s : Finset α<GOAL>∅ - s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s : Finset α<GOAL>∅ / s = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s : Finset α<GOAL>s / ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s : Finset α<GOAL>s - ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>s - t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>s / t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>(s / t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>(s - t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s / t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>s.Nonempty → t.Nonempty → (s - t).Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>(s / t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>(s - t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t : Finset α<GOAL>(s - t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t : Finset α<GOAL>(s / t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s : Finset α<VAR>a : α<GOAL>s / {a} = Finset.image (fun x => x / a) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s : Finset α<VAR>a : α<GOAL>s - {a} = Finset.image (fun x => x - a) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s : Finset α<VAR>a : α<GOAL>{a} / s = Finset.image (fun x => a / x) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s : Finset α<VAR>a : α<GOAL>{a} - s = Finset.image (fun x => a - x) s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>a b : α<GOAL>{a} - {b} = {a - b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>a b : α<GOAL>{a} / {b} = {a / b}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ / t₁ ⊆ s₂ / t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ - t₁ ⊆ s₂ - t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s / t₁ ⊆ s / t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t₁ t₂ : Finset α<GOAL>t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ / t ⊆ s₂ / t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ⊆ s₂ → s₁ - t ⊆ s₂ - t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t u : Finset α<GOAL>s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t u : Finset α<GOAL>s / t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x / y ∈ u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∪ s₂ - t = s₁ - t ∪ (s₂ - t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t : Finset α<GOAL>(s₁ ∪ s₂) / t = s₁ / t ∪ s₂ / t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t₁ t₂ : Finset α<GOAL>s - (t₁ ∪ t₂) = s - t₁ ∪ (s - t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t₁ t₂ : Finset α<GOAL>s / (t₁ ∪ t₂) = s / t₁ ∪ s / t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∩ s₂ - t ⊆ (s₁ - t) ∩ (s₂ - t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t : Finset α<GOAL>s₁ ∩ s₂ / t ⊆ s₁ / t ∩ (s₂ / t)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s t₁ t₂ : Finset α<GOAL>s - t₁ ∩ t₂ ⊆ (s - t₁) ∩ (s - t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s t₁ t₂ : Finset α<GOAL>s / (t₁ ∩ t₂) ⊆ s / t₁ ∩ (s / t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∩ s₂ / (t₁ ∪ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∩ s₂ - (t₁ ∪ t₂) ⊆ s₁ - t₁ ∪ (s₂ - t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Div α<VAR>s₁ s₂ t₁ t₂ : Finset α<GOAL>(s₁ ∪ s₂) / (t₁ ∩ t₂) ⊆ s₁ / t₁ ∪ s₂ / t₂
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Sub α<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>Div α<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>β : Type u_3<VAR>DecidableEq α<VAR>Sub α<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>Div α<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>Sub α<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>Div α<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>Div α<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>Sub α<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>Div α<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>Sub α<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>Div α<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>Sub α<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>Sub α<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>Div α<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>CommSemigroup α<VAR>s t : Finset α<GOAL>s ∩ t * (s ∪ t) ⊆ s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddCommSemigroup α<VAR>s t : Finset α<GOAL>s ∩ t + (s ∪ t) ⊆ s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddCommSemigroup α<VAR>s t : Finset α<GOAL>s ∪ t + s ∩ t ⊆ s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>CommSemigroup α<VAR>s t : Finset α<GOAL>(s ∪ t) * (s ∩ t) ⊆ s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : 1 ∈ t<GOAL>s ⊆ s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : 0 ∈ t<GOAL>s ⊆ s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<VAR>s : Finset α<VAR>t : Finset α<VAR>hs : 1 ∈ s<GOAL>t ⊆ s * t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<VAR>s : Finset α<VAR>t : Finset α<VAR>hs : 0 ∈ s<GOAL>t ⊆ s + t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<GOAL>⇑Finset.singletonAddMonoidHom = singleton
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<GOAL>⇑Finset.singletonMonoidHom = singleton
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<VAR>a : α<GOAL>Finset.singletonMonoidHom a = {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<VAR>a : α<GOAL>Finset.singletonAddMonoidHom a = {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<GOAL>⇑Finset.coeAddMonoidHom = CoeTC.coe
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<GOAL>⇑Finset.coeMonoidHom = CoeTC.coe
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulOneClass α<VAR>s : Finset α<GOAL>Finset.coeMonoidHom s = ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddZeroClass α<VAR>s : Finset α<GOAL>Finset.coeAddMonoidHom s = ↑s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>MulOneClass α<VAR>MulOneClass β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<GOAL>∀ (a : Finset α), (Finset.imageMonoidHom f) a = (Finset.imageMulHom f).toFun a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>AddZeroClass α<VAR>AddZeroClass β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<GOAL>∀ (a : Finset α), (Finset.imageAddMonoidHom f) a = (Finset.imageAddHom f).toFun a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>n : ℕ<GOAL>↑(n • s) = n • ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>n : ℕ<GOAL>↑(s ^ n) = ↑s ^ n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>a ^ n ∈ s ^ n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>a : α<VAR>ha : a ∈ s<VAR>n : ℕ<GOAL>n • a ∈ n • s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s t : Finset α<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>s ^ n ⊆ t ^ n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s t : Finset α<VAR>hst : s ⊆ t<VAR>n : ℕ<GOAL>n • s ⊆ n • t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>m n : ℕ<VAR>hs : 0 ∈ s<GOAL>m ≤ n → m • s ⊆ n • s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>m n : ℕ<VAR>hs : 1 ∈ s<GOAL>m ≤ n → s ^ m ⊆ s ^ n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : List (Finset α)<GOAL>↑s.prod = (List.map Finset.toSet s).prod
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : List (Finset α)<GOAL>↑s.sum = (List.map Finset.toSet s).sum
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>n : ℕ<VAR>a : α<VAR>s : Fin n → Finset α<GOAL>a ∈ (List.ofFn s).prod ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>n : ℕ<VAR>a : α<VAR>s : Fin n → Finset α<GOAL>a ∈ (List.ofFn s).sum ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ s ^ n ↔ ∃ f, (List.ofFn fun i => ↑(f i)).prod = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>a : α<VAR>n : ℕ<GOAL>a ∈ n • s ↔ ∃ f, (List.ofFn fun i => ↑(f i)).sum = a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>n • ∅ = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>∅ ^ n = ∅
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>s : Finset α<VAR>Fintype α<VAR>hs : 0 ∈ s<GOAL>s + Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>s : Finset α<VAR>Fintype α<VAR>hs : 1 ∈ s<GOAL>s * Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>t : Finset α<VAR>Fintype α<VAR>ht : 1 ∈ t<GOAL>Finset.univ * t = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>t : Finset α<VAR>Fintype α<VAR>ht : 0 ∈ t<GOAL>Finset.univ + t = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>Fintype α<GOAL>Finset.univ + Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>Fintype α<GOAL>Finset.univ * Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>n : ℕ<VAR>Fintype α<VAR>hn : n ≠ 0<GOAL>Finset.univ ^ n = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>n : ℕ<VAR>Fintype α<VAR>hn : n ≠ 0<GOAL>n • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Monoid α<VAR>a : α<GOAL>IsUnit a → IsUnit {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddMonoid α<VAR>a : α<GOAL>IsAddUnit a → IsAddUnit {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddCommMonoid α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → Finset α<GOAL>↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>CommMonoid α<VAR>ι : Type u_5<VAR>s : Finset ι<VAR>f : ι → Finset α<GOAL>↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DivisionMonoid α<VAR>s : Finset α<VAR>n : ℤ<GOAL>↑(s ^ n) = ↑s ^ n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SubtractionMonoid α<VAR>s : Finset α<VAR>n : ℤ<GOAL>↑(n • s) = n • ↑s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DivisionMonoid α<VAR>s t : Finset α<GOAL>s * t = 1 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a * b = 1
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SubtractionMonoid α<VAR>s t : Finset α<GOAL>s + t = 0 ↔ ∃ a b, s = {a} ∧ t = {b} ∧ a + b = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DivisionMonoid α<VAR>s : Finset α<GOAL>IsUnit s ↔ ∃ a, s = {a} ∧ IsUnit a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SubtractionMonoid α<VAR>s : Finset α<GOAL>IsAddUnit s ↔ ∃ a, s = {a} ∧ IsAddUnit a
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DivisionMonoid α<VAR>s : Finset α<GOAL>IsUnit ↑s ↔ IsUnit s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SubtractionMonoid α<VAR>s : Finset α<GOAL>IsAddUnit ↑s ↔ IsAddUnit s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>SubtractionMonoid α<VAR>Fintype α<GOAL>Finset.univ - Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>DivisionMonoid α<VAR>Fintype α<GOAL>Finset.univ / Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Distrib α<VAR>s t u : Finset α<GOAL>s * (t + u) ⊆ s * t + s * u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Distrib α<VAR>s t u : Finset α<GOAL>(s + t) * u ⊆ s * u + t * u
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>s : Finset α<GOAL>s * 0 ⊆ 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>s : Finset α<GOAL>0 * s ⊆ 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s * 0 = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>MulZeroClass α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>0 * s = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>s t : Finset α<GOAL>0 ∈ s - t ↔ ¬Disjoint s t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>s t : Finset α<GOAL>1 ∈ s / t ↔ ¬Disjoint s t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>s t : Finset α<GOAL>0 ∉ s - t ↔ Disjoint s t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>s t : Finset α<GOAL>1 ∉ s / t ↔ Disjoint s t
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>1 ∈ s / s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>s : Finset α<VAR>h : s.Nonempty<GOAL>0 ∈ s - s
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>a : α<GOAL>IsUnit {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>a : α<GOAL>IsAddUnit {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>s : Finset α<GOAL>IsUnit s ↔ ∃ a, s = {a}
<VAR>α : Type u_2<VAR>Group α<VAR>s : Finset α<GOAL>(∃ a, s = {a} ∧ IsUnit a) ↔ ∃ a, s = {a}
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>t : Finset α<VAR>a : α<GOAL>Finset.image (fun b => a * b) t = t.preimage (fun b => a⁻¹ * b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>t : Finset α<VAR>a : α<GOAL>Finset.image (fun b => a + b) t = t.preimage (fun b => -a + b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>t : Finset α<VAR>b : α<GOAL>Finset.image (fun x => x + b) t = t.preimage (fun x => x + -b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>t : Finset α<VAR>b : α<GOAL>Finset.image (fun x => x * b) t = t.preimage (fun x => x * b⁻¹) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>t : Finset α<VAR>a : α<GOAL>Finset.image (fun b => a⁻¹ * b) t = t.preimage (fun b => a * b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>t : Finset α<VAR>a : α<GOAL>Finset.image (fun b => -a + b) t = t.preimage (fun b => a + b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>Group α<VAR>t : Finset α<VAR>b : α<GOAL>Finset.image (fun x => x * b⁻¹) t = t.preimage (fun x => x * b) ⋯
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>AddGroup α<VAR>t : Finset α<VAR>b : α<GOAL>Finset.image (fun x => x + -b) t = t.preimage (fun x => x + b) ⋯
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Group α<VAR>DivisionMonoid β<VAR>FunLike F α β<VAR>MonoidHomClass 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>GroupWithZero α<VAR>s : Finset α<GOAL>s / 0 ⊆ 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GroupWithZero α<VAR>s : Finset α<GOAL>0 / s ⊆ 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GroupWithZero α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s / 0 = 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>GroupWithZero α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>0 / s = 0
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a b : α<GOAL>{b}.preimage (fun x => a + x) ⋯ = {-a + b}
<VAR>α : Type u_2<VAR>Group α<VAR>a b : α<GOAL>{b}.preimage (fun x => a * x) ⋯ = {a⁻¹ * b}
<VAR>α : Type u_2<VAR>Group α<VAR>a b : α<GOAL>{b}.preimage (fun x => x * a) ⋯ = {b * a⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a b : α<GOAL>{b}.preimage (fun x => x + a) ⋯ = {b + -a}
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>Finset.preimage 1 (fun x => a * x) ⋯ = {a⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>Finset.preimage 0 (fun x => a + x) ⋯ = {-a}
<VAR>α : Type u_2<VAR>Group α<VAR>b : α<GOAL>Finset.preimage 1 (fun x => x * b) ⋯ = {b⁻¹}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>b : α<GOAL>Finset.preimage 0 (fun x => x + b) ⋯ = {-b}
<VAR>α : Type u_2<VAR>Group α<VAR>a : α<GOAL>Finset.preimage 1 (fun x => a⁻¹ * x) ⋯ = {a}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>a : α<GOAL>Finset.preimage 0 (fun x => -a + x) ⋯ = {a}
<VAR>α : Type u_2<VAR>Group α<VAR>b : α<GOAL>Finset.preimage 1 (fun x => x * b⁻¹) ⋯ = {b}
<VAR>α : Type u_2<VAR>AddGroup α<VAR>b : α<GOAL>Finset.preimage 0 (fun x => x + -b) ⋯ = {b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s +ᵥ t = Finset.image (fun p => p.1 +ᵥ p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s • t = Finset.image (fun p => p.1 • p.2) (s ×ˢ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image (fun x => x.1 +ᵥ x.2) (s ×ˢ t) = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>Finset.image (fun x => x.1 • x.2) (s ×ˢ t) = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<VAR>x : β<GOAL>x ∈ s +ᵥ t ↔ ∃ y ∈ s, ∃ z ∈ t, y +ᵥ z = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<VAR>x : β<GOAL>x ∈ s • t ↔ ∃ y ∈ s, ∃ z ∈ t, y • z = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>↑(s • t) = ↑s • ↑t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>↑(s +ᵥ t) = ↑s +ᵥ ↑t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<GOAL>a ∈ s → b ∈ t → a • b ∈ s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<VAR>a : α<VAR>b : β<GOAL>a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s +ᵥ t).card ≤ s.card • t.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s • t).card ≤ s.card • t.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>t : Finset β<GOAL>∅ • t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>t : Finset β<GOAL>∅ +ᵥ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<GOAL>s +ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<GOAL>s • ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s • t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s.Nonempty → t.Nonempty → (s • t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s +ᵥ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s • t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s • t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s +ᵥ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>b : β<GOAL>s +ᵥ {b} = Finset.image (fun x => x +ᵥ b) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>b : β<GOAL>s • {b} = Finset.image (fun x => x • b) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>{a} • {b} = {a • b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>{a} +ᵥ {b} = {a +ᵥ b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t₁ t₂ : Finset β<GOAL>t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t₁ t₂ : Finset β<GOAL>t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset α<VAR>t : Finset β<GOAL>s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s₁ s₂ : Finset α<VAR>t : Finset β<GOAL>s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t u : Finset β<GOAL>s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t u : Finset β<GOAL>s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s₁ s₂ : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>(s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t