ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X] := f.toSubring E'.toSubring ⋯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X] := f.toSubring E'.toSubring ⋯<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>hsep : IsSeparable E x<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : g.Separable<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this : Algebra.IsSeparable F ↥E'<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝¹ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝ : Algebra.IsSeparable F ↥E'<VAR>this : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝² : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝¹ : Algebra.IsSeparable F ↥E'<VAR>this✝ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝³ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝² : Algebra.IsSeparable F ↥E'<VAR>this✝¹ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this✝ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<VAR>this : FiniteDimensional F ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝⁴ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝³ : Algebra.IsSeparable F ↥E'<VAR>this✝² : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this✝¹ : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<VAR>this✝ : FiniteDimensional F ↥(↥E')⟮x⟯<VAR>this : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝⁵ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝⁴ : Algebra.IsSeparable F ↥E'<VAR>this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<VAR>this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯<VAR>this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯<VAR>this : finSepDegree F ↥E' * finSepDegree ↥E' ↥(↥E')⟮x⟯ = finSepDegree F ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝⁵ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝⁴ : Algebra.IsSeparable F ↥E'<VAR>this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<VAR>this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯<VAR>this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯<VAR>this : Algebra.IsSeparable F ↥(↥E')⟮x⟯<GOAL>IsSeparable F x
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>K : Type w<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>inst✝² : Algebra E K<VAR>inst✝¹ : IsScalarTower F E K<VAR>inst✝ : Algebra.IsSeparable F E<VAR>x : K<VAR>f : E[X] := minpoly E x<VAR>hf : f = minpoly E x<VAR>E' : IntermediateField F E := adjoin F ↑f.coeffs<VAR>this✝⁵ : FiniteDimensional F ↥E'<VAR>g : (↥E')[X]<VAR>h : Polynomial.map (algebraMap (↥E') E) g = f<VAR>hx : x ∈ restrictScalars F (↥E')⟮x⟯<VAR>hzero : (aeval x) g = 0<VAR>halg : IsIntegral (↥E') x<VAR>hsep : (minpoly (↥E') x).Separable<VAR>this✝⁴ : Algebra.IsSeparable F ↥E'<VAR>this✝³ : Algebra.IsSeparable ↥E' ↥(↥E')⟮x⟯<VAR>this✝² : FiniteDimensional ↥E' ↥(↥E')⟮x⟯<VAR>this✝¹ : FiniteDimensional F ↥(↥E')⟮x⟯<VAR>this✝ : Algebra.IsAlgebraic ↥E' ↥(↥E')⟮x⟯<VAR>this : Algebra.IsSeparable F ↥(restrictScalars F (↥E')⟮x⟯)<GOAL>IsSeparable F x
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>Fintype.card ↑(Set.Ioi a) = n - 1 - ↑a
<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>S : NonUnitalSubalgebra R A<VAR>a : A<VAR>ha : a ∈ S ⊔ star S<GOAL>star a ∈ S ⊔ star S
<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>S : NonUnitalSubalgebra R A<VAR>a : A<VAR>ha : a ∈ NonUnitalAlgebra.adjoin R (↑S ⊔ ↑(star S))<GOAL>a ∈ star (NonUnitalAlgebra.adjoin R (↑S ⊔ ↑(star S)))
<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>S : NonUnitalSubalgebra R A<VAR>a : A<VAR>ha : a ∈ NonUnitalAlgebra.adjoin R (↑S ⊔ ↑(star S))<GOAL>star (NonUnitalAlgebra.adjoin R (↑S ⊔ ↑(star S))) = NonUnitalAlgebra.adjoin R (↑S ⊔ ↑(star S))
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<VAR>e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<VAR>e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm<VAR>hem : MeasurePreserving (⇑e) volume volume<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<VAR>e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm<VAR>hem : MeasurePreserving (⇑e) volume volume<VAR>heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π<GOAL>(∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) = ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<VAR>e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm<VAR>hem : MeasurePreserving (⇑e) volume volume<VAR>heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π<GOAL>∫ (x : ℝ) in Icc 0 (2 * π), ∫ (y : Fin n → ℝ) in Icc 0 fun x => 2 * π, (∏ i : Fin (n + 1), ↑(R i) * cexp (↑(e (x, y) i) * I) * I) • f (torusMap c R (e (x, y))) = ∫ (θ : ℝ) in Icc 0 (2 * π), deriv (circleMap (c i) (R i)) θ • ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth (circleMap (c i) (R i) θ) y)
<VAR>n : ℕ<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : (Fin n → ℂ) → E<VAR>c✝ : Fin n → ℂ<VAR>R✝ : Fin n → ℝ<VAR>f : (Fin (n + 1) → ℂ) → E<VAR>c : Fin (n + 1) → ℂ<VAR>R : Fin (n + 1) → ℝ<VAR>hf : TorusIntegrable f c R<VAR>i : Fin (n + 1)<VAR>e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm<VAR>hem : MeasurePreserving (⇑e) volume volume<VAR>heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π<GOAL>IntegrableOn (fun x => (∏ i : Fin (n + 1), ↑(R i) * cexp (↑(e x i) * I) * I) • f (torusMap c R (e x))) (Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π) (volume.prod volume)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<VAR>ho : s.WOppSide x y<GOAL>False
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : LinearOrderedField R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>h : s.SSameSide x y<VAR>ho : s.WOppSide x y<VAR>hxy : x ∈ s ∨ y ∈ s<GOAL>False
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q p : R[X]<VAR>n i : ℕ<VAR>h : i ≠ n<GOAL>(erase n p).coeff i = p.coeff i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<GOAL>Continuous (Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<GOAL>Continuous ((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<GOAL>(Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f = Quotient.mk'
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>x✝ : X<GOAL>((Setoid.quotientKerEquivOfSurjective ⇑f ⋯).invFun ∘ ⇑f) x✝ = Quotient.mk' x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>f : C(X, Y)<VAR>hf : QuotientMap ⇑f<VAR>x✝ : X<GOAL>f x✝ = (Setoid.quotientKerEquivOfSurjective ⇑f ⋯) (Quotient.mk' x✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<GOAL>s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : s ×ˢ t = ∅<GOAL>s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : (s ×ˢ t).Nonempty<GOAL>s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>h : (s ×ˢ t).Nonempty<VAR>st : s.Nonempty ∧ t.Nonempty<GOAL>s ×ˢ t ⊆ s₁ ×ˢ t₁ ↔ s ⊆ s₁ ∧ t ⊆ t₁ ∨ s = ∅ ∨ t = ∅
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>zeroLocus 𝒜 ↑(vanishingIdeal t) = closure t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>zeroLocus 𝒜 ↑(vanishingIdeal t) ⊆ closure t
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<GOAL>closure t ⊆ zeroLocus 𝒜 ↑(vanishingIdeal t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>s t u : Set α<VAR>f : α → β<VAR>h : Disjoint s t<VAR>hf : InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>Disjoint (f '' s) (f '' t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>π : α → Type u_5<VAR>s✝ s₁ s₂ : Set α<VAR>t✝ t₁ t₂ : Set β<VAR>p : Set γ<VAR>f✝ f₁ f₂ f₃ : α → β<VAR>g g₁ g₂ : β → γ<VAR>f' f₁' f₂' : β → α<VAR>g' : γ → β<VAR>a : α<VAR>b : β<VAR>s t u : Set α<VAR>f : α → β<VAR>h : s ∩ t = ∅<VAR>hf : InjOn f u<VAR>hs : s ⊆ u<VAR>ht : t ⊆ u<GOAL>f '' s ∩ f '' t = ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List (Option α)<VAR>x : α<GOAL>(l.concat (some x)).reduceOption = l.reduceOption.concat x
<VAR>𝕜 : Type u_1<VAR>inst✝³⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³⁶ : NormedAddCommGroup E<VAR>inst✝³⁵ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝³⁴ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝³³ : TopologicalSpace M<VAR>inst✝³² : ChartedSpace H M<VAR>inst✝³¹ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝³⁰ : NormedAddCommGroup E'<VAR>inst✝²⁹ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝²⁸ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝²⁷ : TopologicalSpace M'<VAR>inst✝²⁶ : ChartedSpace H' M'<VAR>inst✝²⁵ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝²⁴ : NormedAddCommGroup E''<VAR>inst✝²³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝²² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝²¹ : TopologicalSpace M''<VAR>inst✝²⁰ : ChartedSpace H'' M''<VAR>F : Type u_11<VAR>inst✝¹⁹ : NormedAddCommGroup F<VAR>inst✝¹⁸ : NormedSpace 𝕜 F<VAR>G : Type u_12<VAR>inst✝¹⁷ : TopologicalSpace G<VAR>J : ModelWithCorners 𝕜 F G<VAR>N : Type u_13<VAR>inst✝¹⁶ : TopologicalSpace N<VAR>inst✝¹⁵ : ChartedSpace G N<VAR>inst✝¹⁴ : SmoothManifoldWithCorners J N<VAR>F' : Type u_14<VAR>inst✝¹³ : NormedAddCommGroup F'<VAR>inst✝¹² : NormedSpace 𝕜 F'<VAR>G' : Type u_15<VAR>inst✝¹¹ : TopologicalSpace G'<VAR>J' : ModelWithCorners 𝕜 F' G'<VAR>N' : Type u_16<VAR>inst✝¹⁰ : TopologicalSpace N'<VAR>inst✝⁹ : ChartedSpace G' N'<VAR>inst✝⁸ : SmoothManifoldWithCorners J' N'<VAR>F₁ : Type u_17<VAR>inst✝⁷ : NormedAddCommGroup F₁<VAR>inst✝⁶ : NormedSpace 𝕜 F₁<VAR>F₂ : Type u_18<VAR>inst✝⁵ : NormedAddCommGroup F₂<VAR>inst✝⁴ : NormedSpace 𝕜 F₂<VAR>F₃ : Type u_19<VAR>inst✝³ : NormedAddCommGroup F₃<VAR>inst✝² : NormedSpace 𝕜 F₃<VAR>F₄ : Type u_20<VAR>inst✝¹ : NormedAddCommGroup F₄<VAR>inst✝ : NormedSpace 𝕜 F₄<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f✝ f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>f : M → M'<VAR>g : M → N'<VAR>hf : ContMDiffWithinAt I I' n f s x<VAR>hg : ContMDiffWithinAt I J' n g s x<GOAL>ContMDiffWithinAt I (I'.prod J') n (fun x => (f x, g x)) s x