ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M₂ : Type u_3<VAR>M₃ : Type u_4<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M₂<VAR>inst✝³ : AddCommGroup M₃<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M₂<VAR>inst✝ : Module R M₃<VAR>f : M →ₗ[R] M₂<VAR>p p' : Submodule R M<VAR>x : ↥(p ⊔ p')<GOAL>Submodule.Quotient.mk x = (quotientInfEquivSupQuotient p p') 0 ↔ ↑x ∈ p'
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : IsDomain A<VAR>K : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>x * IsFractionRing.inv A x = 1
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : IsDomain A<VAR>K : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>x * (mk' K ↑(sec (nonZeroDivisors A) x).2 ⟨(sec (nonZeroDivisors A) x).1, ⋯⟩ * (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) = (algebraMap A K) ↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩
<VAR>R : Type u_1<VAR>inst✝¹⁰ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁹ : CommRing S<VAR>inst✝⁸ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁷ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : IsDomain A<VAR>K : Type u_5<VAR>inst✝⁴ : CommRing K<VAR>inst✝³ : Algebra R K<VAR>inst✝² : IsFractionRing R K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>x : K<VAR>hx : x ≠ 0<GOAL>x = mk' K (↑⟨(sec (nonZeroDivisors A) x).1, ⋯⟩) (sec (nonZeroDivisors A) x).2
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<GOAL>(𝓝 x).HasBasis (fun r => 0 < r) (closedBall x)
<VAR>E : Type u_1<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : TopologicalSpace E<VAR>inst✝⁴ : TopologicalAddGroup E<VAR>inst✝³ : T2Space E<VAR>inst✝² : Module ℝ E<VAR>inst✝¹ : ContinuousSMul ℝ E<VAR>inst✝ : FiniteDimensional ℝ E<VAR>x : E<GOAL>(Filter.comap (⇑toEuclidean.toHomeomorph) (𝓝 (toEuclidean.toHomeomorph x))).HasBasis (fun r => 0 < r) (closedBall x)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝² : Semiring R<VAR>p q r : R[X]<VAR>inst✝¹ : Semiring S<VAR>f : R →+* S<VAR>inst✝ : Semiring T<VAR>g : S →+* T<VAR>x : T<GOAL>eval₂ g x (map f p) = eval₂ (g.comp f) x p
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>(o.oangle x (x + y)).tan * ‖x‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<VAR>hs : (o.oangle x (x + y)).sign = 1<GOAL>(o.oangle x (x + y)).tan * ‖x‖ = ‖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>a : R<VAR>b : ↥M<VAR>c : R<GOAL>mk a b + mk c b = mk (a + c) b
<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>a : R<VAR>b : ↥M<VAR>c : R<GOAL>(r' M) (↑b * c + ↑b * a, b * b) (a + c, b)
<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>a : R<VAR>b : ↥M<VAR>c : R<GOAL>↑1 * (↑(↑b * c + ↑b * a, b * b).2 * (a + c, b).1) = ↑1 * (↑(a + c, b).2 * (↑b * c + ↑b * a, b * b).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>a : R<VAR>b : ↥M<VAR>c : R<GOAL>1 * (↑b * ↑b * (a + c)) = 1 * (↑b * (↑b * c + ↑b * a))
<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 : ℕ∞<GOAL>ContMDiff I I' n f ↔ Continuous f ∧ ∀ (x : M) (y : M'), ContDiffOn 𝕜 n (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (f ⁻¹' (extChartAt I' y).source))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>obs : ∀ (x : ℝ), ∫ (t : ℝ) in 0 ..x, t ^ (p - 1) = x ^ p / p<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ENNReal.ofReal p * ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)<GOAL>∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ = ∫⁻ (a : α), ENNReal.ofReal p * ENNReal.ofReal (f a ^ p / p) ∂μ
<VAR>α : Type u_1<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℝ<VAR>μ : Measure α<VAR>f_nn : 0 ≤ᶠ[ae μ] f<VAR>f_mble : AEMeasurable f μ<VAR>p : ℝ<VAR>p_pos : 0 < p<VAR>one_lt_p : -1 < p - 1<VAR>g : ℝ → ℝ := fun t => t ^ (p - 1)<VAR>obs : ∀ (x : ℝ), intervalIntegral g 0 x volume = x ^ p / p<VAR>g_nn : ∀ᵐ (t : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ g t<VAR>g_intble : ∀ t > 0, IntervalIntegrable g volume 0 t<VAR>key : ∫⁻ (ω : α), ENNReal.ofReal (∫ (t : ℝ) in 0 ..f ω, g t) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (g t)<GOAL>AEMeasurable (fun ω => ENNReal.ofReal (f ω ^ p / p)) μ
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>im ⟪x, y⟫_𝕜 = (‖x - I • y‖ * ‖x - I • y‖ - ‖x + I • y‖ * ‖x + I • y‖) / 4
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : E<GOAL>im ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ - 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖ - (‖x‖ * ‖x‖ + 2 * -im ⟪x, y⟫_𝕜 + ‖I • y‖ * ‖I • y‖)) / 4
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>p : ↑(PrimeSpectrum.Top R)<VAR>hpU : p ∈ U.carrier<GOAL>p ∈ ⇑(PrimeSpectrum.comap (RingHom.id R)) ⁻¹' U.carrier
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U : Opens ↑(PrimeSpectrum.Top R)<GOAL>comap (RingHom.id R) U U ⋯ = RingHom.id ↑((structureSheaf R).val.obj (op U))
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>S : Type u<VAR>inst✝¹ : CommRing S<VAR>P : Type u<VAR>inst✝ : CommRing P<VAR>U : Opens ↑(PrimeSpectrum.Top R)<GOAL>eqToHom ⋯ = RingHom.id ↑((structureSheaf R).val.obj (op U))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>s : Set ι<GOAL>span 𝕜 (gramSchmidtNormed 𝕜 f '' s) = span 𝕜 (gramSchmidt 𝕜 f '' s)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>gramSchmidt 𝕜 f i ∈ span 𝕜 (gramSchmidtNormed 𝕜 f '' ↑{i})
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁵ : RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝² : LinearOrder ι<VAR>inst✝¹ : LocallyFiniteOrderBot ι<VAR>inst✝ : IsWellOrder ι fun x x_1 => x < x_1<VAR>f : ι → E<VAR>s : Set ι<VAR>i : ι<VAR>hi : i ∈ s<GOAL>gramSchmidt 𝕜 f i ∈ span 𝕜 {gramSchmidtNormed 𝕜 f i}
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H✝ : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>H : Type u_4<VAR>F : Type u_5<VAR>inst✝⁶ : CommSemiring k<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : Algebra k A<VAR>inst✝³ : AddMonoid G<VAR>inst✝² : AddMonoid H<VAR>inst✝¹ : FunLike F G H<VAR>inst✝ : AddMonoidHomClass F G H<VAR>f : F<VAR>r : k<GOAL>mapDomain (⇑f) ((algebraMap k A[G]) r) = (algebraMap k A[H]) r
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝² : NormedLinearOrderedField K<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace K E<VAR>b : Basis ι K E<VAR>ι' : Type u_4<VAR>e : ι ≃ ι'<VAR>x✝ : E<GOAL>x✝ ∈ fundamentalDomain (b.reindex e) ↔ x✝ ∈ fundamentalDomain b
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝² : NormedLinearOrderedField K<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace K E<VAR>b : Basis ι K E<VAR>ι' : Type u_4<VAR>e : ι ≃ ι'<VAR>x✝ : E<GOAL>(∀ (i : ι'), (b.repr x✝) (e.symm i) ∈ Set.Ico 0 1) ↔ ∀ (i : ι), (b.repr x✝) i ∈ Set.Ico 0 1
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>K : Type u_3<VAR>inst✝² : NormedLinearOrderedField K<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace K E<VAR>b : Basis ι K E<VAR>ι' : Type u_4<VAR>e : ι ≃ ι'<VAR>x✝ : E<GOAL>∀ (b_1 : ι'), (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1 ↔ (b.repr x✝) (e.symm b_1) ∈ Set.Ico 0 1
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>(α_ X Y Z).inv ≫ fst (X ⊗ Y) Z ≫ fst X Y = fst X (Y ⊗ Z)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : ChosenFiniteProducts C<VAR>X Y Z : C<GOAL>Limits.BinaryFan.fst (product X (product Y Z).cone.pt).cone = fst X (Y ⊗ Z)
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>x ∈ antidiagonal n ↔ x.1 + x.2 = n
<VAR>n : ℕ<VAR>x : ℕ × ℕ<GOAL>(∃ a ∈ range (n + 1), (a, n - a) = x) ↔ x.1 + x.2 = n
<VAR>α : Type u_1<GOAL>comap Real.toNNReal atTop = atTop
<VAR>α : Type u_1<GOAL>comap Real.toNNReal atTop ≤ atTop
<VAR>α : Type u_1<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>Set.Ioi a ∈ comap Real.toNNReal atTop
<VAR>α : Type u_1<VAR>a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<VAR>hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal<GOAL>x ∈ Set.Ioi a
<VAR>G : Type u_1<VAR>inst✝³ : Group G<VAR>A B : Subgroup G<VAR>φ : ↥A ≃* ↥B<VAR>H : Type u_2<VAR>inst✝² : Group H<VAR>M : Type u_3<VAR>inst✝¹ : Monoid M<VAR>d : TransversalPair G A B<VAR>inst✝ : DecidableEq G<VAR>g : G<VAR>w : NormalWord d<GOAL>ReducedWord.prod φ (g • w).toReducedWord = of g * ReducedWord.prod φ w.toReducedWord
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t✝ u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s t : Finset α<GOAL>(t \ (s ∩ t)).card ≤ (t \ s).card
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β = chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β ≤ chainLength α β
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα✝ : α.IsNonZero<VAR>hα : ¬α.IsZero<GOAL>chainLength α β ≤ chainBotCoeff (⇑α) β + chainTopCoeff (⇑α) β
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>HasSum (fun n => (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2) (hurwitzZetaEven (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>(1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2 = 1 / ↑|↑↑n + a| ^ s / 2 + 1 / ↑|↑(-(↑n + 1)) + a| ^ s / 2
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → R<GOAL>trop (∑ i ∈ s, f i) = ∏ i ∈ s, trop (f i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → R<GOAL>∏ i ∈ s, trop (f i) = (Multiset.map trop (Multiset.map f s.val)).prod
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝ : AddCommMonoid R<VAR>s : Finset S<VAR>f : S → R<GOAL>∏ i ∈ s, trop (f i) = (Multiset.map (fun i => trop (f i)) s.val).prod
<VAR>Ω : Type u_1<VAR>inst✝¹ : Nonempty Ω<VAR>m0 : MeasurableSpace Ω<VAR>μ : FiniteMeasure Ω<VAR>inst✝ : TopologicalSpace Ω<VAR>nonzero : μ ≠ 0<VAR>f : Ω →ᵇ ℝ≥0<GOAL>μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f✝ : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f✝ = 0<VAR>inst✝ : Algebra R S<VAR>f : R[X]<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>liftHom f (ϕ (root f)) ⋯ = ϕ
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f✝ : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f✝ = 0<VAR>inst✝ : Algebra R S<VAR>f : R[X]<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯) = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝² : CommRing R<VAR>f✝ : R[X]<VAR>inst✝¹ : CommRing S<VAR>i : R →+* S<VAR>a : S<VAR>h : eval₂ i a f✝ = 0<VAR>inst✝ : Algebra R S<VAR>f : R[X]<VAR>ϕ : AdjoinRoot f →ₐ[R] S<GOAL>root f ∈ ↑(AlgHom.equalizer ϕ (liftHom f (ϕ (root f)) ⋯))
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r : S<VAR>x : R<VAR>hx : x ∈ ⇑(Algebra.norm R) '' ↑(span {r})<GOAL>(Algebra.norm R) r ∣ x
<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>r x : S<VAR>hx' : x ∈ ↑(span {r})<VAR>hx : (Algebra.norm R) x ∈ ⇑(Algebra.norm R) '' ↑(span {r})<GOAL>(Algebra.norm R) r ∣ (Algebra.norm R) x
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>x : Completion G<GOAL>(id G).completion x = (id (Completion G)) x
<VAR>G : Type u_1<VAR>inst✝² : SeminormedAddCommGroup G<VAR>H : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup H<VAR>K : Type u_3<VAR>inst✝ : SeminormedAddCommGroup K<VAR>x : Completion G<GOAL>_root_.id x = (id (Completion G)) 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>I : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>J : Submodule R P<VAR>b : P<VAR>hb : b ∈ I ⊓ J<GOAL>IsInteger R (aI • b)
<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>I : Submodule R P<VAR>aI : R<VAR>haI : aI ∈ S<VAR>hI : ∀ b ∈ I, IsInteger R (aI • b)<VAR>J : Submodule R P<VAR>b : P<VAR>hb : b ∈ I ⊓ J<VAR>hbI : b ∈ I<VAR>right✝ : b ∈ J<GOAL>IsInteger R (aI • b)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : y ≤ x<VAR>u : ℕ → α := fun n => if n = 0 then y else x<GOAL>edist (f x) (f y) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : y ≤ x<VAR>u : ℕ → α := fun n => if n = 0 then y else x<VAR>hu : Monotone u<GOAL>edist (f x) (f y) ≤ eVariationOn f s
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>x y : α<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : y ≤ x<VAR>u : ℕ → α := fun n => if n = 0 then y else x<VAR>hu : Monotone u<VAR>us : ∀ (i : ℕ), u i ∈ s<GOAL>edist (f x) (f y) ≤ eVariationOn f s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>h : 4 ≠ 0<GOAL>W.Ψ₂Sq.coeff 3 ≠ 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>u v : R<GOAL>![((u * v) ^ 2) ^ 2 * W'.addX P Q, ((u * v) ^ 2) ^ 3 * W'.addY P Q, (u * v) ^ 2 * addZ P Q] = (u * v) ^ 2 • W'.addXYZ P Q
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>(M ↾ R).Dep X ↔ ¬M.Indep X ∧ X ⊆ R
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>R I J X Y : Set α<GOAL>¬(M.Indep X ∧ X ⊆ R) ∧ X ⊆ R ↔ ¬M.Indep X ∧ X ⊆ R
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<GOAL>(cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>hf : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g✝ (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g✝ 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>a : A<VAR>g : R → R<VAR>ha : p a<VAR>f : C(↑(σₙ R a), R)₀<VAR>h : ⇑f = (σₙ R a).restrict (Function.extend Subtype.val (⇑f) g)<GOAL>(cfcₙHom ha) f = cfcₙ (Function.extend Subtype.val (⇑f) g) a