ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ<VAR>OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>AddCommGroup U<VAR>Module R U<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>r : R<VAR>u : U<GOAL>A.compHahnSeries B (r • u) = r • A.compHahnSeries B u
<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ<VAR>OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>AddCommGroup U<VAR>Module R U<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>u : U<GOAL>(A.comp B) u = (HahnModule.of R) (A.compHahnSeries B u).ofIterate
<VAR>Γ : Type u_5<VAR>Γ' : Type u_6<VAR>OrderedCancelAddCommMonoid Γ<VAR>OrderedCancelAddCommMonoid Γ'<VAR>R : Type u_7<VAR>CommRing R<VAR>U : Type u_8<VAR>V : Type u_9<VAR>W : Type u_10<VAR>AddCommGroup U<VAR>Module R U<VAR>AddCommGroup V<VAR>Module R V<VAR>AddCommGroup W<VAR>Module R W<VAR>A : HVertexOperator Γ R V W<VAR>B : HVertexOperator Γ' R U V<VAR>g : Lex (Γ' × Γ)<GOAL>(A.comp B).coeff g = A.coeff (ofLex g).2 ∘ₗ B.coeff (ofLex g).1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>OrderedAddCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x + y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommMonoid M<VAR>OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs_nonempty : s.Nonempty<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>OrderedAddCommMonoid N<VAR>f : M → N<VAR>h_mul : ∀ (x y : M), f (x + y) ≤ f x + f y<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → M<GOAL>f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommMonoid M<VAR>OrderedCommMonoid N<VAR>f : M → N<VAR>h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>g : ι → M<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>OrderedAddCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_one : f 0 = 0<VAR>h_mul : ∀ (x y : M), p x → p y → f (x + y) ≤ f x + f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x + y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommMonoid M<VAR>OrderedCommMonoid N<VAR>f : M → N<VAR>p : M → Prop<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), p x → p y → f (x * y) ≤ f x * f y<VAR>hp_mul : ∀ (x y : M), p x → p y → p (x * y)<VAR>g : ι → M<VAR>s : Finset ι<VAR>hs : ∀ i ∈ s, p (g i)<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>CommMonoid M<VAR>OrderedCommMonoid N<VAR>f : M → N<VAR>h_one : f 1 = 1<VAR>h_mul : ∀ (x y : M), f (x * y) ≤ f x * f y<VAR>s : Finset ι<VAR>g : ι → M<GOAL>f (∏ i ∈ s, g i) ≤ ∏ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>N : Type u_5<VAR>AddCommMonoid M<VAR>OrderedAddCommMonoid N<VAR>f : M → N<VAR>h_one : f 0 = 0<VAR>h_mul : ∀ (x y : M), f (x + y) ≤ f x + f y<VAR>s : Finset ι<VAR>g : ι → M<GOAL>f (∑ i ∈ s, g i) ≤ ∑ i ∈ s, f (g i)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f g : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>∑ i ∈ s, f i ≤ ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f g : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>∏ i ∈ s, f i ≤ ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f g : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>s.prod f ≤ s.prod g
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f g : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>s.sum f ≤ s.sum g
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 1 ≤ f i<GOAL>1 ≤ ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 0 ≤ f i<GOAL>0 ≤ ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ (i : ι), 1 ≤ f i<GOAL>1 ≤ ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ (i : ι), 0 ≤ f i<GOAL>0 ≤ ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ 0<GOAL>∑ i ∈ s, f i ≤ 0
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ 1<GOAL>∏ i ∈ s, f i ≤ 1
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hf : ∀ i ∈ t, i ∉ s → 1 ≤ f i<GOAL>∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>hf : ∀ i ∈ t, i ∉ s → 0 ≤ f i<GOAL>∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>hf : ∀ (x : ι), 1 ≤ f x<GOAL>Monotone fun s => ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>hf : ∀ (x : ι), 0 ≤ f x<GOAL>Monotone fun s => ∑ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>Fintype ι<VAR>s : Finset ι<VAR>w : ∀ (x : ι), 0 ≤ f x<GOAL>∑ x ∈ s, f x ≤ ∑ x : ι, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>Fintype ι<VAR>s : Finset ι<VAR>w : ∀ (x : ι), 1 ≤ f x<GOAL>∏ x ∈ s, f x ≤ ∏ x : ι, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<GOAL>(∀ i ∈ s, 0 ≤ f i) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<GOAL>(∀ i ∈ s, 1 ≤ f i) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<GOAL>(∀ i ∈ s, f i ≤ 0) → (∑ i ∈ s, f i = 0 ↔ ∀ i ∈ s, f i = 0)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<GOAL>(∀ i ∈ s, f i ≤ 1) → (∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1)
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 1 ≤ f i<VAR>a : ι<VAR>h : a ∈ s<GOAL>f a ≤ ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>a : ι<VAR>h : a ∈ s<GOAL>f a ≤ ∑ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>i j : ι<VAR>hf : ∀ i ∈ s, 0 ≤ f i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hne : i ≠ j<GOAL>f i + f j ≤ ∑ k ∈ s, f k
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>f : ι → N<VAR>s : Finset ι<VAR>i j : ι<VAR>hf : ∀ i ∈ s, 1 ≤ f i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hne : i ≠ j<GOAL>f i * f j ≤ ∏ k ∈ s, f k
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, f x ≤ n<GOAL>s.sum f ≤ s.card • n
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, f x ≤ n<GOAL>s.prod f ≤ n ^ s.card
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, n ≤ f x<GOAL>n ^ s.card ≤ s.prod f
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>s : Finset ι<VAR>f : ι → N<VAR>n : N<VAR>h : ∀ x ∈ s, n ≤ f x<GOAL>s.card • n ≤ s.sum f
<VAR>ι : Type u_1<VAR>β : Type u_3<VAR>DecidableEq β<VAR>s : Finset ι<VAR>f : ι → Finset β<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (f a).card ≤ n<GOAL>(s.biUnion f).card ≤ s.card * n
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>s : Finset ι<VAR>ι' : Type u_9<VAR>DecidableEq ι'<VAR>t : Finset ι'<VAR>g : ι → ι'<VAR>f : ι → N<VAR>h : ∀ y ∉ t, 0 ≤ ∑ x ∈ Finset.filter (fun x => g x = y) s, f x<GOAL>∑ y ∈ t, ∑ x ∈ Finset.filter (fun x => g x = y) s, f x ≤ ∑ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>s : Finset ι<VAR>ι' : Type u_9<VAR>DecidableEq ι'<VAR>t : Finset ι'<VAR>g : ι → ι'<VAR>f : ι → N<VAR>h : ∀ y ∉ t, 1 ≤ ∏ x ∈ Finset.filter (fun x => g x = y) s, f x<GOAL>∏ y ∈ t, ∏ x ∈ Finset.filter (fun x => g x = y) s, f x ≤ ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedAddCommMonoid N<VAR>s : Finset ι<VAR>ι' : Type u_9<VAR>DecidableEq ι'<VAR>t : Finset ι'<VAR>g : ι → ι'<VAR>f : ι → N<VAR>h : ∀ y ∉ t, ∑ x ∈ Finset.filter (fun x => g x = y) s, f x ≤ 0<GOAL>∑ x ∈ s, f x ≤ ∑ y ∈ t, ∑ x ∈ Finset.filter (fun x => g x = y) s, f x
<VAR>ι : Type u_1<VAR>N : Type u_5<VAR>OrderedCommMonoid N<VAR>s : Finset ι<VAR>ι' : Type u_9<VAR>DecidableEq ι'<VAR>t : Finset ι'<VAR>g : ι → ι'<VAR>f : ι → N<VAR>h : ∀ y ∉ t, ∏ x ∈ Finset.filter (fun x => g x = y) s, f x ≤ 1<GOAL>∏ x ∈ s, f x ≤ ∏ y ∈ t, ∏ x ∈ Finset.filter (fun x => g x = y) s, f x
<VAR>ι : Type u_1<VAR>G : Type u_9<VAR>LinearOrderedAddCommGroup G<VAR>f : ι → G<VAR>s : Finset ι<GOAL>|∑ i ∈ s, f i| ≤ ∑ i ∈ s, |f i|
<VAR>ι : Type u_1<VAR>G : Type u_9<VAR>LinearOrderedAddCommGroup G<VAR>f : ι → G<VAR>s : Finset ι<VAR>hf : ∀ i ∈ s, 0 ≤ f i<GOAL>|∑ i ∈ s, f i| = ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>G : Type u_9<VAR>LinearOrderedAddCommGroup G<VAR>f : ι → G<VAR>s : Finset ι<VAR>hf : ∀ (i : ι), 0 ≤ f i<GOAL>|∑ i ∈ s, f i| = ∑ i ∈ s, f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>Hf : ∀ a ∈ s, f a ∈ t<VAR>n : ℕ<VAR>hn : ∀ a ∈ t, (Finset.filter (fun x => f x = a) s).card ≤ n<GOAL>s.card ≤ n * t.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>n : ℕ<VAR>hn : ∀ a ∈ Finset.image f s, (Finset.filter (fun x => f x = a) s).card ≤ n<GOAL>s.card ≤ n * (Finset.image f s).card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>Hf : ∀ a ∈ s, f a ∈ t<VAR>n : ℕ<VAR>hn : ∀ a ∈ t, n ≤ (Finset.filter (fun x => f x = a) s).card<GOAL>n * t.card ≤ s.card
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>DecidableEq β<VAR>f : α → β<VAR>s : Finset α<VAR>n : ℕ<VAR>hn : ∀ a ∈ Finset.image f s, n ≤ (Finset.filter (fun x => f x = a) s).card<GOAL>n * (Finset.image f s).card ≤ s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (Finset.filter (fun x => a ∈ x) B).card ≤ n<GOAL>∑ t ∈ B, (s ∩ t).card ≤ s.card * n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>Fintype α<VAR>h : ∀ (a : α), (Finset.filter (fun x => a ∈ x) B).card ≤ n<GOAL>∑ s ∈ B, s.card ≤ Fintype.card α * n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, n ≤ (Finset.filter (fun x => a ∈ x) B).card<GOAL>s.card * n ≤ ∑ t ∈ B, (s ∩ t).card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>Fintype α<VAR>h : ∀ (a : α), n ≤ (Finset.filter (fun x => a ∈ x) B).card<GOAL>Fintype.card α * n ≤ ∑ s ∈ B, s.card
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>h : ∀ a ∈ s, (Finset.filter (fun x => a ∈ x) B).card = n<GOAL>∑ t ∈ B, (s ∩ t).card = s.card * n
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>B : Finset (Finset α)<VAR>n : ℕ<VAR>Fintype α<VAR>h : ∀ (a : α), (Finset.filter (fun x => a ∈ x) B).card = n<GOAL>∑ s ∈ B, s.card = Fintype.card α * n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<VAR>hf : ∀ i ∈ s, (f i).Nonempty<GOAL>s.card ≤ (s.biUnion f).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hs : (↑s).PairwiseDisjoint f<GOAL>s.card ≤ (s.biUnion f).card + (Finset.filter (fun i => f i = ∅) s).card
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>DecidableEq α<VAR>s : Finset ι<VAR>f : ι → Finset α<VAR>hf : Function.Injective f<VAR>hs : (↑s).PairwiseDisjoint f<GOAL>s.card ≤ (s.biUnion f).card + 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>f i ≤ ∏ j ∈ s, f j
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>f i ≤ ∑ j ∈ s, f j
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<GOAL>∑ x ∈ s, f x = 0 ↔ ∀ x ∈ s, f x = 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<GOAL>∏ x ∈ s, f x = 1 ↔ ∀ x ∈ s, f x = 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : s ⊆ t<GOAL>∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : s ⊆ t<GOAL>∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>f : ι → M<GOAL>Monotone fun s => ∏ x ∈ s, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>f : ι → M<GOAL>Monotone fun s => ∑ x ∈ s, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : ∀ x ∈ s, f x ≠ 1 → x ∈ t<GOAL>∏ x ∈ s, f x ≤ ∏ x ∈ t, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>CanonicallyOrderedAddCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : ∀ x ∈ s, f x ≠ 0 → x ∈ t<GOAL>∑ x ∈ s, f x ≤ ∑ x ∈ t, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hle : ∀ i ∈ s, f i ≤ g i<VAR>hlt : ∃ i ∈ s, f i < g i<GOAL>∑ i ∈ s, f i < ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hle : ∀ i ∈ s, f i ≤ g i<VAR>hlt : ∃ i ∈ s, f i < g i<GOAL>∏ i ∈ s, f i < ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hlt : ∀ i ∈ s, f i < g i<GOAL>∏ i ∈ s, f i < ∏ i ∈ s, g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>hlt : ∀ i ∈ s, f i < g i<GOAL>∑ i ∈ s, f i < ∑ i ∈ s, g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>Hlt : ∀ i ∈ s, f i < g i<GOAL>s.sum f < s.sum g
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>Hlt : ∀ i ∈ s, f i < g i<GOAL>s.prod f < s.prod g
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>i : ι<VAR>ht : i ∈ t<VAR>hs : i ∉ s<VAR>hlt : 1 < f i<VAR>hle : ∀ j ∈ t, j ∉ s → 1 ≤ f j<GOAL>∏ j ∈ s, f j < ∏ j ∈ t, f j
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>h : s ⊆ t<VAR>i : ι<VAR>ht : i ∈ t<VAR>hs : i ∉ s<VAR>hlt : 0 < f i<VAR>hle : ∀ j ∈ t, j ∉ s → 0 ≤ f j<GOAL>∑ j ∈ s, f j < ∑ j ∈ t, f j
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>i j : ι<VAR>hij : j ≠ i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hlt : 0 < f j<VAR>hle : ∀ k ∈ s, k ≠ i → 0 ≤ f k<GOAL>f i < ∑ k ∈ s, f k
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>i j : ι<VAR>hij : j ≠ i<VAR>hi : i ∈ s<VAR>hj : j ∈ s<VAR>hlt : 1 < f j<VAR>hle : ∀ k ∈ s, k ≠ i → 1 ≤ f k<GOAL>f i < ∏ k ∈ s, f k
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 1 < f i<VAR>hs : s.Nonempty<GOAL>1 < ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 0 < f i<VAR>hs : s.Nonempty<GOAL>0 < ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i < 0<VAR>hs : s.Nonempty<GOAL>∑ i ∈ s, f i < 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i < 1<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, f i < 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 0 ≤ f i<VAR>hs : ∃ i ∈ s, 0 < f i<GOAL>0 < ∑ i ∈ s, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, 1 ≤ f i<VAR>hs : ∃ i ∈ s, 1 < f i<GOAL>1 < ∏ i ∈ s, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ 1<VAR>hs : ∃ i ∈ s, f i < 1<GOAL>∏ i ∈ s, f i < 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, f i ≤ 0<VAR>hs : ∃ i ∈ s, f i < 0<GOAL>∑ i ∈ s, f i < 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>∑ i ∈ s, f i = ∑ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>s : Finset ι<VAR>f g : ι → M<VAR>h : ∀ i ∈ s, f i ≤ g i<GOAL>∏ i ∈ s, f i = ∏ i ∈ s, g i ↔ ∀ i ∈ s, f i = g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>DecidableEq ι<GOAL>∑ i ∈ s \ t, f i ≤ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≤ ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>DecidableEq ι<GOAL>∏ i ∈ s \ t, f i ≤ ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i ≤ ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>DecidableEq ι<GOAL>∏ i ∈ s \ t, f i < ∏ i ∈ t \ s, f i ↔ ∏ i ∈ s, f i < ∏ i ∈ t, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>s t : Finset ι<VAR>DecidableEq ι<GOAL>∑ i ∈ s \ t, f i < ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i < ∑ i ∈ t, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelAddCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>Hlt : ∑ i ∈ s, f i < ∑ i ∈ s, g i<GOAL>∃ i ∈ s, f i < g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>Hlt : ∏ i ∈ s, f i < ∏ i ∈ s, g i<GOAL>∃ i ∈ s, f i < g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelAddCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>Hle : ∑ i ∈ s, f i ≤ ∑ i ∈ s, g i<GOAL>∃ i ∈ s, f i ≤ g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelCommMonoid M<VAR>f g : ι → M<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>Hle : ∏ i ∈ s, f i ≤ ∏ i ∈ s, g i<GOAL>∃ i ∈ s, f i ≤ g i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelCommMonoid M<VAR>s : Finset ι<VAR>f : ι → M<VAR>h₁ : ∏ i ∈ s, f i = 1<VAR>h₂ : ∃ i ∈ s, f i ≠ 1<GOAL>∃ i ∈ s, 1 < f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>LinearOrderedCancelAddCommMonoid M<VAR>s : Finset ι<VAR>f : ι → M<VAR>h₁ : ∑ i ∈ s, f i = 0<VAR>h₂ : ∃ i ∈ s, f i ≠ 0<GOAL>∃ i ∈ s, 0 < f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedAddCommMonoid M<GOAL>Monotone fun f => ∑ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCommMonoid M<GOAL>Monotone fun f => ∏ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : 1 ≤ f<GOAL>1 ≤ ∏ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedAddCommMonoid M<VAR>f : ι → M<VAR>hf : 0 ≤ f<GOAL>0 ≤ ∑ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedAddCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 0<GOAL>∑ i : ι, f i ≤ 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 1<GOAL>∏ i : ι, f i ≤ 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedAddCommMonoid M<VAR>f : ι → M<VAR>hf : 0 ≤ f<GOAL>∑ i : ι, f i = 0 ↔ f = 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : 1 ≤ f<GOAL>∏ i : ι, f i = 1 ↔ f = 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 1<GOAL>∏ i : ι, f i = 1 ↔ f = 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedAddCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 0<GOAL>∑ i : ι, f i = 0 ↔ f = 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelCommMonoid M<GOAL>StrictMono fun f => ∏ x : ι, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelAddCommMonoid M<GOAL>StrictMono fun f => ∑ x : ι, f x
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>hf : 0 < f<GOAL>0 < ∑ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : 1 < f<GOAL>1 < ∏ i : ι, f i
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : f < 1<GOAL>∏ i : ι, f i < 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>hf : f < 0<GOAL>∑ i : ι, f i < 0
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : 1 ≤ f<GOAL>1 < ∏ i : ι, f i ↔ 1 < f
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>hf : 0 ≤ f<GOAL>0 < ∑ i : ι, f i ↔ 0 < f
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 1<GOAL>∏ i : ι, f i < 1 ↔ f < 1
<VAR>ι : Type u_1<VAR>M : Type u_4<VAR>Fintype ι<VAR>OrderedCancelAddCommMonoid M<VAR>f : ι → M<VAR>hf : f ≤ 0<GOAL>∑ i : ι, f i < 0 ↔ f < 0
<VAR>α : Type u_2<VAR>DecidableEq α<VAR>β : Type u_9<VAR>i : Finset β<VAR>f : β → Multiset α<GOAL>i.sum f = i.sup f ↔ ∀ x ∈ i, ∀ y ∈ i, x ≠ y → (f x).Disjoint (f y)
<VAR>α : Type u_9<VAR>DecidableEq α<VAR>x : Multiset α<GOAL>((Finset.range (Multiset.card x + 1)).sup fun k => Multiset.powersetCard k x) = x.powerset
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.HasTrivialRadical R L<GOAL>LieAlgebra.radical R L = ⊥
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSimple R L<VAR>I : LieIdeal R L<GOAL>I = ⊥ ∨ I = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSimple R L<GOAL>¬IsLieAbelian L
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSemisimple R L<GOAL>CompleteLattice.SetIndependent {I | IsAtom I}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSemisimple R L<GOAL>sSup {I | IsAtom I} = ⊤
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>CommRing R<VAR>LieRing L<VAR>LieAlgebra R L<VAR>self : LieAlgebra.IsSemisimple R L<VAR>I : LieIdeal R L<GOAL>IsAtom I → ¬IsLieAbelian ↥↑I
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ (β_ (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv = X ◁ (β_ Y Z).hom ≫ (α_ X Z Y).inv ≫ (β_ X Z).hom ▷ Y
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.BraidedCategory C<VAR>X Y Z : C<GOAL>(α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom ≫ (α_ Y Z X).hom = (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.BraidedCategory C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>Z : C<GOAL>f ▷ Z ≫ (β_ Y Z).hom = (β_ X Z).hom ≫ Z ◁ f
<VAR>C : Type u<VAR>CategoryTheory.Category.{v, u} C<VAR>CategoryTheory.MonoidalCategory C<VAR>self : CategoryTheory.BraidedCategory C<VAR>X : C<VAR>Y Z : C<VAR>f : Y ⟶ Z<GOAL>X ◁ f ≫ (β_ X Z).hom = (β_ X Y).hom ≫ f ▷ X