ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<GOAL>{0}ᶜ ⊆ resolventSet 𝕜 0
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<VAR>hk : k ∈ {0}ᶜ<GOAL>k ∈ resolventSet 𝕜 0
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<VAR>hk : k ≠ 0<GOAL>k ∈ resolventSet 𝕜 0
<VAR>𝕜 : Type u<VAR>A : Type v<VAR>inst✝³ : Field 𝕜<VAR>inst✝² : Ring A<VAR>inst✝¹ : Algebra 𝕜 A<VAR>inst✝ : Nontrivial A<VAR>k : 𝕜<VAR>hk : k ≠ 0<VAR>this : IsUnit (Units.mk0 k hk • 1)<GOAL>k ∈ resolventSet 𝕜 0
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Rₗ : Type u_10<VAR>Mₗ : Type u_11<VAR>Nₗ : Type u_12<VAR>Pₗ : Type u_13<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : Semiring S<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : CommSemiring Rₗ<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Mₗ<VAR>inst✝⁹ : AddCommMonoid Nₗ<VAR>inst✝⁸ : AddCommMonoid Pₗ<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : Module R₂ P<VAR>inst✝⁴ : Module S₂ P<VAR>inst✝³ : Module Rₗ Mₗ<VAR>inst✝² : Module Rₗ Nₗ<VAR>inst✝¹ : Module Rₗ Pₗ<VAR>inst✝ : SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>b₁' : Basis ι₁ Rₗ Mₗ<VAR>b₂' : Basis ι₂ Rₗ Nₗ<VAR>B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ<VAR>x : Mₗ<VAR>y : Nₗ<GOAL>((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y
<VAR>ι₁ : Type u_1<VAR>ι₂ : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>S : Type u_5<VAR>S₂ : Type u_6<VAR>M : Type u_7<VAR>N : Type u_8<VAR>P : Type u_9<VAR>Rₗ : Type u_10<VAR>Mₗ : Type u_11<VAR>Nₗ : Type u_12<VAR>Pₗ : Type u_13<VAR>inst✝¹⁸ : Semiring R<VAR>inst✝¹⁷ : Semiring S<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring S₂<VAR>inst✝¹⁴ : CommSemiring Rₗ<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Mₗ<VAR>inst✝⁹ : AddCommMonoid Nₗ<VAR>inst✝⁸ : AddCommMonoid Pₗ<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module S N<VAR>inst✝⁵ : Module R₂ P<VAR>inst✝⁴ : Module S₂ P<VAR>inst✝³ : Module Rₗ Mₗ<VAR>inst✝² : Module Rₗ Nₗ<VAR>inst✝¹ : Module Rₗ Pₗ<VAR>inst✝ : SMulCommClass S₂ R₂ P<VAR>ρ₁₂ : R →+* R₂<VAR>σ₁₂ : S →+* S₂<VAR>b₁ : Basis ι₁ R M<VAR>b₂ : Basis ι₂ S N<VAR>b₁' : Basis ι₁ Rₗ Mₗ<VAR>b₂' : Basis ι₂ Rₗ Nₗ<VAR>B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ<VAR>x : Mₗ<VAR>y : Nₗ<GOAL>((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B ((Finsupp.total ι₁ Mₗ Rₗ ⇑b₁') (b₁'.repr x))) ((Finsupp.total ι₂ Nₗ Rₗ ⇑b₂') (b₂'.repr y))
<VAR>R : Type u_1<VAR>inst✝⁵ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>t : M ⊗[R] (ι →₀ N)<VAR>i : ι<GOAL>((finsuppRight R M N ι) t) i = (lTensor M (Finsupp.lapply i)) t
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(((associatedHom S) Q) x) x = Q x
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : AddCommGroup N<VAR>inst✝⁵ : Module R N<VAR>inst✝⁴ : CommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S N<VAR>inst✝¹ : IsScalarTower S R N<VAR>inst✝ : Invertible 2<VAR>B₁ : BilinMap R M R<VAR>Q : QuadraticMap R M N<VAR>x : M<GOAL>(⅟2 • 2) • Q x = Q x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>κ : Kernel α β<VAR>μ : Measure α<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((const α (μ.bind ⇑κ)) a) s = ((κ ∘ₖ const α μ) a) s
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<GOAL>lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<VAR>i' : R' → R<VAR>hi' : Function.RightInverse i' ⇑i<GOAL>lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R' M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<VAR>i' : R' → R<VAR>hi' : Function.RightInverse i' ⇑i<VAR>x✝ : R'<VAR>h : i' x✝ = 0<GOAL>x✝ = 0
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>i : ZeroHom R R'<VAR>j : M →+ M'<VAR>hi : Surjective ⇑i<VAR>hj : Injective ⇑j<VAR>hc : ∀ (r : R) (m : M), j (r • m) = i r • j m<VAR>i' : R' → R<VAR>hi' : Function.RightInverse i' ⇑i<VAR>r : R'<VAR>m : M<GOAL>j (i' r • m) = r • j m
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ≥0<GOAL>HasFiniteIntegral (fun x => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤
<VAR>A✝ : Type u_1<VAR>inst✝¹⁰ : NormedRing A✝<VAR>inst✝⁹ : StarRing A✝<VAR>inst✝⁸ : CstarRing A✝<VAR>inst✝⁷ : CompleteSpace A✝<VAR>inst✝⁶ : NormedAlgebra ℂ A✝<VAR>inst✝⁵ : StarModule ℂ A✝<VAR>A : Type u_2<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Ring A<VAR>inst✝² : StarRing A<VAR>inst✝¹ : Algebra ℂ A<VAR>inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal<VAR>a : A<VAR>x : ℝ<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<GOAL>↑x ∈ σ ℂ a ↔ x ∈ σ ℝ a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>this : ProperSpace ↥(span 𝕜 v)<GOAL>(∀ u ⊇ v, Orthonormal 𝕜 Subtype.val → u = v) ↔ ∃ b, ⇑b = Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>this : ProperSpace ↥(span 𝕜 v)<GOAL>(span 𝕜 v)ᗮ = ⊥ ↔ ∃ b, ⇑b = Subtype.val
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>v : Set E<VAR>inst✝ : FiniteDimensional 𝕜 E<VAR>hv : Orthonormal 𝕜 Subtype.val<VAR>this : ProperSpace ↥(span 𝕜 v)<GOAL>span 𝕜 v = ⊤ ↔ ∃ b, ⇑b = Subtype.val
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>i : F.obj 0 ≅ 0<VAR>X Y : C<GOAL>F.map 0 = F.map 0 ≫ F.map 0
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>i : F.obj 0 ≅ 0<VAR>X Y : C<GOAL>F.map 0 ≫ F.map 0 = F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0
<VAR>C : Type u₁<VAR>inst✝⁶ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} E<VAR>inst✝³ : HasZeroObject C<VAR>inst✝² : HasZeroObject D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>F : C ⥤ D<VAR>i : F.obj 0 ≅ 0<VAR>X Y : C<GOAL>F.map 0 ≫ (i.hom ≫ i.inv) ≫ F.map 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MonoidWithZero α<VAR>a : α<VAR>u : αˣ<GOAL>a = 0 ↔ a * ↑u = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝⁵ : Countable ι<VAR>μ : Measure X<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<GOAL>IntegrableOn (⇑f) (⋃ i, ↑(s i)) μ
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝⁵ : Countable ι<VAR>μ : Measure X<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<VAR>i : ι<GOAL>∫ (x : X) in ↑(s i), ‖f x‖ ∂μ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : MeasurableSpace X<VAR>ι : Type u_5<VAR>inst✝⁵ : Countable ι<VAR>μ : Measure X<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : BorelSpace X<VAR>inst✝¹ : MetrizableSpace X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : C(X, E)<VAR>s : ι → Compacts X<VAR>hf : Summable fun i => ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal<VAR>i : ι<GOAL>‖∫ (x : X) in ↑(s i), ‖f x‖ ∂μ‖ ≤ ‖ContinuousMap.restrict (↑(s i)) f‖ * (μ ↑(s i)).toReal
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.negAddY P Q * (P z * Q z) ^ 3 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3
<VAR>k : Type u<VAR>inst✝ : Field k<VAR>m n : ℕ<VAR>h : m ≤ n<VAR>x : Step k m<GOAL>AlgebraicClosure.toStepOfLE' k m n.succ ⋯ x = (⇑(toStepSucc k n) ∘ AlgebraicClosure.toStepOfLE' k m n h) x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>S✝ S : ConvexCone 𝕜 E<VAR>x : E<VAR>hx : x ∈ S<VAR>left✝ : x ≠ 0<VAR>hxneg : -x ∈ S<GOAL>S.Pointed
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : OrderedSemiring 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>S✝ S : ConvexCone 𝕜 E<VAR>x : E<VAR>hx : x ∈ S<VAR>left✝ : x ≠ 0<VAR>hxneg : -x ∈ S<GOAL>x + -x ∈ S
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p q : F[X]<VAR>hpq : Splits (algebraMap F q.SplittingField) p<VAR>hp : IsSolvable p.Gal<VAR>hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal<VAR>K : Type u_1 := p.SplittingField<VAR>L : Type u_1 := q.SplittingField<VAR>this : Fact (Splits (algebraMap F L) p)<VAR>ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p q : F[X]<VAR>hpq : Splits (algebraMap F q.SplittingField) p<VAR>hp : IsSolvable p.Gal<VAR>hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal<VAR>K : Type u_1 := p.SplittingField<VAR>L : Type u_1 := q.SplittingField<VAR>this : Fact (Splits (algebraMap F L) p)<VAR>ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr<VAR>ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p q : F[X]<VAR>hpq : Splits (algebraMap F q.SplittingField) p<VAR>hp : IsSolvable p.Gal<VAR>hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal<VAR>K : Type u_1 := p.SplittingField<VAR>L : Type u_1 := q.SplittingField<VAR>this✝ : Fact (Splits (algebraMap F L) p)<VAR>ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr<VAR>ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom<VAR>this : IsSolvable (K ≃ₐ[F] K)<GOAL>IsSolvable q.Gal
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>p q : F[X]<VAR>hpq : Splits (algebraMap F q.SplittingField) p<VAR>hp : IsSolvable p.Gal<VAR>hq : IsSolvable (Polynomial.map (algebraMap F p.SplittingField) q).Gal<VAR>K : Type u_1 := p.SplittingField<VAR>L : Type u_1 := q.SplittingField<VAR>this✝¹ : Fact (Splits (algebraMap F L) p)<VAR>ϕ : (L ≃ₐ[K] L) ≃* (Polynomial.map (algebraMap F K) q).Gal := (IsSplittingField.algEquiv L (Polynomial.map (algebraMap F K) q)).autCongr<VAR>ϕ_inj : Function.Injective ⇑ϕ.toMonoidHom<VAR>this✝ : IsSolvable (K ≃ₐ[F] K)<VAR>this : IsSolvable (L ≃ₐ[K] L)<GOAL>IsSolvable q.Gal
<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>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace 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>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>this : (toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x) = LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace 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>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>this : (toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x) = LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯<VAR>k : ℕ<VAR>hk : ↑(weightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)<GOAL>_root_.IsNilpotent ((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace 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>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>this : (toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x) = LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯<VAR>k : ℕ<VAR>hk : ↑(weightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)<GOAL>((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x)) ^ k = 0
<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>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>this : (toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x) = LinearMap.restrict ((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ⋯<VAR>k : ℕ<VAR>hk : ↑(weightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)<VAR>m : M<VAR>hm : m ∈ ↑(weightSpace M χ)<GOAL>↑((((toEnd R L ↥↑(weightSpace M χ)) x - (algebraMap R (Module.End R ↥↑(weightSpace M χ))) (χ x)) ^ k) ⟨m, hm⟩) = ↑(0 ⟨m, hm⟩)
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hab : AddLECancellable (a - b)<VAR>h : b ≤ a<GOAL>a - c - (a - b) = b - c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>inst✝ : CompleteLattice α<VAR>s : Set α<GOAL>Ici (sSup s) = ⋂ a ∈ s, Ici a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s₁ s₂ : Finset α<VAR>t t₁ t₂ : α → Finset β<VAR>inst✝ : DecidableEq β<GOAL>↑(s.biUnion t) = ⋃ x ∈ ↑s, ↑(t x)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>{x | ↑x.asIdeal ^ (-↑((Associates.mk x.asIdeal).count (Associates.mk I).factors)) ≠ 1}.Finite
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : Ideal R<VAR>hI : I ≠ 0<GOAL>{x | ¬↑x.asIdeal ^ ↑((Associates.mk x.asIdeal).count (Associates.mk I).factors) = 1}.Finite
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(oneCocycles A)<GOAL>↑f 1 = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>f : ↥(oneCocycles A)<VAR>this : (A.ρ 1) (↑f 1) - ↑f (1 * 1) + ↑f 1 = 0<GOAL>↑f 1 = 0
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : u.r = 0<VAR>hs : x✝.IsSpecial<GOAL>x✝.reduce.IsSpecial
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : u.r = 0<VAR>hs : x✝.IsSpecial<GOAL>u.finish.IsSpecial
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<VAR>hs : x✝.IsSpecial<GOAL>x✝.reduce.IsSpecial
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<VAR>hs : x✝.IsSpecial<VAR>this : sizeOf u.step < sizeOf u<GOAL>x✝.reduce.IsSpecial
<VAR>u✝ x✝ : XgcdType<VAR>u : XgcdType := x✝<VAR>h : ¬u.r = 0<VAR>hs : x✝.IsSpecial<VAR>this : sizeOf u.step < sizeOf u<GOAL>u.step.reduce.flip.IsSpecial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (mulSupport f).Finite<GOAL>∏ᶠ (abc : α × β × γ), f abc = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (mulSupport f).Finite<GOAL>∏ᶠ (a : α) (b : β × γ), f (a, b) = ∏ᶠ (a : α) (b : β) (c : γ), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a✝ b : α<VAR>s t : Set α<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (mulSupport f).Finite<VAR>a : α<GOAL>∏ᶠ (b : β × γ), f (a, b) = ∏ᶠ (b : β) (c : γ), f (a, b, c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f✝ g : α → M<VAR>a✝ b : α<VAR>s t : Set α<VAR>γ : Type u_7<VAR>f : α × β × γ → M<VAR>h : (mulSupport f).Finite<VAR>a : α<GOAL>(mulSupport fun b => f (a, b)).Finite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>({x} ∩ s).encard ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>a b : α<VAR>s : Set α<VAR>x : α<GOAL>({x} ∩ s).encard ≤ {x}.encard
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : One α<GOAL>‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : One α<GOAL>‖(WithLp.equiv 2 (n → α)).symm fun x => 1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : One α<GOAL>↑(Fintype.card n) ^ (1 / 2).toReal * ‖1‖₊ = NNReal.sqrt ↑(Fintype.card n) * ‖1‖₊
<VAR>R : Type u_1<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁶ : Fintype l<VAR>inst✝⁵ : Fintype m<VAR>inst✝⁴ : Fintype n<VAR>inst✝³ : Unique ι<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : SeminormedAddCommGroup α<VAR>inst✝ : One α<GOAL>↑(Fintype.card n) ^ (1 / 2).toReal * ‖1‖₊ = ↑(Fintype.card n) ^ (1 / 2) * ‖1‖₊