ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : SemilatticeSup δ<VAR>inst✝ : OrderBot δ<VAR>g : γ → δ<GOAL>(image₂ f s t).sup g = t.sup fun y => s.sup fun x => g (f x y)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>ζ : Type u_11<VAR>ζ' : Type u_12<VAR>ν : Type u_13<VAR>inst✝⁹ : DecidableEq α'<VAR>inst✝⁸ : DecidableEq β'<VAR>inst✝⁷ : DecidableEq γ<VAR>inst✝⁶ : DecidableEq γ'<VAR>inst✝⁵ : DecidableEq δ<VAR>inst✝⁴ : DecidableEq δ'<VAR>inst✝³ : DecidableEq ε<VAR>inst✝² : DecidableEq ε'<VAR>f f' : α → β → γ<VAR>g✝ g' : α → β → γ → δ<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>u u' : Finset γ<VAR>a a' : α<VAR>b b' : β<VAR>c : γ<VAR>inst✝¹ : SemilatticeSup δ<VAR>inst✝ : OrderBot δ<VAR>g : γ → δ<GOAL>(t.sup fun i' => s.sup fun i => (g ∘ uncurry f) (i, i')) = t.sup fun y => s.sup fun x => g (f x y)
<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✝⁸ : Nonempty ι<VAR>inst✝⁷ : Nonempty ι'<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>p : SeminormFamily 𝕜 E ι<VAR>q : SeminormFamily 𝕜 E ι'<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>hpq : Seminorm.IsBounded p q LinearMap.id<VAR>hqp : Seminorm.IsBounded q p LinearMap.id<GOAL>t = q.moduleFilterBasis.topology
<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✝⁸ : Nonempty ι<VAR>inst✝⁷ : Nonempty ι'<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>p : SeminormFamily 𝕜 E ι<VAR>q : SeminormFamily 𝕜 E ι'<VAR>t : TopologicalSpace E<VAR>hp : WithSeminorms p<VAR>hpq : Seminorm.IsBounded p q LinearMap.id<VAR>hqp : Seminorm.IsBounded q p LinearMap.id<GOAL>p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
<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✝⁸ : Nonempty ι<VAR>inst✝⁷ : Nonempty ι'<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>p : SeminormFamily 𝕜 E ι<VAR>q : SeminormFamily 𝕜 E ι'<VAR>hpq : Seminorm.IsBounded p q LinearMap.id<VAR>hqp : Seminorm.IsBounded q p LinearMap.id<GOAL>p.moduleFilterBasis.topology = q.moduleFilterBasis.topology
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod<VAR>hl : ∀ f_1 ∈ f :: l, Measurable f_1<GOAL>Measurable (f :: l).prod
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod<VAR>hl : Measurable f ∧ ∀ x ∈ l, Measurable x<GOAL>Measurable (f :: l).prod
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : MeasurableSpace M<VAR>inst✝ : MeasurableMul₂ M<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → M<VAR>l : List (α → M)<VAR>ihl : (∀ f ∈ l, Measurable f) → Measurable l.prod<VAR>hl : Measurable f ∧ ∀ x ∈ l, Measurable x<GOAL>Measurable (f * l.prod)
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<VAR>i : ↥M →+* ↥L := Subsemiring.inclusion hi<VAR>this✝ : Algebra ↥M ↥L := i.toAlgebra<VAR>this : SMul ↥M ↥L := Algebra.toSMul<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<VAR>i : ↥M →+* ↥L := Subsemiring.inclusion hi<VAR>this✝¹ : Algebra ↥M ↥L := i.toAlgebra<VAR>this✝ : SMul ↥M ↥L := Algebra.toSMul<VAR>this : IsScalarTower F ↥M ↥L<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<VAR>i : ↥M →+* ↥L := Subsemiring.inclusion hi<VAR>this✝² : Algebra ↥M ↥L := i.toAlgebra<VAR>this✝¹ : SMul ↥M ↥L := Algebra.toSMul<VAR>this✝ : IsScalarTower F ↥M ↥L<VAR>this : IsPurelyInseparable ↥M ↥L<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<VAR>i : ↥M →+* ↥L := Subsemiring.inclusion hi<VAR>this✝² : Algebra ↥M ↥L := i.toAlgebra<VAR>this✝¹ : SMul ↥M ↥L := Algebra.toSMul<VAR>this✝ : IsScalarTower F ↥M ↥L<VAR>this : IsPurelyInseparable ↥M ↥L<VAR>h : Cardinal.lift.{w, v} (sepDegree F E) * Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)<GOAL>sepDegree E ↥L = sepDegree F ↥M
<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>S : Set K<VAR>inst✝¹ : IsPurelyInseparable F E<VAR>M : IntermediateField F K := adjoin F S<VAR>inst✝ : Algebra.IsAlgebraic F ↥M<VAR>L : IntermediateField E K := adjoin E S<VAR>E' : IntermediateField F K := (IsScalarTower.toAlgHom F E K).fieldRange<VAR>j : E ≃ₐ[F] ↥E' := AlgEquiv.ofInjectiveField (IsScalarTower.toAlgHom F E K)<VAR>hi : M ≤ restrictScalars F L<VAR>i : ↥M →+* ↥L := Subsemiring.inclusion hi<VAR>this✝² : Algebra ↥M ↥L := i.toAlgebra<VAR>this✝¹ : SMul ↥M ↥L := Algebra.toSMul<VAR>this✝ : IsScalarTower F ↥M ↥L<VAR>this : IsPurelyInseparable ↥M ↥L<VAR>h : Cardinal.lift.{v, w} (sepDegree E ↥L) = Cardinal.lift.{v, w} (sepDegree F ↥L)<GOAL>sepDegree E ↥L = sepDegree F ↥M
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>y : ↥N<VAR>m : R<VAR>hm : m * ↑y ∈ M<GOAL>IsUnit ((algebraMap R S) ↑y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>y : ↥N<VAR>m : R<VAR>hm : m * ↑y ∈ M<VAR>this : IsUnit ((algebraMap R S) ↑⟨m * ↑y, hm⟩)<GOAL>IsUnit ((algebraMap R S) ↑y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>y : ↥N<VAR>m : R<VAR>hm : m * ↑y ∈ M<VAR>this : IsUnit ((algebraMap R S) m * (algebraMap R S) ↑y)<GOAL>IsUnit ((algebraMap R S) ↑y)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>z : S<GOAL>∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>z : S<VAR>y : R<VAR>s : ↥M<VAR>e : z * (algebraMap R S) ↑(y, s).2 = (algebraMap R S) (y, s).1<GOAL>∃ x, z * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>x✝¹ x✝ : R<GOAL>(algebraMap R S) x✝¹ = (algebraMap R S) x✝ → ∃ c, ↑c * x✝¹ = ↑c * x✝
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁵ : CommSemiring S<VAR>inst✝⁴ : Algebra R S<VAR>P : Type u_3<VAR>inst✝³ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>M N : Submonoid R<VAR>inst✝ : IsLocalization M S<VAR>h : M ≤ N<VAR>h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M<VAR>x✝¹ x✝ : R<GOAL>(∃ c, ↑c * x✝¹ = ↑c * x✝) → ∃ c, ↑c * x✝¹ = ↑c * x✝
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Submonoid R<VAR>P : Type u_2<VAR>inst✝⁵ : CommRing P<VAR>inst✝⁴ : Algebra R P<VAR>loc : IsLocalization S P<VAR>R₁ : Type u_3<VAR>inst✝³ : CommRing R₁<VAR>K : Type u_4<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R₁ K<VAR>inst✝ : IsFractionRing R₁ K<VAR>x✝ : P<GOAL>x✝ ∈ spanSingleton S 0 ↔ x✝ ∈ 0
<VAR>α : Type u_1<VAR>l₁ l₂ l : List α<VAR>d : l.Nodup<VAR>s₁ : l₁ <+ l<VAR>s₂ : l₂ <+ l<VAR>h : l₁ ~ l₂<GOAL>l₁ = l₂
<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₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>i : ι<GOAL>range (Sigma.mk i) = Sigma.fst ⁻¹' {i}
<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₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>i : ι<GOAL>range (Sigma.mk i) ⊆ Sigma.fst ⁻¹' {i}
<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₂ : (i : ι) → Set (α i)<VAR>u : Set ((i : ι) × α i)<VAR>x : (i : ι) × α i<VAR>i✝ j : ι<VAR>a : α i✝<VAR>i : ι<GOAL>Sigma.fst ⁻¹' {i} ⊆ range (Sigma.mk i)
<VAR>n : ℕ<VAR>a b : Fin n<GOAL>(uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
<VAR>x : ℂ<GOAL>ContinuousAt tan x ↔ cos x ≠ 0
<VAR>x : ℂ<VAR>hc : ContinuousAt tan x<VAR>h₀ : cos x = 0<GOAL>False
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d✝ : ℝ<VAR>f : ℝ → E<VAR>d : ℝ<GOAL>∫ (x : ℝ) in a..b, f (d + x) = ∫ (x : ℝ) in d + a..d + b, f x
<VAR>a b : ℝ<VAR>n✝ m n : ℕ<GOAL>∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n) = ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>f : ι → α → β<VAR>μ : Measure α<VAR>p : α → (ι → β) → Prop<VAR>hf : ∀ (i : ι), AEMeasurable (f i) μ<VAR>x : α<VAR>hx : x ∈ aeSeqSet hf p<VAR>i : ι<GOAL>aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp3 : p % 4 = 3<VAR>hpi : ¬Irreducible ↑p<VAR>a b : ℕ<VAR>hab : a ^ 2 + b ^ 2 = p<GOAL>∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hp3 : p % 4 = 3<VAR>hpi : ¬Irreducible ↑p<VAR>a b : ℕ<VAR>hab : a ^ 2 + b ^ 2 = p<GOAL>∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑3
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableInv G<VAR>f : G → E<VAR>μ : Measure G<VAR>inst✝ : μ.IsInvInvariant<GOAL>∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
<VAR>𝕜 : Type u_1<VAR>M : Type u_2<VAR>α : Type u_3<VAR>G : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>μ✝ : Measure G<VAR>f✝ : G → E<VAR>g : G<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableInv G<VAR>f : G → E<VAR>μ : Measure G<VAR>inst✝ : μ.IsInvInvariant<VAR>h : MeasurableEmbedding fun x => x⁻¹<GOAL>∫ (x : G), f x⁻¹ ∂μ = ∫ (x : G), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>σ : Type u_5<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Primcodable β<VAR>inst✝³ : Primcodable γ<VAR>inst✝² : Primcodable δ<VAR>inst✝¹ : Primcodable σ<VAR>inst✝ : DecidableEq α<VAR>a : ℕ × ℕ<GOAL>(fun x x_1 => x ≤ x_1) a.1 a.2 ∧ (fun x x_1 => x ≤ x_1) a.2 a.1 ↔ (fun a b => a = b) a.1 a.2
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<GOAL>IsClosed ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<VAR>val✝ : Fintype ι<GOAL>IsClosed ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hf : ∀ (n : ℕ), f n ∈ ↑(lowerClosure s)<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<GOAL>x ∈ ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hfg : ∀ (n : ℕ), f n ≤ g n<VAR>this : BoundedGENhdsClass ℝ<GOAL>x ∈ ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hfg : ∀ (n : ℕ), f n ≤ g n<VAR>this : BoundedGENhdsClass ℝ<VAR>a : ι → ℝ<VAR>ha : a ∈ lowerBounds (range f)<GOAL>x ∈ ↑(lowerClosure s)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>s t : Set (ι → ℝ)<VAR>a₁ a₂ b₁ b₂ x✝ y : ι → ℝ<VAR>δ : ℝ<VAR>hs : IsClosed s<VAR>hs' : BddAbove s<VAR>val✝ : Fintype ι<VAR>f : ℕ → ι → ℝ<VAR>x : ι → ℝ<VAR>hx : Filter.Tendsto f Filter.atTop (nhds x)<VAR>g : ℕ → ι → ℝ<VAR>hg : ∀ (n : ℕ), g n ∈ s<VAR>hfg : ∀ (n : ℕ), f n ≤ g n<VAR>this : BoundedGENhdsClass ℝ<VAR>a : ι → ℝ<VAR>ha : a ∈ lowerBounds (range f)<VAR>b : ι → ℝ<VAR>hb : b ∈ closure (s ∩ Ici a)<VAR>φ : ℕ → ℕ<VAR>hφ : StrictMono φ<VAR>hbf : Filter.Tendsto (g ∘ φ) Filter.atTop (nhds b)<GOAL>x ∈ ↑(lowerClosure s)
<VAR>α✝ : Type u_1<VAR>M : Type u_2<VAR>β : Type u_3<VAR>α : Type u_4<VAR>inst✝⁹ : MeasurableSpace M<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : Monoid M<VAR>inst✝⁶ : MulAction M β<VAR>inst✝⁵ : MeasurableSMul M β<VAR>inst✝⁴ : MeasurableSpace α<VAR>f : α → β<VAR>μ : Measure α<VAR>G : Type u_5<VAR>inst✝³ : Group G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : MulAction G β<VAR>inst✝ : MeasurableSMul G β<VAR>c : G<VAR>h : AEMeasurable (fun x => c • f x) μ<GOAL>AEMeasurable f μ
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S T : Subsemigroup M<GOAL>∀ {x : M}, x ∈ S → x ∈ S ⊔ T
<VAR>ι : Sort u_1<VAR>M : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝ : Mul M<VAR>S T : Subsemigroup M<VAR>this : S ≤ S ⊔ T<GOAL>∀ {x : M}, x ∈ S → x ∈ S ⊔ T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ✝ : Kernel α (γ × β)<VAR>ν✝ : Kernel α γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>a : α<GOAL>Measurable ((fun p => κ.density ν p.1 p.2 s) ∘ fun x => (a, x))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>ψ θ : R ⧸ AddSubgroup.zmultiples p<VAR>z : ℤ<VAR>hz : z ≠ 0<GOAL>z • ψ = z • θ ↔ ∃ k, ψ = θ + ↑(↑k • (p / ↑z))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>θ : R ⧸ AddSubgroup.zmultiples p<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>a✝ : R<GOAL>z • Quotient.mk'' a✝ = z • θ ↔ ∃ k, Quotient.mk'' a✝ = θ + ↑(↑k • (p / ↑z))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>a✝¹ a✝ : R<GOAL>z • Quotient.mk'' a✝¹ = z • Quotient.mk'' a✝ ↔ ∃ k, Quotient.mk'' a✝¹ = Quotient.mk'' a✝ + ↑(↑k • (p / ↑z))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>a✝¹ a✝ : R<VAR>Zp : AddSubgroup R := AddSubgroup.zmultiples p<VAR>this : Quotient.mk'' = mk<GOAL>z • ↑a✝¹ = z • ↑a✝ ↔ ∃ k, ↑a✝¹ = ↑a✝ + ↑(↑k • (p / ↑z))
<VAR>R : Type u_1<VAR>inst✝¹ : DivisionRing R<VAR>inst✝ : CharZero R<VAR>p : R<VAR>z : ℤ<VAR>hz : z ≠ 0<VAR>a✝¹ a✝ : R<VAR>Zp : AddSubgroup R := AddSubgroup.zmultiples p<VAR>this : Quotient.mk'' = mk<GOAL>z • (a✝¹ - a✝) ∈ Zp ↔ ∃ k, a✝¹ - a✝ - ↑k • (p / ↑z) ∈ Zp
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f✝ g : ι → α<VAR>inst✝ : DivisionSemiring α<VAR>s : Finset ι<VAR>f : ι → α<VAR>a : α<GOAL>(∑ i ∈ s, f i) / a = ∑ i ∈ s, f i / a
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝ : CommSemiring R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<VAR>h : ∀ i ∈ s, (f i).Monic<GOAL>(∏ i ∈ s, f i).natDegree = ∑ i ∈ s, (f i).natDegree
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<VAR>x : α<VAR>F : Set α<VAR>hx : x ∈ F<GOAL>x ∈ connectedComponentIn F x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E'<VAR>h : IsBigOWith c l f₁ f₂<VAR>hc : c < 1<VAR>x : α<GOAL>-(-f₂ x - f₁ x) = f₁ x + f₂ x
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>∑ t ∈ s, weightedVSubVSubWeights k i j t = 0
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>hi : i ∈ s<VAR>hj : j ∈ s<GOAL>∑ x ∈ s, affineCombinationSingleWeights k i x - ∑ x ∈ s, affineCombinationSingleWeights k j x = 0