ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>f p ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>hf : ∀ (r : R), f (star r) = star (f r)<GOAL>f p ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hf : ∀ (r : R), f (star r) = star (f r)<VAR>x✝ : R<VAR>h✝ : x✝ ∈ range fun s => star s * s<GOAL>f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hf : ∀ (r : R), f (star r) = star (f r)<GOAL>f 0 ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>R✝ : Type u<VAR>F : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁷ : NonUnitalSemiring R<VAR>inst✝⁶ : PartialOrder R<VAR>inst✝⁵ : StarRing R<VAR>inst✝⁴ : StarOrderedRing R<VAR>inst✝³ : NonUnitalSemiring S<VAR>inst✝² : PartialOrder S<VAR>inst✝¹ : StarRing S<VAR>inst✝ : StarOrderedRing S<VAR>f : R →⋆ₙ+* S<VAR>x p : R<VAR>hf : ∀ (r : R), f (star r) = star (f r)<VAR>x✝ : R<VAR>hx✝ : x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>y✝ : R<VAR>hy✝ : y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>a✝¹ : f x✝ ∈ AddSubmonoid.closure (range fun s => star s * s)<VAR>a✝ : f y✝ ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>f (x✝ + y✝) ∈ AddSubmonoid.closure (range fun s => star s * s)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N✝ : Type u_5<VAR>inst✝² : AddCommGroup N✝<VAR>inst✝¹ : Module R N✝<VAR>inst✝ : IsSemisimpleModule R M<VAR>N : Submodule R M<GOAL>sSup {m | IsSimpleModule R ↥m ∧ m ≤ N} = N
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>W.Φ (-n) = W.Φ n
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((NatTrans.leftDerivedToHomotopyCategory α).app X) = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv = (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ HomologicalComplex.homologyMap ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) n ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} D<VAR>inst✝⁴ : Abelian C<VAR>inst✝³ : HasProjectiveResolutions C<VAR>inst✝² : Abelian D<VAR>F G : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : G.Additive<VAR>α : F ⟶ G<VAR>X : C<VAR>P : ProjectiveResolution X<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv = (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.quotient D (ComplexShape.down ℕ) ⋙ HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).inv.app ((G.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj G).inv
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r f : R[X]<VAR>I : Ideal R[X]<VAR>cf : ∀ (i : ℕ), C (f.coeff i) ∈ I<GOAL>Ideal.span {g | ∃ i, g = C (f.coeff i)} ≤ I
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type x<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r f : R[X]<VAR>I : Ideal R[X]<VAR>cf : ∀ (i : ℕ), C (f.coeff i) ∈ I<GOAL>Ideal.span {g | ∃ i, C (f.coeff i) = g} ≤ I
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>(G.nonuniformWitnesses ε s t).2 ⊆ t
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝¹ : LinearOrderedField 𝕜<VAR>G : SimpleGraph α<VAR>inst✝ : DecidableRel G.Adj<VAR>ε : 𝕜<VAR>s t : Finset α<VAR>a b : α<VAR>h : ¬G.IsUniform ε s t<GOAL>(⋯.choose, ⋯.choose).2 ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : ℕ<GOAL>multiplicity ↑a ↑b = multiplicity a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : ℕ<GOAL>(multiplicity ↑a ↑b).Dom ↔ (multiplicity a b).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Monoid α<VAR>inst✝ : Monoid β<VAR>a b : ℕ<GOAL>∀ (h₁ : (multiplicity ↑a ↑b).Dom) (h₂ : (multiplicity a b).Dom), (multiplicity ↑a ↑b).get h₁ = (multiplicity a b).get h₂
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ P.f₀ = 0<VAR>hs' : s ≠ ↑P.k ∨ P.g₀ = 0<GOAL>DifferentiableAt ℂ P.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ P.f₀ = 0<VAR>hs' : s ≠ ↑P.k ∨ P.g₀ = 0<GOAL>DifferentiableAt ℂ (fun y => (1 / y) • P.f₀) s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : WeakFEPair E<VAR>s : ℂ<VAR>hs : s ≠ 0 ∨ P.f₀ = 0<VAR>hs' : s ≠ ↑P.k ∨ P.g₀ = 0<GOAL>DifferentiableAt ℂ (fun y => (P.ε / (↑P.k - y)) • P.g₀) s
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<GOAL>IsMeagre ∅
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>ι' : Sort u_4<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<GOAL>univ ∈ residual X
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>a : R[X]<GOAL>a.wronskian a = 0
<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>x : R<VAR>B : Type u_2<VAR>inst✝² : CommRing B<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsLocalization.Away x B<VAR>d : ℤ<GOAL>selfZPow x B (-d) * selfZPow x B d = 1
<VAR>K : Type u_1<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : LieRingModule L M<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : Module K M<VAR>inst✝³ : LieModule K L M<VAR>inst✝² : LieAlgebra.IsNilpotent K L<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<GOAL>⨆ χ, weightSpace M χ = ⊤
<VAR>K : Type u_1<VAR>L : Type u_3<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : LieAlgebra K L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent K L<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (M : Type u_4) [inst : AddCommGroup M] [inst_1 : LieRingModule L M] [inst_2 : Module K M] [inst_3 : LieModule K L M] [inst_4 : FiniteDimensional K M] [inst_5 : IsTriangularizable K L M], finrank K M = m → ⨆ χ, weightSpace M χ = ⊤<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : Module K M<VAR>inst✝² : LieModule K L M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<VAR>h_dim : finrank K M = n<GOAL>⨆ χ, weightSpace M χ = ⊤
<VAR>K : Type u_1<VAR>L : Type u_3<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : LieAlgebra K L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent K L<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (M : Type u_4) [inst : AddCommGroup M] [inst_1 : LieRingModule L M] [inst_2 : Module K M] [inst_3 : LieModule K L M] [inst_4 : FiniteDimensional K M] [inst_5 : IsTriangularizable K L M], finrank K M = m → ⨆ χ, weightSpace M χ = ⊤<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : Module K M<VAR>inst✝² : LieModule K L M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<VAR>h_dim : finrank K M = n<VAR>h' : ∀ (a : L), ∃ φ, weightSpaceOf M φ a = ⊤<GOAL>⨆ χ, weightSpace M χ = ⊤
<VAR>K : Type u_1<VAR>L : Type u_3<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : LieAlgebra K L<VAR>inst✝⁶ : LieAlgebra.IsNilpotent K L<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ (M : Type u_4) [inst : AddCommGroup M] [inst_1 : LieRingModule L M] [inst_2 : Module K M] [inst_3 : LieModule K L M] [inst_4 : FiniteDimensional K M] [inst_5 : IsTriangularizable K L M], finrank K M = m → ⨆ χ, weightSpace M χ = ⊤<VAR>M : Type u_4<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : LieRingModule L M<VAR>inst✝³ : Module K M<VAR>inst✝² : LieModule K L M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : IsTriangularizable K L M<VAR>h_dim : finrank K M = n<VAR>y : L<VAR>hy : ¬∃ φ, weightSpaceOf M φ y = ⊤<GOAL>⨆ χ, weightSpace M χ = ⊤
<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✝² : TopologicalSpace E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousConstSMul 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x y : E<VAR>hx : x ∈ interior s<VAR>hy : y ∈ closure s<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>a • x + b • y ∈ interior s
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝ : Frame α<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<VAR>s : Set ι<VAR>t : Set ι'<GOAL>(⨆ i ∈ s, f i) ⊓ ⨆ j ∈ t, g j = ⨆ p ∈ s ×ˢ t, f p.1 ⊓ g p.2
<VAR>α : Type u<VAR>β : Type v<VAR>ι✝ : Sort w<VAR>κ : ι✝ → Sort w'<VAR>inst✝ : Frame α<VAR>s✝ t✝ : Set α<VAR>a b : α<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>f : ι → α<VAR>g : ι' → α<VAR>s : Set ι<VAR>t : Set ι'<GOAL>⨆ i, f ↑i.1 ⊓ g ↑i.2 = ⨆ x, f (↑x).1 ⊓ g (↑x).2
<VAR>α : Type u_1<VAR>inst✝² : LinearOrder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : OrderClosedTopology α<VAR>a b c d : α<GOAL>Ioi a ∈ 𝓝ˢ (Ici b) ↔ a < b
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<VAR>a : Γ<GOAL>map f (cons a l) = cons (f.f a) (map f l)
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>inst✝¹ : Inhabited Γ<VAR>inst✝ : Inhabited Γ'<VAR>f : PointedMap Γ Γ'<VAR>l : ListBlank Γ<VAR>a : Γ<GOAL>cons (map f (cons a l)).head (map f (cons a l)).tail = cons (f.f a) (map f l)
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x y z : ℝ<VAR>hy : 0 < y<VAR>hxy : y < x<VAR>hz : z < 0<VAR>hx : 0 < x<GOAL>x ^ z < y ^ z
<VAR>x✝ y✝ z✝ : ℝ<VAR>n : ℕ<VAR>x y z : ℝ<VAR>hy : 0 < y<VAR>hxy : y < x<VAR>hz : z < 0<VAR>hx : 0 < x<GOAL>y ^ (-z) < x ^ (-z)
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Semigroup M<VAR>a✝ b z : M<VAR>a : z ∈ center M<VAR>g : M<GOAL>g * z = z * g
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁵ : NonUnitalNonAssocRing R<VAR>inst✝⁴ : NonUnitalNonAssocRing S✝<VAR>inst✝³ : NonUnitalNonAssocRing T<VAR>inst✝² : FunLike F R S✝<VAR>inst✝¹ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>ι : Sort u_2<VAR>inst✝ : Nonempty ι<VAR>S : ι → NonUnitalSubring R<VAR>hS : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)
<VAR>α : Type u<VAR>l✝ l' l : List α<GOAL>l.cyclicPermutations.head? = some l
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>LinearMap.ker (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) = kerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>LinearMap.ker (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S)) ≤ kerTotal R S
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>M : Type u_1<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<GOAL>kerTotal R S ≤ LinearMap.ker (Finsupp.total S (Ω[S⁄R]) S ⇑(D R S))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<GOAL>(insert a s).val = (a ::ₘ s.val).dedup
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s✝ t u v : Finset α<VAR>a✝ b a : α<VAR>s : Finset α<GOAL>(insert a s).val = ndinsert a s.val
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>nth p (count p n) = sInf {i | p i ∧ n ≤ i}
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n : ℕ<GOAL>{x | p x ∧ ∀ k < count p n, nth p k < x} = {i | p i ∧ n ≤ i}
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n a : ℕ<VAR>hpa : p a<GOAL>(∀ k < count p n, nth p k < a) ↔ n ≤ a
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n a : ℕ<VAR>hpa : p a<VAR>h : ∀ k < count p n, nth p k < a<VAR>ha : a < n<GOAL>False
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>n a : ℕ<VAR>hpa : p a<VAR>h : ∀ k < count p n, nth p k < a<VAR>ha : a < n<VAR>hn : nth p (count p a) < a<GOAL>False
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<GOAL>(trace R M) 1 = ↑(finrank R M)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>h✝ : Subsingleton R<GOAL>(trace R M) 1 = ↑(finrank R M)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>h✝ : Nontrivial R<GOAL>(trace R M) 1 = ↑(finrank R M)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M<GOAL>(trace R M) 1 = ↑(finrank R M)
<VAR>R : Type u_1<VAR>inst✝¹² : CommRing R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommGroup M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁹ : AddCommGroup N<VAR>inst✝⁸ : Module R N<VAR>inst✝⁷ : AddCommGroup P<VAR>inst✝⁶ : Module R P<VAR>ι : Type u_5<VAR>inst✝⁵ : Module.Free R M<VAR>inst✝⁴ : Module.Finite R M<VAR>inst✝³ : Module.Free R N<VAR>inst✝² : Module.Finite R N<VAR>inst✝¹ : Module.Free R P<VAR>inst✝ : Module.Finite R P<VAR>h✝ : Nontrivial R<VAR>b : Basis (Module.Free.ChooseBasisIndex R M) R M<GOAL>Matrix.trace 1 = ↑(Fintype.card (Module.Free.ChooseBasisIndex R M))
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<GOAL>∃ k > 0, Nat.card ↥(center G) = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<VAR>this : Finite G<GOAL>∃ k > 0, Nat.card ↥(center G) = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<VAR>this : Finite G<VAR>hcG : IsPGroup p ↥(center G)<GOAL>∃ k > 0, Nat.card ↥(center G) = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<VAR>this : Finite G<VAR>hcG : IsPGroup p ↥(center G)<VAR>x✝ : ∃ n, Nat.card ↥(center G) = p ^ n<GOAL>∃ k > 0, Nat.card ↥(center G) = p ^ k
<VAR>p : ℕ<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : Fact (Nat.Prime p)<VAR>n : ℕ<VAR>hGpn : Nat.card G = p ^ n<VAR>hn : 0 < n<VAR>this✝ : Finite G<VAR>hcG : IsPGroup p ↥(center G)<VAR>x✝ : ∃ n, Nat.card ↥(center G) = p ^ n<VAR>this : Nontrivial G<GOAL>∃ k > 0, Nat.card ↥(center G) = p ^ k
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>s : Multiset α<VAR>a : α<VAR>h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>h' : {x | x ∈ s}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>b : β<GOAL>noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f : α → β → β<VAR>op : α → α → α<VAR>a : α<VAR>b : β<VAR>a✝ : List α<VAR>h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<VAR>h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y => ∀ (b : β), f x (f y b) = f y (f x b)<GOAL>noncommFoldr f (a ::ₘ ⟦a✝⟧) h b = f a (noncommFoldr f ⟦a✝⟧ h' b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>i : Fin k<GOAL>↑i < (sort (fun x x_1 => x ≤ x_1) s).length
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>s : Finset α<VAR>k : ℕ<VAR>h : s.card = k<VAR>i : Fin k<GOAL>↑i < k
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x y : E<VAR>a b : 𝕜<VAR>S : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>hS : ∀ s ∈ S, StrictConvex 𝕜 s<GOAL>StrictConvex 𝕜 (⋃₀ S)
<VAR>𝕜 : Type u_1<VAR>𝕝 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>β : Type u_5<VAR>inst✝⁶ : OrderedSemiring 𝕜<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalSpace F<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : SMul 𝕜 E<VAR>inst✝ : SMul 𝕜 F<VAR>s : Set E<VAR>x y : E<VAR>a b : 𝕜<VAR>S : Set (Set E)<VAR>hdir : DirectedOn (fun x x_1 => x ⊆ x_1) S<VAR>hS : ∀ s ∈ S, StrictConvex 𝕜 s<GOAL>StrictConvex 𝕜 (⋃ i, ↑i)
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>‖↑p‖ = (↑p)⁻¹
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>‖↑p‖ = (↑↑p)⁻¹
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<GOAL>‖↑↑p‖ = (↑↑p)⁻¹
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : R<VAR>x y : L<VAR>m : M<VAR>hy : y ∈ 𝕎(L, χ₁, x)<VAR>hm : m ∈ 𝕎(M, χ₂, x)<GOAL>⁅y, m⁆ ∈ 𝕎(M, χ₁ + χ₂, x)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : R<VAR>x y : L<VAR>m : M<VAR>hy : y ∈ 𝕎(L, χ₁, x)<VAR>hm : m ∈ 𝕎(M, χ₂, x)<GOAL>⁅y, m⁆ ∈ LinearMap.range (↑(toModuleHom R L M) ∘ₗ TensorProduct.mapIncl 𝕎(L, χ₁, x) 𝕎(M, χ₂, x))
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : R<VAR>x y : L<VAR>m : M<VAR>hy : y ∈ 𝕎(L, χ₁, x)<VAR>hm : m ∈ 𝕎(M, χ₂, x)<GOAL>∃ y_1, (toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) y_1) = ⁅y, m⁆
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : LieAlgebra.IsNilpotent R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>χ₁ χ₂ : R<VAR>x y : L<VAR>m : M<VAR>hy : y ∈ 𝕎(L, χ₁, x)<VAR>hm : m ∈ 𝕎(M, χ₂, x)<GOAL>(toModuleHom R L M) ((TensorProduct.map 𝕎(L, χ₁, x).subtype 𝕎(M, χ₂, x).subtype) (⟨y, hy⟩ ⊗ₜ[R] ⟨m, hm⟩)) = ⁅y, m⁆