ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<VAR>i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K<VAR>E' : IntermediateField F K := i.fieldRange<VAR>i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i<VAR>hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'<GOAL>(adjoin E ↑L).toSubalgebra = Algebra.adjoin E ↑L
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<VAR>i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K<VAR>E' : IntermediateField F K := i.fieldRange<VAR>i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i<VAR>hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'<GOAL>Subalgebra.restrictScalars F (adjoin E ↑L).toSubalgebra = Subalgebra.restrictScalars F (Algebra.adjoin E ↑L)
<VAR>F : Type u_1<VAR>inst✝⁶ : Field F<VAR>E : Type u_2<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>S : Set E<VAR>α : E<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>L : IntermediateField F K<VAR>halg : Algebra.IsAlgebraic F E ∨ Algebra.IsAlgebraic F ↥L<VAR>i : E →ₐ[F] K := IsScalarTower.toAlgHom F E K<VAR>E' : IntermediateField F K := i.fieldRange<VAR>i' : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField i<VAR>hi : ⇑(algebraMap E K) = ⇑(algebraMap (↥E') K) ∘ ⇑i'<GOAL>(adjoin F (↑E' ∪ ↑L)).toSubalgebra = Algebra.adjoin F (↑E'.toSubalgebra ∪ ↑L)
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : n < finrank R M<GOAL>↑n < Module.rank R M
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : n < finrank R M<GOAL>↑n < ℵ₀
<VAR>R : Type u<VAR>M : Type v<VAR>N : Type w<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>n : ℕ<VAR>h : n < finrank R M<GOAL>Module.rank R M < ℵ₀
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<GOAL>↑⊥ = {0}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>s : Multiset (ι →₀ M)<VAR>hs : Pairwise (_root_.Disjoint on Finsupp.support) s<GOAL>s.sum.support = (map Finsupp.support s).sup
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>a : List (ι →₀ M)<VAR>hs : Pairwise (_root_.Disjoint on Finsupp.support) (Quot.mk Setoid.r a)<GOAL>(sum (Quot.mk Setoid.r a)).support = (map Finsupp.support (Quot.mk Setoid.r a)).sup
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>a l : List (ι →₀ M)<VAR>hl : Quot.mk Setoid.r a = ↑l<VAR>hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l<GOAL>List.Pairwise (_root_.Disjoint on Finsupp.support) a
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>a l : List (ι →₀ M)<VAR>hd : List.Pairwise (_root_.Disjoint on Finsupp.support) l<VAR>hl : a.Perm l<GOAL>List.Pairwise (_root_.Disjoint on Finsupp.support) a
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>(⋂₀ F).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<GOAL>∀ (G : Finset (Set E)), ↑G ⊆ F → G.card ≤ finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<GOAL>(⋂₀ ↑I).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Set (Set E)<VAR>left✝ : ↑I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.encard = ↑(finrank 𝕜 E) + 1<GOAL>(⋂₀ ↑I).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Set (Set E)<VAR>left✝ : ↑I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.encard = ↑(finrank 𝕜 E) + 1<GOAL>(⋂₀ J).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Set (Set E)<VAR>left✝ : ↑I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.encard = ↑(finrank 𝕜 E) + 1<VAR>hJ_fin : Fintype ↑J<GOAL>(⋂₀ J).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Set (Set E)<VAR>left✝ : ↑I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.encard = ↑(finrank 𝕜 E) + 1<VAR>hJ_fin : Fintype ↑J<VAR>J' : Finset (Set E) := J.toFinset<GOAL>(⋂₀ J).Nonempty
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : FiniteDimensional 𝕜 E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : T2Space E<VAR>F : Set (Set E)<VAR>h_card : ↑(finrank 𝕜 E) + 1 ≤ F.encard<VAR>h_convex : ∀ X ∈ F, Convex 𝕜 X<VAR>h_compact : ∀ X ∈ F, IsCompact X<VAR>h_inter : ∀ (G : Finset (Set E)), ↑G ⊆ F → G.card = finrank 𝕜 E + 1 → (⋂₀ ↑G).Nonempty<VAR>I : Finset (Set E)<VAR>hI_ss : ↑I ⊆ F<VAR>hI_card : I.card ≤ finrank 𝕜 E + 1<VAR>J : Set (Set E)<VAR>left✝ : ↑I ⊆ J<VAR>hJ_ss : J ⊆ F<VAR>hJ_card : J.encard = ↑(finrank 𝕜 E) + 1<VAR>hJ_fin : Fintype ↑J<VAR>J' : Finset (Set E) := J.toFinset<GOAL>(⋂₀ ↑J.toFinset).Nonempty
<VAR>R : Type u<VAR>inst✝³ : CommSemiring R<VAR>S : Type u_1<VAR>inst✝² : CommSemiring S<VAR>f : R →* S<VAR>g : R →+* S<VAR>p m n : ℕ<VAR>inst✝¹ : ExpChar R p<VAR>inst✝ : ExpChar S p<VAR>x y : R<GOAL>(iterateFrobenius R p (m + n)) x = (iterateFrobenius R p m) ((iterateFrobenius R p n) x)
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝² : AddCommMonoid α<VAR>inst✝¹ : CommSemigroup α<VAR>inst✝ : Fintype n<VAR>M : Matrix m n α<VAR>N : Matrix n l α<VAR>i✝ : l<VAR>j✝ : m<GOAL>(M * N)ᵀ i✝ j✝ = (Nᵀ * Mᵀ) i✝ j✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>inst✝¹ : Preorder α<VAR>inst✝ : ConditionallyCompleteLattice β<VAR>f : α → β<VAR>h_mono : Monotone f<VAR>s : Set α<VAR>c : α<VAR>hcs : c ∈ s<VAR>h_bdd : BddBelow s<VAR>f' : αᵒᵈ → βᵒᵈ := f<GOAL>sInf (f '' s) ≤ f c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t u : Set α<VAR>f : α → β<VAR>p q : Prop<GOAL>q ∈ {p}ᶜ ↔ q ∈ {¬p}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁ s₂ t t₁ t₂ u v : Finset α<VAR>a b : α<GOAL>s = t ∪ s ↔ t ⊆ s
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι'✝ : Type u_9<VAR>inst✝⁷ : NormedField 𝕜<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜 E<VAR>inst✝⁴ : NormedField 𝕜₂<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>ι' : Type u_10<VAR>inst✝ : Nonempty ι'<VAR>p : ι → Seminorm 𝕜 E<VAR>q : Seminorm 𝕜₂ F<VAR>f : E →ₛₗ[σ₁₂] F<GOAL>IsBounded p (fun x => q) f ↔ ∃ s C, q.comp f ≤ C • s.sup p
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>OpenEmbedding ((forget TopCat).map f ≫ (forget TopCat).map g) ↔ OpenEmbedding ⇑g
<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso f<GOAL>OpenEmbedding ((forget TopCat).map (f ≫ g)) ↔ OpenEmbedding ⇑g
<VAR>cf cg : Code<GOAL>encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)
<VAR>cf cg : Code<VAR>this : encode (cf.pair cg) < encode (cf.prec cg)<GOAL>encode cf < encode (cf.prec cg) ∧ encode cg < encode (cf.prec cg)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>P Q : Karoubi C<VAR>f g : P ⟶ Q<VAR>h : f.f = g.f<GOAL>f = g
<VAR>n : ℕ<VAR>h₁ : 1 < n<VAR>h₂ : ¬Prime n<GOAL>n ∣ 1 ^ (n - 1) - 1
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>X Y : C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{w, u₂} D<VAR>F : C ⥤ D<VAR>A A' B B' : C<VAR>inst✝⁴ : HasBinaryCoproduct A B<VAR>inst✝³ : HasBinaryCoproduct A' B'<VAR>inst✝² : HasBinaryCoproduct (F.obj A) (F.obj B)<VAR>inst✝¹ : HasBinaryCoproduct (F.obj A') (F.obj B')<VAR>inst✝ : IsIso (coprodComparison F A B)<GOAL>F.map coprod.inl ≫ inv (coprodComparison F A B) = coprod.inl
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>M.det = (-1 • eval ((scalar n) 0) (X - C M)).det
<VAR>ι : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>Z : Type u_5<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : TopologicalSpace F<VAR>proj : Z → B<VAR>e✝ : Pretrivialization F proj<VAR>x : Z<VAR>e' : Pretrivialization F TotalSpace.proj<VAR>x' : TotalSpace F E<VAR>b : B<VAR>y : E b<VAR>inst✝ : (x : B) → Zero (E x)<VAR>e : Pretrivialization F TotalSpace.proj<VAR>z : TotalSpace F E<VAR>hz : z.proj ∈ e.baseSet<GOAL>e.symm z.proj (↑e z).2 = z.snd
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<VAR>hs : s = {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<GOAL>∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<VAR>hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}<GOAL>∀ᵐ (x : α) ∂μ, ∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<VAR>hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}<VAR>f : α → Set (Set α) := fun x => {a | μ a = 0}<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<VAR>hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}<VAR>f : α → Set (Set α) := fun x => {a | μ a = 0}<VAR>h : v.FineSubfamilyOn f s<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>inst✝² : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : SecondCountableTopology α<VAR>s : Set α := {x | ¬∀ᶠ (a : Set α) in v.filterAt x, 0 < μ a}<VAR>hs : s = {x | ∃ᶠ (x : Set α) in v.filterAt x, μ x = 0}<VAR>f : α → Set (Set α) := fun x => {a | μ a = 0}<VAR>h : v.FineSubfamilyOn f s<GOAL>μ s ≤ 0
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>N : LieSubmodule R L M<GOAL>↑⁅⊤, N⁆ = Submodule.map ((toEnd R L M) x) ↑N ⊔ ↑⁅I, N⁆
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>N : LieSubmodule R L M<GOAL>Submodule.span R {m | ∃ x, ∃ n ∈ N, ⁅x, n⁆ = m} = Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m})
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>N : LieSubmodule R L M<GOAL>{m | ∃ x, ∃ n ∈ N, ⁅x, n⁆ = m} ⊆ ↑(Submodule.span R ((fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m}))
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieRing L₂<VAR>inst✝⁴ : LieAlgebra R L₂<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>I : LieIdeal R L<VAR>x : L<VAR>hxI : Submodule.span R {x} ⊔ (lieIdealSubalgebra R L I).toSubmodule = ⊤<VAR>N : LieSubmodule R L M<VAR>z : M<VAR>hz : z ∈ (fun a => ⁅x, a⁆) '' ↑↑N ∪ {m | ∃ x ∈ I, ∃ n ∈ N, ⁅x, n⁆ = m}<GOAL>z ∈ {m | ∃ x, ∃ n ∈ N, ⁅x, n⁆ = m}
<VAR>a b : ℕ<VAR>d : ℕ := a.gcd b<GOAL>φ a * φ b ≤ φ (a * b)
<VAR>b : ℕ<VAR>d : ℕ := gcd 0 b<GOAL>φ 0 * φ b ≤ φ (0 * b)
<VAR>a b : ℕ<VAR>d : ℕ := a.gcd b<VAR>ha0 : 0 < a<GOAL>φ a * φ b ≤ φ (a * b)
<VAR>a b : ℕ<VAR>d : ℕ := a.gcd b<VAR>ha0 : 0 < a<VAR>hd0 : 0 < d<GOAL>φ a * φ b ≤ φ (a * b)
<VAR>a b : ℕ<VAR>d : ℕ := a.gcd b<VAR>ha0 : 0 < a<VAR>hd0 : 0 < d<GOAL>φ a * φ b * d ≤ φ (a * b) * d
<VAR>a b : ℕ<VAR>d : ℕ := a.gcd b<VAR>ha0 : 0 < a<VAR>hd0 : 0 < d<GOAL>φ (a * b) * φ (a.gcd b) ≤ φ (a * b) * d
<VAR>α : Type u_1<VAR>l : List α<GOAL>l.tail = l.tail?.getD []
<VAR>x y : ℝ<GOAL>(x * y).negMulLog = y * x.negMulLog + x * y.negMulLog
<VAR>x y : ℝ<GOAL>-(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
<VAR>x y : ℝ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>-(x * y * log (x * y)) = y * -(x * log x) + x * -(y * log y)
<VAR>x y : ℝ<VAR>hx : ¬x = 0<VAR>hy : ¬y = 0<GOAL>-(x * y * (log x + log y)) = y * -(x * log x) + x * -(y * log y)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>S : Type u_10<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M'<VAR>inst✝¹ : SMulCommClass R S M'<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>f : ι → M'<VAR>x : M<GOAL>((b.constr S) f) x = ∑ i : ι, b.equivFun x i • f i
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>ψ : AddChar B M<VAR>hψ : Injective ⇑ψ<VAR>f g : A →+ B<VAR>h : (fun f => ψ.compAddMonoidHom f) f = (fun f => ψ.compAddMonoidHom f) g<GOAL>f = g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : AddMonoid B<VAR>inst✝¹ : Monoid M<VAR>inst✝ : Monoid N<VAR>ψ✝ : AddChar A M<VAR>ψ : AddChar B M<VAR>hψ : Injective ⇑ψ<VAR>f g : A →+ B<VAR>h : ⇑((fun f => ψ.compAddMonoidHom f) f) = ⇑((fun f => ψ.compAddMonoidHom f) g)<GOAL>⇑f = ⇑g
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>s : Multiset R<VAR>hs : (Multiset.map (fun a => X - C a) s).prod.Separable<GOAL>s.Nodup
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>s : Multiset R<VAR>hs : (Multiset.map (fun a => X - C a) s).prod.Separable<GOAL>∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>a : R<VAR>t : Multiset R<VAR>hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable<GOAL>False
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Nontrivial R<VAR>a : R<VAR>t : Multiset R<VAR>hs : (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod.Separable<GOAL>(X - C a) * (X - C a) ∣ (Multiset.map (fun a => X - C a) (a ::ₘ a ::ₘ t)).prod
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : DifferentiableOn 𝕜 (fun y => -f y) s<GOAL>DifferentiableOn 𝕜 f s
<VAR>R✝ : Type u_1<VAR>R' : Type u_2<VAR>A✝ : Type u_3<VAR>T : Type u_4<VAR>B✝ : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝¹² : Semiring R✝<VAR>inst✝¹¹ : Ring R'<VAR>inst✝¹⁰ : AddZeroClass A✝<VAR>inst✝⁹ : SemilatticeSup B✝<VAR>inst✝⁸ : Add B✝<VAR>inst✝⁷ : OrderBot B✝<VAR>D✝ : A✝ → B✝<VAR>p q : R✝[A✝]<VAR>hadd✝ : ∀ (a1 a2 : A✝), D✝ (a1 + a2) = D✝ a1 + D✝ a2<VAR>R : Type u_7<VAR>A : Type u_8<VAR>B : Type u_9<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : SemilatticeSup B<VAR>inst✝² : OrderBot B<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>D : A → B<VAR>hzero : D 0 = 0<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>f : ι → R[A]<GOAL>supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i)
<VAR>R✝ : Type u_1<VAR>R' : Type u_2<VAR>A✝ : Type u_3<VAR>T : Type u_4<VAR>B✝ : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝¹² : Semiring R✝<VAR>inst✝¹¹ : Ring R'<VAR>inst✝¹⁰ : AddZeroClass A✝<VAR>inst✝⁹ : SemilatticeSup B✝<VAR>inst✝⁸ : Add B✝<VAR>inst✝⁷ : OrderBot B✝<VAR>D✝ : A✝ → B✝<VAR>p q : R✝[A✝]<VAR>hadd✝ : ∀ (a1 a2 : A✝), D✝ (a1 + a2) = D✝ a1 + D✝ a2<VAR>R : Type u_7<VAR>A : Type u_8<VAR>B : Type u_9<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : SemilatticeSup B<VAR>inst✝² : OrderBot B<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>D : A → B<VAR>hzero : D 0 = 0<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>f : ι → R[A]<GOAL>supDegree D (∏ i ∈ ∅, f i) ≤ ∑ i ∈ ∅, supDegree D (f i)
<VAR>R✝ : Type u_1<VAR>R' : Type u_2<VAR>A✝ : Type u_3<VAR>T : Type u_4<VAR>B✝ : Type u_5<VAR>ι✝ : Type u_6<VAR>inst✝¹² : Semiring R✝<VAR>inst✝¹¹ : Ring R'<VAR>inst✝¹⁰ : AddZeroClass A✝<VAR>inst✝⁹ : SemilatticeSup B✝<VAR>inst✝⁸ : Add B✝<VAR>inst✝⁷ : OrderBot B✝<VAR>D✝ : A✝ → B✝<VAR>p q : R✝[A✝]<VAR>hadd✝ : ∀ (a1 a2 : A✝), D✝ (a1 + a2) = D✝ a1 + D✝ a2<VAR>R : Type u_7<VAR>A : Type u_8<VAR>B : Type u_9<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : AddCommMonoid A<VAR>inst✝⁴ : AddCommMonoid B<VAR>inst✝³ : SemilatticeSup B<VAR>inst✝² : OrderBot B<VAR>inst✝¹ : CovariantClass B B (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass B B (Function.swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>D : A → B<VAR>hzero : D 0 = 0<VAR>hadd : ∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2<VAR>ι : Type u_10<VAR>s : Finset ι<VAR>f : ι → R[A]<GOAL>∀ ⦃a : ι⦄ {s : Finset ι}, a ∉ s → supDegree D (∏ i ∈ s, f i) ≤ ∑ i ∈ s, supDegree D (f i) → supDegree D (∏ i ∈ insert a s, f i) ≤ ∑ i ∈ insert a s, supDegree D (f i)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommSemiring R<VAR>f : α → R<VAR>s : Finset α<VAR>inst✝ : CommSemiring R<VAR>x : α → R<VAR>n : ℕ<GOAL>s.sum x ^ n = ∑ k ∈ s.sym n, ↑(↑k).multinomial * (Multiset.map x ↑k).prod
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommSemiring R<VAR>f : α → R<VAR>s : Finset α<VAR>inst✝ : CommSemiring R<VAR>x : α → R<VAR>n : ℕ<GOAL>s.sum x ^ n = ∑ i : { x // x ∈ s.sym n }, ↑(↑↑i).multinomial * (Multiset.map x ↑↑i).prod
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommSemiring R<VAR>f : α → R<VAR>s : Finset α<VAR>inst✝ : CommSemiring R<VAR>x : α → R<VAR>n : ℕ<VAR>x✝ : { x // x ∈ s.sym n }<VAR>a✝ : x✝ ∈ univ<GOAL>(Multiset.map x ↑↑x✝).prod = (Multiset.map x ↑↑x✝).noncommProd ⋯