ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>Ω : Type u_1<VAR>inst✝² : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝¹ : TopologicalSpace Ω<VAR>inst✝ : OpensMeasurableSpace Ω<VAR>γ : Type u_2<VAR>F : Filter γ<VAR>μs : γ → FiniteMeasure Ω<VAR>μs_lim : ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ((ProbabilityMeasure.toFiniteMeasure ∘ fun i => (μs i).normalize) i).testAgainstNN f) F (𝓝 (μ.normalize.toFiniteMeasure.testAgainstNN f))<VAR>mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)<VAR>f : Ω →ᵇ ℝ≥0<VAR>h_mass : ¬μ.mass = 0<VAR>lim_pair : Tendsto (fun i => ((μs i).mass, (μs i).normalize.toFiniteMeasure.testAgainstNN f)) F (𝓝 (μ.mass, μ.normalize.toFiniteMeasure.testAgainstNN f))<GOAL>Tendsto (fun i => (μs i).mass * (μs i).normalize.toFiniteMeasure.testAgainstNN f) F (𝓝 (μ.mass * μ.normalize.toFiniteMeasure.testAgainstNN f))
<VAR>x y : ℝ<VAR>hx : 0 < x<GOAL>log x ≤ 0 ↔ x ≤ 1
<VAR>l m r : List Char<VAR>f : Char → Bool<VAR>x✝ : Substring<VAR>h : ValidFor l m r x✝<GOAL>x✝.all f = m.all f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : ℕ<VAR>s : Multiset α<GOAL>powersetCard n (map f s) = map (map f) (powersetCard n s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>n : ℕ<GOAL>powersetCard n (map f 0) = map (map f) (powersetCard n 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>t : α<VAR>s : Multiset α<VAR>ih : ∀ (n : ℕ), powersetCard n (map f s) = map (map f) (powersetCard n s)<VAR>n : ℕ<GOAL>powersetCard n (map f (t ::ₘ s)) = map (map f) (powersetCard n (t ::ₘ s))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : (image f s).Nonempty<GOAL>(image f s).max' h = f (s.max' ⋯)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : LinearOrder α<VAR>s✝ : Finset α<VAR>H : s✝.Nonempty<VAR>x : α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>hf : Monotone f<VAR>s : Finset α<VAR>h : (image f s).Nonempty<GOAL>s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)
<VAR>X : Type u_1<VAR>inst✝ : TopologicalSpace X<VAR>L : Locale<VAR>x : X<VAR>S : Set (Opens X)<GOAL>{ toFun := fun x_1 => x ∈ x_1, map_inf' := ⋯, map_top' := ⋯ }.toFun (sSup S) = sSup ({ toFun := fun x_1 => x ∈ x_1, map_inf' := ⋯, map_top' := ⋯ }.toFun '' S)
<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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝¹ : IsIntegralClosure B A (FractionRing B)<VAR>this✝ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this : FiniteDimensional (FractionRing A) (FractionRing B)<GOAL>(algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(algebraMap A K) ((intTrace A B) x) = (trace K L) ((algebraMap B L) 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(FractionRing.algEquiv A K).symm ((algebraMap A K) ((intTrace A B) x)) = (FractionRing.algEquiv A K).symm ((trace K L) ((algebraMap B L) 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(trace (FractionRing A) (FractionRing B)) ((algebraMap B (FractionRing B)) x) = (FractionRing.algEquiv A K).symm ((trace K L) ((FractionRing.algEquiv B L) ((algebraMap B (FractionRing 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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>(algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv = (↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))
<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.262054<VAR>Bₘ : Type ?u.262057<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>x : B<VAR>this✝² : IsIntegralClosure B A (FractionRing B)<VAR>this✝¹ : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<VAR>this✝ : FiniteDimensional (FractionRing A) (FractionRing B)<VAR>this : IsFractionRing B L<GOAL>((algebraMap K L).comp ↑(FractionRing.algEquiv A K).toRingEquiv).comp (algebraMap A (FractionRing A)) = ((↑(FractionRing.algEquiv B L).toRingEquiv).comp (algebraMap (FractionRing A) (FractionRing B))).comp (algebraMap A (FractionRing A))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>x y : R<VAR>H : (iterateFrobenius R p n) x = (iterateFrobenius R p n) y<GOAL>x = y
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>x y : R<VAR>H : (iterateFrobenius R p n) x - (iterateFrobenius R p n) y = 0<GOAL>x - y = 0
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsReduced R<VAR>p n : ℕ<VAR>inst✝ : ExpChar R p<VAR>x y : R<VAR>H : (x - y) ^ p ^ n = 0<GOAL>x - y = 0
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝⁴ : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>inst✝² : MonoidalCategory C<VAR>W X Y Z : C<VAR>f : W ⟶ X<VAR>inst✝¹ : IsIso f<VAR>g : Y ⟶ Z<VAR>inst✝ : IsIso g<GOAL>inv (f ⊗ g) = inv f ⊗ inv g
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>(basisDivisor x y).degree = 1
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>(x - y)⁻¹ ≠ 0
<VAR>m : Type u_1<VAR>n : Type u_2<VAR>o : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝³ : Fintype n<VAR>inst✝² : Fintype o<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>M N : Matrix m n R<VAR>i : m<GOAL>(M + N).toMvPolynomial i = (M.toMvPolynomial + N.toMvPolynomial) i
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>(o.areaForm x) x = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>o.volumeForm ![x, x] = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>![x, x] 0 = ![x, x] 1
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x : E<GOAL>0 ≠ 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x : FreeAbelianGroup α<GOAL>(map id) x = x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>x : FreeAbelianGroup α<GOAL>(AddMonoidHom.id (FreeAbelianGroup α)) x = x
<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 : ℝ<VAR>f g : ℝ → E<VAR>μ : Measure ℝ<VAR>h : a ≤ b<GOAL>∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ = ∫ (x : ℝ) in a..b, ‖f x‖ ∂μ
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>a x : 𝕜<VAR>𝕜' : Type u_2<VAR>inst✝¹ : NormedAddCommGroup 𝕜'<VAR>inst✝ : NormedSpace 𝕜 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h' : 𝕜'<VAR>hh : HasDerivAt h h' (a + x)<GOAL>HasDerivAt (fun x => h (a + x)) h' x
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<GOAL>J(a | b) = J(a | b % (4 * a.natAbs))
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<VAR>ha : a = ↑a.natAbs<GOAL>J(↑a.natAbs | b) = J(↑a.natAbs | b % (4 * a.natAbs))
<VAR>a : ℤ<VAR>b : ℕ<VAR>hb : Odd b<VAR>ha : a = -↑a.natAbs<GOAL>J(-↑a.natAbs | b) = J(-↑a.natAbs | b % (4 * a.natAbs))
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>h_anti : AntitoneOn (deriv f) (interior D)<GOAL>MonotoneOn (deriv (-f)) (interior D)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0<GOAL>DifferentiableOn ℝ (deriv f) (interior (interior D))
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'' : DifferentiableOn ℝ (deriv f) (interior D)<VAR>hf''_nonpos : ∀ x ∈ interior D, deriv^[2] f x ≤ 0<GOAL>∀ x ∈ interior (interior D), deriv (deriv f) x ≤ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0<VAR>s : Set α<VAR>hs : ν s = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>f : α → β<VAR>h : ∀ ⦃s : Set α⦄, MeasurableSet s → ν s = 0 → μ s = 0<VAR>s : Set α<VAR>hs : ν s = 0<VAR>t : Set α<VAR>h1t : s ⊆ t<VAR>h2t : MeasurableSet t<VAR>h3t : ν t = 0<GOAL>μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>∫⁻ (x : α × β) in s ×ˢ t, f x ∂μ ⊗ₘ κ = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>μ : Measure α<VAR>κ η : Kernel α β<VAR>inst✝¹ : SFinite μ<VAR>inst✝ : IsSFiniteKernel κ<VAR>f : α × β → ℝ≥0∞<VAR>hf : Measurable f<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set β<VAR>ht : MeasurableSet t<GOAL>∫⁻ (x : α) in s, ∫⁻ (y : β) in t, f (x, y) ∂(Kernel.prodMkLeft Unit κ) ((), x) ∂(Kernel.const Unit μ) () = ∫⁻ (a : α) in s, ∫⁻ (b : β) in t, f (a, b) ∂κ a ∂μ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<GOAL>s ∈ coclosedLindelof X ↔ ∃ t, IsClosed t ∧ IsLindelof t ∧ sᶜ ⊆ t
<VAR>V✝ : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝⁵ : SeminormedAddCommGroup V✝<VAR>inst✝⁴ : SeminormedAddCommGroup V₁<VAR>inst✝³ : SeminormedAddCommGroup V₂<VAR>inst✝² : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>V : Type u_5<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : Nontrivial V<GOAL>‖id V‖ = 1
<VAR>V✝ : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝⁵ : SeminormedAddCommGroup V✝<VAR>inst✝⁴ : SeminormedAddCommGroup V₁<VAR>inst✝³ : SeminormedAddCommGroup V₂<VAR>inst✝² : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>V : Type u_5<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : Nontrivial V<GOAL>∃ x, ‖x‖ ≠ 0
<VAR>V✝ : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝⁵ : SeminormedAddCommGroup V✝<VAR>inst✝⁴ : SeminormedAddCommGroup V₁<VAR>inst✝³ : SeminormedAddCommGroup V₂<VAR>inst✝² : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>V : Type u_5<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : Nontrivial V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∃ x, ‖x‖ ≠ 0
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fst✝¹ : Perm α<VAR>snd✝¹ : Perm β<VAR>fst✝ : Perm α<VAR>snd✝ : Perm β<VAR>h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)<GOAL>(fst✝¹, snd✝¹) = (fst✝, snd✝)
<VAR>α✝ : Type u<VAR>β✝ : Type v<VAR>α : Type u_1<VAR>β : Type u_2<VAR>fst✝¹ : Perm α<VAR>snd✝¹ : Perm β<VAR>fst✝ : Perm α<VAR>snd✝ : Perm β<VAR>h : (sumCongrHom α β) (fst✝¹, snd✝¹) = (sumCongrHom α β) (fst✝, snd✝)<GOAL>fst✝¹ = fst✝ ∧ snd✝¹ = snd✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIcoMod hp a (b + m • p) = toIcoMod hp a b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b + m • p - (toIcoDiv hp a b • p + m • p) = b - toIcoDiv hp a b • p
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<VAR>x : α<VAR>x_mem : x ∈ closure E<GOAL>thickenedIndicatorAux δ E x = 1
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.RightHomologyData<VAR>A : C<VAR>hf : S.f = 0<VAR>hg : S.g = 0<GOAL>(ofZeros S hf hg).g' = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>S₁ S₂ S₃ : ShortComplex C<VAR>φ φ' : S₁ ⟶ S₂<VAR>h₁ : S₁.RightHomologyData<VAR>h₂ : S₂.RightHomologyData<VAR>γ : RightHomologyMapData φ h₁ h₂<GOAL>opcyclesMap' (-φ) h₁ h₂ = -opcyclesMap' φ h₁ h₂
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>f : (n → R) →ₗ[R] m → R<VAR>g : (l → R) →ₗ[R] n → R<GOAL>toMatrix' (f ∘ₗ g) = toMatrix' f * toMatrix' g
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype l<VAR>inst✝ : DecidableEq l<VAR>f : (n → R) →ₗ[R] m → R<VAR>g : (l → R) →ₗ[R] n → R<GOAL>f ∘ₗ g = toLin' (toMatrix' f * toMatrix' g)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝¹¹ : CommRing K<VAR>inst✝¹⁰ : CommRing L<VAR>inst✝⁹ : CommRing M<VAR>inst✝⁸ : CommRing N<VAR>i : K →+* L<VAR>j : K →+* M<VAR>k : K →+* N<VAR>f : L →+* M<VAR>g : L →+* N<VAR>p : ℕ<VAR>inst✝⁷ : ExpChar K p<VAR>inst✝⁶ : ExpChar L p<VAR>inst✝⁵ : ExpChar M p<VAR>inst✝⁴ : ExpChar N p<VAR>inst✝³ : PerfectRing L p<VAR>inst✝² : IsPerfectClosure i p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPerfectClosure j p<VAR>x : M<VAR>n : ℕ<VAR>y : K<VAR>h : j y = x ^ p ^ n<GOAL>(equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>ha : ↑a ≠ ⊤<VAR>h'a : ↑a ≠ ⊥<GOAL>Tendsto toReal (𝓝 ↑a) (𝓝 (↑a).toReal)
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>a : ℝ<VAR>ha : ↑a ≠ ⊤<VAR>h'a : ↑a ≠ ⊥<GOAL>Tendsto (toReal ∘ Real.toEReal) (𝓝 a) (𝓝 (↑a).toReal)
<VAR>ι : Type u<VAR>X : Type v<VAR>inst✝⁴ : TopologicalSpace X<VAR>E : Type u_1<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMulWithZero ℝ E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ : Set X<VAR>f : PartitionOfUnity ι X s✝<VAR>s : Set X<VAR>ρ : PartitionOfUnity ι X s<VAR>x₀✝ x₀ : X<VAR>hx₀ : x₀ ∈ s<VAR>I : Finset ι<VAR>hI : ρ.finsupport x₀ ⊆ I<GOAL>∑ i ∈ I, (ρ i) x₀ = 1
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x y : R<VAR>h : Commute x y<VAR>n : ℕ<VAR>t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)<GOAL>(x + y) ^ n = ∑ m ∈ range (n + 1), t n m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x y : R<VAR>h : Commute x y<VAR>n : ℕ<VAR>t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)<VAR>h_first : ∀ (n : ℕ), t n 0 = y ^ n<GOAL>(x + y) ^ n = ∑ m ∈ range (n + 1), t n m
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>x y : R<VAR>h : Commute x y<VAR>n : ℕ<VAR>t : ℕ → ℕ → R := fun n m => x ^ m * y ^ (n - m) * ↑(n.choose m)<VAR>h_first : ∀ (n : ℕ), t n 0 = y ^ n<VAR>h_last : ∀ (n : ℕ), t n n.succ = 0<GOAL>(x + y) ^ n = ∑ m ∈ range (n + 1), t n m