ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>s₁ ∪ s₂ +ᵥ 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>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>s • (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 β<VAR>DecidableEq α<GOAL>s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)
<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
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t₁ t₂ : Finset β<GOAL>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>s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>DecidableEq α<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 β<VAR>DecidableEq α<GOAL>(s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset α<VAR>t₁ t₂ : Finset β<VAR>DecidableEq α<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 β<VAR>DecidableEq α<GOAL>(s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>u : Finset β<VAR>s : Set α<VAR>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>SMul α β<VAR>u : Finset β<VAR>s : Set α<VAR>t : Set β<GOAL>↑u ⊆ s • t → ∃ s' t', ↑s' ⊆ s ∧ ↑t' ⊆ t ∧ u ⊆ s' • t'
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>s -ᵥ t = Finset.image₂ (fun x x_1 => x -ᵥ x_1) s t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>Finset.image₂ (fun x x_1 => x -ᵥ x_1) s t = s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<VAR>a : α<GOAL>a ∈ s -ᵥ t ↔ ∃ b ∈ s, ∃ c ∈ t, b -ᵥ c = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>↑(s -ᵥ t) = ↑s -ᵥ ↑t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<VAR>b c : β<GOAL>b ∈ s → c ∈ t → b -ᵥ c ∈ s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>(s -ᵥ t).card ≤ s.card * t.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>t : Finset β<GOAL>∅ -ᵥ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s : Finset β<GOAL>s -ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>(s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>(s -ᵥ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<GOAL>(s -ᵥ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s : Finset β<VAR>b : β<GOAL>s -ᵥ {b} = Finset.image (fun x => x -ᵥ b) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>t : Finset β<VAR>a : β<GOAL>{a} -ᵥ t = Finset.image (fun x => a -ᵥ x) t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>a b : β<GOAL>{a} -ᵥ {b} = {a -ᵥ b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s₁ s₂ t₁ t₂ : Finset β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset β<GOAL>t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s₁ s₂ t : Finset β<GOAL>s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t : Finset β<VAR>u : Finset α<GOAL>s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s₁ s₂ t : Finset β<VAR>DecidableEq β<GOAL>s₁ ∪ s₂ -ᵥ t = s₁ -ᵥ t ∪ (s₂ -ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset β<VAR>DecidableEq β<GOAL>s -ᵥ (t₁ ∪ t₂) = s -ᵥ t₁ ∪ (s -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s₁ s₂ t : Finset β<VAR>DecidableEq β<GOAL>s₁ ∩ s₂ -ᵥ t ⊆ (s₁ -ᵥ t) ∩ (s₂ -ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<VAR>s t₁ t₂ : Finset β<VAR>DecidableEq β<GOAL>s -ᵥ t₁ ∩ t₂ ⊆ (s -ᵥ t₁) ∩ (s -ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>DecidableEq α<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>SMul α β<VAR>s : Finset β<VAR>a : α<GOAL>a • s = Finset.image (fun x => a • x) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<GOAL>a +ᵥ s = Finset.image (fun x => a +ᵥ x) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<GOAL>Finset.image (fun x => a +ᵥ x) s = a +ᵥ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<GOAL>Finset.image (fun x => a • x) s = a • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<VAR>x : β<GOAL>x ∈ a +ᵥ s ↔ ∃ y ∈ s, a +ᵥ y = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<VAR>x : β<GOAL>x ∈ a • s ↔ ∃ y ∈ s, a • y = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>a : α<VAR>s : Finset β<GOAL>↑(a • s) = a • ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>a : α<VAR>s : Finset β<GOAL>↑(a +ᵥ s) = a +ᵥ ↑s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>b ∈ s → a • b ∈ a • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>b ∈ s → a +ᵥ b ∈ a +ᵥ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<GOAL>(a • s).card ≤ s.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<GOAL>(a +ᵥ s).card ≤ s.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>a : α<GOAL>a • ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>a : α<GOAL>a +ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<GOAL>a +ᵥ s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<GOAL>a • s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<GOAL>(a • s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<GOAL>(a +ᵥ s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset β<VAR>a : α<VAR>hs : s.Nonempty<GOAL>(a +ᵥ s).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset β<VAR>a : α<VAR>hs : s.Nonempty<GOAL>(a • s).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>t : Finset β<VAR>a : α<GOAL>{a} • t = a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>t : Finset β<VAR>a : α<GOAL>{a} +ᵥ t = a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s t : Finset β<VAR>a : α<GOAL>s ⊆ t → a +ᵥ s ⊆ a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s t : Finset β<VAR>a : α<GOAL>s ⊆ t → a • s ⊆ a • t
<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>a : α<GOAL>a +ᵥ (s₁ ∪ s₂) = a +ᵥ s₁ ∪ (a +ᵥ s₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s₁ s₂ : Finset β<VAR>a : α<GOAL>a • (s₁ ∪ s₂) = a • s₁ ∪ a • s₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s₁ s₂ : Finset β<VAR>a : α<GOAL>a +ᵥ s₁ ∩ s₂ ⊆ (a +ᵥ s₁) ∩ (a +ᵥ s₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s₁ s₂ : Finset β<VAR>a : α<GOAL>a • (s₁ ∩ s₂) ⊆ a • s₁ ∩ a • s₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>t : Finset β<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s → a +ᵥ t ⊆ s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>t : Finset β<VAR>a : α<VAR>s : Finset α<GOAL>a ∈ s → a • t ⊆ s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>VAdd α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s.biUnion fun x => x +ᵥ t) = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>SMul α β<VAR>s : Finset α<VAR>t : Finset β<GOAL>(s.biUnion fun x => x • t) = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>VAdd αᵃᵒᵖ β<VAR>VAdd β γ<VAR>VAdd α γ<VAR>a : α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : ∀ (a : α) (b : β) (c : γ), AddOpposite.op a +ᵥ b +ᵥ c = b +ᵥ (a +ᵥ c)<GOAL>AddOpposite.op a +ᵥ s +ᵥ t = s +ᵥ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SMul αᵐᵒᵖ β<VAR>SMul β γ<VAR>SMul α γ<VAR>a : α<VAR>s : Finset β<VAR>t : Finset γ<VAR>h : ∀ (a : α) (b : β) (c : γ), (MulOpposite.op a • b) • c = b • a • c<GOAL>(MulOpposite.op a • s) • t = s • a • t
<VAR>α : Type u_2<VAR>Add α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>a ∈ t → MulOpposite.op a • s ⊆ s * t
<VAR>α : Type u_2<VAR>Mul α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(t.biUnion fun a => MulOpposite.op a • s) = s * t
<VAR>α : Type u_2<VAR>Add α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>(t.biUnion fun a => AddOpposite.op a +ᵥ s) = s + t
<VAR>α : Type u_2<VAR>Add α<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u
<VAR>α : Type u_2<VAR>Mul α<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
<VAR>α : Type u_2<VAR>Mul α<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u
<VAR>α : Type u_2<VAR>Add α<VAR>DecidableEq α<VAR>s t u : Finset α<GOAL>s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u
<VAR>α : Type u_2<VAR>Semigroup α<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>MulOpposite.op a • s * t = s * a • t
<VAR>α : Type u_2<VAR>AddSemigroup α<VAR>DecidableEq α<VAR>a : α<VAR>s t : Finset α<GOAL>AddOpposite.op a +ᵥ s + t = s + (a +ᵥ t)
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>DecidableEq α<VAR>s : Set α<VAR>t : Finset α<GOAL>(s.PairwiseDisjoint fun x => x +ᵥ t) ↔ Set.InjOn (fun p => p.1 + p.2) (s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>DecidableEq α<VAR>s : Set α<VAR>t : Finset α<GOAL>(s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 * p.2) (s ×ˢ ↑t)
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>DecidableEq α<VAR>t : Finset α<VAR>a : α<GOAL>({a} * t).card = t.card
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>DecidableEq α<VAR>t : Finset α<VAR>a : α<GOAL>({a} + t).card = t.card
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>{a} + s ∩ t = ({a} + s) ∩ ({a} + t)
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>{a} * (s ∩ t) = {a} * s ∩ ({a} * t)
<VAR>α : Type u_2<VAR>Add α<VAR>IsLeftCancelAdd α<VAR>DecidableEq α<VAR>t : Finset α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>t.card ≤ (s + t).card
<VAR>α : Type u_2<VAR>Mul α<VAR>IsLeftCancelMul α<VAR>DecidableEq α<VAR>t : Finset α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>t.card ≤ (s * t).card
<VAR>α : Type u_2<VAR>Add α<VAR>IsRightCancelAdd α<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(s + {a}).card = s.card
<VAR>α : Type u_2<VAR>Mul α<VAR>IsRightCancelMul α<VAR>DecidableEq α<VAR>s : Finset α<VAR>a : α<GOAL>(s * {a}).card = s.card
<VAR>α : Type u_2<VAR>Mul α<VAR>IsRightCancelMul α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>s ∩ t * {a} = s * {a} ∩ (t * {a})
<VAR>α : Type u_2<VAR>Add α<VAR>IsRightCancelAdd α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>a : α<GOAL>s ∩ t + {a} = (s + {a}) ∩ (t + {a})
<VAR>α : Type u_2<VAR>Mul α<VAR>IsRightCancelMul α<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : t.Nonempty<GOAL>s.card ≤ (s * t).card
<VAR>α : Type u_2<VAR>Add α<VAR>IsRightCancelAdd α<VAR>DecidableEq α<VAR>s : Finset α<VAR>t : Finset α<VAR>ht : t.Nonempty<GOAL>s.card ≤ (s + t).card
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>t.card ≤ (s / t).card
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>hs : s.Nonempty<GOAL>t.card ≤ (s - t).card
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>ht : t.Nonempty<GOAL>s.card ≤ (s / t).card
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<VAR>ht : t.Nonempty<GOAL>s.card ≤ (s - t).card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>SMul α β<VAR>SMul α γ<VAR>f : β → γ<VAR>a : α<VAR>s : Finset β<GOAL>(∀ (b : β), f (a • b) = a • f b) → Finset.image f (a • s) = a • Finset.image f s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>DecidableEq β<VAR>DecidableEq γ<VAR>VAdd α β<VAR>VAdd α γ<VAR>f : β → γ<VAR>a : α<VAR>s : Finset β<GOAL>(∀ (b : β), f (a +ᵥ b) = a +ᵥ f b) → Finset.image f (a +ᵥ s) = a +ᵥ Finset.image f s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>AddMonoid α<VAR>AddMonoid β<VAR>FunLike F α β<VAR>AddMonoidHomClass F α β<VAR>f : F<VAR>a : α<VAR>s : Finset α<GOAL>Finset.image (⇑f) (a +ᵥ s) = f a +ᵥ Finset.image (⇑f) s
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq α<VAR>DecidableEq β<VAR>Monoid α<VAR>Monoid β<VAR>FunLike F α β<VAR>MonoidHomClass F α β<VAR>f : F<VAR>a : α<VAR>s : Finset α<GOAL>Finset.image (⇑f) (a • s) = f a • Finset.image (⇑f) s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s : Finset β<VAR>b : β<VAR>a : α<GOAL>a • b ∈ a • s ↔ b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Finset β<VAR>b : β<VAR>a : α<GOAL>a +ᵥ b ∈ a +ᵥ s ↔ b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>a⁻¹ • b ∈ s ↔ b ∈ a • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>-a +ᵥ b ∈ s ↔ b ∈ a +ᵥ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>b ∈ -a +ᵥ s ↔ a +ᵥ b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<GOAL>b ∈ a⁻¹ • s ↔ a • b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a +ᵥ s ⊆ a +ᵥ t ↔ s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a • s ⊆ a • t ↔ s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a +ᵥ s ⊆ t ↔ s ⊆ -a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a • s ⊆ t ↔ s ⊆ a⁻¹ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>s ⊆ a +ᵥ t ↔ -a +ᵥ s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>s ⊆ a • t ↔ a⁻¹ • s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a +ᵥ s ∩ t = (a +ᵥ s) ∩ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a • (s ∩ t) = a • s ∩ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a +ᵥ s \ t = (a +ᵥ s) \ (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a • (s \ t) = a • s \ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a • symmDiff s t = symmDiff (a • s) (a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>s t : Finset β<VAR>a : α<GOAL>a +ᵥ symmDiff s t = symmDiff (a +ᵥ s) (a +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>Fintype β<GOAL>a • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>Fintype β<GOAL>a +ᵥ Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>Fintype β<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s +ᵥ Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>Fintype β<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>a : α<VAR>s : Finset β<GOAL>(a • s).card = s.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>a : α<VAR>s : Finset β<GOAL>(a +ᵥ s).card = s.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>Group α<VAR>MulAction α β<VAR>t : Finset β<VAR>s : Finset α<GOAL>((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s • t).card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>AddGroup α<VAR>AddAction α β<VAR>t : Finset β<VAR>s : Finset α<GOAL>((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s +ᵥ t).card
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>((fun b => Finset.image (fun a => a + b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s + t).card
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>((fun b => Finset.image (fun a => a * b) s) '' ↑t).PairwiseDisjoint id → s.card ∣ (s * t).card
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>((fun x => x • t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s * t).card
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>s t : Finset α<GOAL>((fun x => x +ᵥ t) '' ↑s).PairwiseDisjoint id → t.card ∣ (s + t).card
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>-(a +ᵥ s) = AddOpposite.op (-a) +ᵥ -s
<VAR>α : Type u_2<VAR>Group α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>AddGroup α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>-(AddOpposite.op a +ᵥ s) = -a +ᵥ -s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>DecidableEq β<VAR>s : Finset α<GOAL>s • 0 ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>DecidableEq β<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>s • 0 = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>DecidableEq β<VAR>t : Finset β<VAR>a : α<VAR>h : 0 ∈ t<GOAL>0 ∈ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero β<VAR>SMulZeroClass α β<VAR>DecidableEq β<VAR>t : Finset β<VAR>a : α<VAR>Zero α<VAR>NoZeroSMulDivisors α β<VAR>ha : a ≠ 0<GOAL>0 ∈ a • t ↔ 0 ∈ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>DecidableEq β<VAR>t : Finset β<GOAL>0 • t ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>DecidableEq β<VAR>t : Finset β<VAR>ht : t.Nonempty<GOAL>0 • t = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>DecidableEq β<VAR>s : Finset β<VAR>h : s.Nonempty<GOAL>0 • s = 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>DecidableEq β<VAR>s : Finset β<GOAL>0 • s ⊆ 0
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Zero α<VAR>Zero β<VAR>SMulWithZero α β<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>NoZeroSMulDivisors α β<GOAL>0 ∈ s • t ↔ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<VAR>ha : a ≠ 0<GOAL>a • b ∈ a • s ↔ b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<VAR>ha : a ≠ 0<GOAL>a⁻¹ • b ∈ s ↔ b ∈ a • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s : Finset β<VAR>a : α<VAR>b : β<VAR>ha : a ≠ 0<GOAL>b ∈ a⁻¹ • s ↔ a • b ∈ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • s ⊆ a • t ↔ s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • s ⊆ t ↔ s ⊆ a⁻¹ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>s ⊆ a • t ↔ a⁻¹ • s ⊆ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • (s ∩ t) = a • s ∩ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • (s \ t) = a • s \ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>s t : Finset β<VAR>a : α<VAR>ha : a ≠ 0<GOAL>a • symmDiff s t = symmDiff (a • s) (a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>a : α<VAR>Fintype β<VAR>ha : a ≠ 0<GOAL>a • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>Fintype β<VAR>s : Finset α<VAR>hs : ¬s ⊆ 0<GOAL>s • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>GroupWithZero α<VAR>MulAction α β<VAR>Fintype β<VAR>s : Finset α<VAR>hs : s.Nontrivial<GOAL>s • Finset.univ = Finset.univ
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>DecidableEq α<GOAL>0⁻¹ = 0
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(a • s)⁻¹ = MulOpposite.op a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>GroupWithZero α<VAR>DecidableEq α<VAR>a : α<VAR>s : Finset α<GOAL>(MulOpposite.op a • s)⁻¹ = a⁻¹ • s⁻¹
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid α<VAR>AddGroup β<VAR>DistribMulAction α β<VAR>DecidableEq β<VAR>a : α<VAR>t : Finset β<GOAL>a • -t = -(a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Monoid α<VAR>AddGroup β<VAR>DistribMulAction α β<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<GOAL>s • -t = -(s • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>DecidableEq β<VAR>t : Finset β<VAR>a : α<GOAL>-a • t = -(a • t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>Ring α<VAR>AddCommGroup β<VAR>Module α β<VAR>DecidableEq β<VAR>s : Finset α<VAR>t : Finset β<VAR>DecidableEq α<GOAL>-s • t = -(s • t)