ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁷ : IsIntegralClosure B A L<VAR>this✝⁶ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁵ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁴ : IsScalarTower A Aₘ K<VAR>this✝³ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝² : Algebra Bₘ L := g.toAlgebra<VAR>this✝¹ : IsScalarTower B Bₘ L<VAR>this✝ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this : IsScalarTower Aₘ K L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁸ : IsIntegralClosure B A L<VAR>this✝⁷ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁶ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁵ : IsScalarTower A Aₘ K<VAR>this✝⁴ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝³ : Algebra Bₘ L := g.toAlgebra<VAR>this✝² : IsScalarTower B Bₘ L<VAR>this✝¹ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝ : IsScalarTower Aₘ K L<VAR>this : IsScalarTower Aₘ Bₘ L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝⁹ : IsIntegralClosure B A L<VAR>this✝⁸ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁷ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁶ : IsScalarTower A Aₘ K<VAR>this✝⁵ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁴ : Algebra Bₘ L := g.toAlgebra<VAR>this✝³ : IsScalarTower B Bₘ L<VAR>this✝² : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝¹ : IsScalarTower Aₘ K L<VAR>this✝ : IsScalarTower Aₘ Bₘ L<VAR>this : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹⁰ : IsIntegralClosure B A L<VAR>this✝⁹ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁸ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁷ : IsScalarTower A Aₘ K<VAR>this✝⁶ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁵ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁴ : IsScalarTower B Bₘ L<VAR>this✝³ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝² : IsScalarTower Aₘ K L<VAR>this✝¹ : IsScalarTower Aₘ Bₘ L<VAR>this✝ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this : FiniteDimensional K L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹¹ : IsIntegralClosure B A L<VAR>this✝¹⁰ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁸ : IsScalarTower A Aₘ K<VAR>this✝⁷ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁶ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁵ : IsScalarTower B Bₘ L<VAR>this✝⁴ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝³ : IsScalarTower Aₘ K L<VAR>this✝² : IsScalarTower Aₘ Bₘ L<VAR>this✝¹ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this✝ : FiniteDimensional K L<VAR>this : IsIntegralClosure Bₘ Aₘ L<GOAL>(algebraMap A Aₘ) ((intTrace A B) x) = (intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x)
<VAR>A : Type u_1<VAR>K✝ : Type u_2<VAR>L✝ : Type u_3<VAR>B : Type u_4<VAR>inst✝³⁵ : CommRing A<VAR>inst✝³⁴ : CommRing B<VAR>inst✝³³ : Algebra A B<VAR>inst✝³² : Field K✝<VAR>inst✝³¹ : Field L✝<VAR>inst✝³⁰ : Algebra A K✝<VAR>inst✝²⁹ : IsFractionRing A K✝<VAR>inst✝²⁸ : Algebra B L✝<VAR>inst✝²⁷ : Algebra K✝ L✝<VAR>inst✝²⁶ : Algebra A L✝<VAR>inst✝²⁵ : IsScalarTower A B L✝<VAR>inst✝²⁴ : IsScalarTower A K✝ L✝<VAR>inst✝²³ : IsIntegralClosure B A L✝<VAR>inst✝²² : FiniteDimensional K✝ L✝<VAR>Aₘ : Type u_5<VAR>Bₘ : Type u_6<VAR>inst✝²¹ : CommRing Aₘ<VAR>inst✝²⁰ : CommRing Bₘ<VAR>inst✝¹⁹ : Algebra Aₘ Bₘ<VAR>inst✝¹⁸ : Algebra A Aₘ<VAR>inst✝¹⁷ : Algebra B Bₘ<VAR>inst✝¹⁶ : Algebra A Bₘ<VAR>inst✝¹⁵ : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹⁴ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹³ : IsLocalization M Aₘ<VAR>inst✝¹² : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝¹¹ : IsDomain A<VAR>inst✝¹⁰ : IsIntegrallyClosed A<VAR>inst✝⁹ : IsDomain B<VAR>inst✝⁸ : IsIntegrallyClosed B<VAR>inst✝⁷ : Module.Finite A B<VAR>inst✝⁶ : NoZeroSMulDivisors A B<VAR>inst✝⁵ : IsDomain Aₘ<VAR>inst✝⁴ : IsIntegrallyClosed Aₘ<VAR>inst✝³ : IsDomain Bₘ<VAR>inst✝² : IsIntegrallyClosed Bₘ<VAR>inst✝¹ : NoZeroSMulDivisors Aₘ Bₘ<VAR>inst✝ : Module.Finite Aₘ Bₘ<VAR>x : B<VAR>hM : M ≤ A⁰<VAR>K : Type u_1 := FractionRing A<VAR>L : Type u_4 := FractionRing B<VAR>this✝¹¹ : IsIntegralClosure B A L<VAR>this✝¹⁰ : IsLocalization (algebraMapSubmonoid B A⁰) L<VAR>f : Aₘ →+* K := IsLocalization.map K (RingHom.id A) hM<VAR>this✝⁹ : Algebra Aₘ K := f.toAlgebra<VAR>this✝⁸ : IsScalarTower A Aₘ K<VAR>this✝⁷ : IsFractionRing Aₘ K := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization M Aₘ K<VAR>g : Bₘ →+* L := IsLocalization.map L (RingHom.id B) ⋯<VAR>this✝⁶ : Algebra Bₘ L := g.toAlgebra<VAR>this✝⁵ : IsScalarTower B Bₘ L<VAR>this✝⁴ : Algebra Aₘ L := ((algebraMap K L).comp f).toAlgebra<VAR>this✝³ : IsScalarTower Aₘ K L<VAR>this✝² : IsScalarTower Aₘ Bₘ L<VAR>this✝¹ : IsFractionRing Bₘ L := IsFractionRing.isFractionRing_of_isDomain_of_isLocalization (algebraMapSubmonoid B M) Bₘ L<VAR>this✝ : FiniteDimensional K L<VAR>this : IsIntegralClosure Bₘ Aₘ L<GOAL>(algebraMap Aₘ K) ((algebraMap A Aₘ) ((intTrace A B) x)) = (algebraMap Aₘ K) ((intTrace Aₘ Bₘ) ((algebraMap B Bₘ) x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : UpperSet α<VAR>a : α<VAR>f : (i : ι) → κ i → UpperSet α<GOAL>(⨅ i, ⨅ j, f i j).compl = ⨅ i, ⨅ j, (f i j).compl
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<GOAL>∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Ioc 0 M, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<GOAL>∫ (t : ℝ) in Ioi 0, (μ {a | t ≤ f a}).toReal = ∫ (t : ℝ) in Ioc 0 M, (μ {a | t ≤ f a}).toReal
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<GOAL>∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → (μ {a | x ≤ f a}).toReal = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0 \ Ioc 0 M<GOAL>(μ {a | t ≤ f a}).toReal = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0 \ Ioc 0 M<VAR>htM : M < t<GOAL>(μ {a | t ≤ f a}).toReal = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0 \ Ioc 0 M<VAR>htM : M < t<VAR>obs : μ {a | M < f a} = 0<GOAL>(μ {a | t ≤ f a}).toReal = 0
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>μ : Measure α<VAR>f✝ f : α → ℝ<VAR>M : ℝ<VAR>f_intble : Integrable f μ<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_bdd : f ≤ᶠ[ae μ] fun x => M<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0 \ Ioc 0 M<VAR>htM : M < t<VAR>obs : μ {a | M < f a} = 0<GOAL>μ {a | t ≤ f a} = 0 ∨ μ {a | t ≤ f a} = ⊤
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>m.toNat ≤ n ↔ m ≤ ↑n
<VAR>a b c d m n✝ : ℤ<VAR>n : ℕ<GOAL>m ≤ ↑n ∧ 0 ≤ ↑n ↔ m ≤ ↑n
<VAR>B : Type u<VAR>inst✝ : Bicategory B<VAR>a b c : B<VAR>f : a ⟶ b<VAR>h : b ⟶ c<GOAL>eqToHom ⋯ ▷ h = eqToHom ⋯
<VAR>z τ : ℂ<GOAL>jacobiTheta₂'' (-z) τ = -jacobiTheta₂'' z τ
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R<VAR>hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R<VAR>hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)<VAR>hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)<GOAL>∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<VAR>Ω : Type u_1<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>ℱ : Filtration ℕ m0<VAR>f : ℕ → Ω → ℝ<VAR>ω✝ : Ω<VAR>r : ℝ<VAR>R : ℝ≥0<VAR>inst✝ : IsFiniteMeasure μ<VAR>hf : Martingale f ℱ μ<VAR>hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R<VAR>hbdd' : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |(-f) (i + 1) ω - (-f) i ω| ≤ ↑R<VAR>hup : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)<VAR>hdown : ∀ᵐ (ω : Ω) ∂μ, BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)<VAR>ω : Ω<VAR>hω₁ : BddAbove (Set.range fun n => f n ω) ↔ ∃ c, Tendsto (fun n => f n ω) atTop (𝓝 c)<VAR>hω₂ : BddAbove (Set.range fun n => (-f) n ω) ↔ ∃ c, Tendsto (fun n => (-f) n ω) atTop (𝓝 c)<GOAL>BddAbove (Set.range fun n => f n ω) ↔ BddBelow (Set.range fun n => f n ω)
<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Quiver.IsThin C<GOAL>EssentiallySmall.{w, v, u} C ↔ Small.{w, u} (Skeleton C)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>R : ℝ<VAR>hR : 0 ≤ R<GOAL>∫ (x : E), f (R • x) ∂μ = (R ^ finrank ℝ E)⁻¹ • ∫ (x : E), f x ∂μ
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit z<VAR>h1 : x = y * inverse z<GOAL>x * z = y
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝ : MonoidWithZero M₀<VAR>x y z : M₀<VAR>h : IsUnit z<VAR>h1 : x * z = y<GOAL>x = y * inverse z
<VAR>M : Type u_1<VAR>inst✝¹ : OrderedCancelAddCommMonoid M<VAR>inst✝ : ExistsAddOfLE M<VAR>a b c d : M<GOAL>(fun x => a + x) '' Ico b c = Ico (a + b) (a + c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : TopologicalSpace α<VAR>f g : β → α<VAR>a b : α<VAR>s : Finset β<VAR>h : ¬Multipliable f<GOAL>∏' (b : β), f b = 1
<VAR>G₀ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : GroupWithZero G₀<VAR>inst✝¹ : Bornology G₀<VAR>inst✝ : MulAction G₀ α<VAR>s t u : Set α<VAR>S : Set (Set α)<VAR>hS : S.Finite<GOAL>Absorbs G₀ (⋂₀ S) t ↔ ∀ s ∈ S, Absorbs G₀ s t
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedRing R<VAR>inst✝ : Archimedean R<VAR>hr : r < 0<VAR>hf : Tendsto f l atTop<GOAL>Tendsto (fun x => f x * r) l atBot
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<GOAL>(closure s ∩ u).Nonempty → (closure s ∩ v).Nonempty → (closure s ∩ (u ∩ v)).Nonempty ↔ (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<GOAL>IsOpen (u ∩ v)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<GOAL>IsOpen v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<GOAL>IsOpen u
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>R : Type u_3<VAR>inst✝ : LinearOrderedSemiring R<VAR>a b : R<VAR>m n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n ≠ 0<GOAL>1 ≤ a ^ n ↔ 1 ≤ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<GOAL>↑(⋯.fix (fun a IH => let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) a) ∈ {b | ∀ (a' : α), r a' a → s (↑(⋯.fix (fun a IH => let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) a')) b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<GOAL>↑(let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑((fun y x => ⋯.fix (fun a IH => let S := {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) y) a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) ∈ {b | ∀ (a' : α), r a' a → s (↑(⋯.fix (fun a IH => let S := {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b}; let_fun this := ⋯; ⟨⋯.min S ⋯, ⋯⟩) a')) b}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>inst✝ : IsWellOrder β s<VAR>f : r ↪r s<VAR>a : α<GOAL>⋯.min {b | ∀ (a_1 : α), r a_1 a → s (↑(⋯.fix (fun a IH => ⟨⋯.min {b | ∀ (a_2 : α) (h : r a_2 a), s (↑(IH a_2 h)) b} ⋯, ⋯⟩) a_1)) b} ⋯ ∈ {b | ∀ (a' : α), r a' a → s (↑(⋯.fix (fun a IH => ⟨⋯.min {b | ∀ (a_1 : α) (h : r a_1 a), s (↑(IH a_1 h)) b} ⋯, ⋯⟩) a')) b}
<VAR>F : Type u<VAR>inst✝³ : Field F<VAR>K : Type v<VAR>inst✝² : Field K<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Nontrivial S<VAR>f : F →+* S<VAR>p : F[X]<GOAL>(map f p).Separable ↔ p.Separable
<VAR>F : Type u<VAR>inst✝³ : Field F<VAR>K : Type v<VAR>inst✝² : Field K<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Nontrivial S<VAR>f : F →+* S<VAR>p : F[X]<VAR>H : (map f p).Separable<GOAL>p.Separable
<VAR>F : Type u<VAR>inst✝³ : Field F<VAR>K : Type v<VAR>inst✝² : Field K<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Nontrivial S<VAR>f : F →+* S<VAR>p : F[X]<VAR>H : (map f p).Separable<VAR>m : Ideal S<VAR>hm : m.IsMaximal<GOAL>p.Separable
<VAR>F : Type u<VAR>inst✝³ : Field F<VAR>K : Type v<VAR>inst✝² : Field K<VAR>S : Type u_1<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Nontrivial S<VAR>f : F →+* S<VAR>p : F[X]<VAR>H : (map f p).Separable<VAR>m : Ideal S<VAR>hm : m.IsMaximal<VAR>this : (map (Ideal.Quotient.mk m) (map f p)).Separable<GOAL>p.Separable
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : Preadditive C<VAR>R : Type u_1<VAR>inst✝¹ : Ring R<VAR>inst✝ : Linear R C<VAR>F G K L : CochainComplex C ℤ<VAR>n m n₁ n₂ n₁₂ : ℤ<VAR>z₂ : Cochain G K n₂<VAR>h : n₁ + n₂ = n₁₂<VAR>p q : ℤ<VAR>hpq : p + n₁₂ = q<GOAL>(comp 0 z₂ h).v p q hpq = v 0 p q hpq
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>g : X ⟶ X<GOAL>g ≫ f = f ↔ g = 𝟙 X
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : C<VAR>f : X ⟶ Y<VAR>inst✝ : Mono f<VAR>g : X ⟶ X<GOAL>f = 𝟙 X ≫ f
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>Continuous toLevyProkhorov
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝³ : PseudoMetricSpace Ω<VAR>inst✝² : SeparableSpace Ω<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<GOAL>∀ (x : ProbabilityMeasure Ω), ContinuousAt toLevyProkhorov x