ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>Q : Type v<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>inj : CategoryTheory.Injective (ModuleCat.of R Q)<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>f : X →ₗ[R] Y<VAR>hf : Function.Injective ⇑f<VAR>g : X →ₗ[R] Q<VAR>this : CategoryTheory.Mono (ModuleCat.ofHom f)<GOAL>∃ h, ∀ (x : X), h (f x) = g x
<VAR>R : Type u<VAR>inst✝² : Ring R<VAR>Q : Type v<VAR>inst✝¹ : AddCommGroup Q<VAR>inst✝ : Module R Q<VAR>inj : CategoryTheory.Injective (ModuleCat.of R Q)<VAR>X Y : Type v<VAR>x✝³ : AddCommGroup X<VAR>x✝² : AddCommGroup Y<VAR>x✝¹ : Module R X<VAR>x✝ : Module R Y<VAR>f : X →ₗ[R] Y<VAR>hf : Function.Injective ⇑f<VAR>this : CategoryTheory.Mono (ModuleCat.ofHom f)<VAR>l : ModuleCat.of R Y ⟶ ModuleCat.of R Q<GOAL>∃ h, ∀ (x : X), h (f x) = (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom f) l) x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>IsLocallySurjective J f ↔ Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A))) = ⊤
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<GOAL>IsLocallySurjective J f ↔ ∀ (a : Cᵒᵖ) (x : (G ⋙ forget A).obj a), x ∈ (Subpresheaf.sheafify J (imagePresheaf (whiskerRight f (forget A)))).obj a
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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>inst✝ : StrongRankCondition R<VAR>s : Set M<GOAL>Module.rank R ↥(span R s) ≤ #↑s
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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>inst✝ : StrongRankCondition R<VAR>s : Set M<GOAL>lift.{?u.585050, v} (Module.rank R ↥(LinearMap.range (Finsupp.total (↑s) M R Subtype.val))) ≤ lift.{?u.585050, v} #↑s
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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>inst✝ : StrongRankCondition R<VAR>s : Set M<GOAL>lift.{v, max u v} (Module.rank R (↑s →₀ R)) ≤ lift.{max u v, v} #↑s
<VAR>R S : Type u<VAR>M : Type v<VAR>M' : Type v'<VAR>M₁ : Type v<VAR>ι : Type w<VAR>ι' : Type w'<VAR>η : Type u₁'<VAR>φ : η → Type u_1<VAR>inst✝⁸ : Ring R<VAR>inst✝⁷ : CommRing S<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>inst✝ : StrongRankCondition R<VAR>s : Set M<GOAL>lift.{v, max u v} (lift.{u, v} #↑s) ≤ lift.{max u v, v} #↑s
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : t ∈ 𝓝[s] x<GOAL>HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'
<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>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>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 f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : t ∈ 𝓝[s] x<GOAL>↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace X'<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Y'<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace Z'<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>inst✝ : Nonempty X<VAR>x : X<GOAL>↑(toPartialHomeomorph f h).symm (f x) = x
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁶ : TopologicalSpace X<VAR>inst✝⁵ : TopologicalSpace X'<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Y'<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace Z'<VAR>f : X → Y<VAR>h : OpenEmbedding f<VAR>inst✝ : Nonempty X<VAR>x : X<GOAL>x ∈ (toPartialHomeomorph f h).source
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CommGroup β<VAR>s : Set α<VAR>t u : Finset α<VAR>d : ℕ<VAR>a : α<GOAL>MulDissociated {a} ↔ a ≠ 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : N →* G<VAR>x : N<GOAL>x ∈ comap f H.normalizer → x ∈ (comap f H).normalizer
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>H K : Subgroup G<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : N →* G<VAR>x : N<GOAL>(∀ (h : G), h ∈ H ↔ f x * h * (f x)⁻¹ ∈ H) → ∀ (h : N), f h ∈ H ↔ f (x * h * x⁻¹) ∈ H
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : N.FG<VAR>hin : N ≤ I • N<GOAL>∃ r ∈ I, ∀ n ∈ N, r • n = n
<VAR>R✝ : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝⁵ : Semiring R✝<VAR>inst✝⁴ : AddCommMonoid M✝<VAR>inst✝³ : Module R✝ M✝<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>M : Type u_4<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>N : Submodule R M<VAR>hn : N.FG<VAR>hin : N ≤ I • N<VAR>r : R<VAR>hr : r - 1 ∈ I<VAR>hr' : ∀ n ∈ N, r • n = 0<GOAL>∃ r ∈ I, ∀ n ∈ N, r • n = n
<VAR>m n : ℕ<GOAL>↑m ≤ ↑n ↔ m ≤ n
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ∠ p₁ p₂ p₃ = π / 2<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₁ ≠ p₂ ∨ p₃ = p₂<GOAL>dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>p₁ p₂ p₃ : P<VAR>h : ⟪p₂ -ᵥ p₃, p₁ -ᵥ p₂⟫_ℝ = 0<VAR>h0 : p₂ -ᵥ p₃ = 0 ∨ p₁ -ᵥ p₂ ≠ 0<GOAL>dist p₁ p₂ / Real.tan (∠ p₂ p₃ p₁) = dist p₃ p₂
<VAR>R : Type u<VAR>inst✝⁵ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type v<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>T : Type u_1<VAR>inst✝² : CommSemiring T<VAR>inst✝¹ : Algebra R T<VAR>inst✝ : IsLocalization S T<VAR>r : R<VAR>s : ↥S<VAR>m : M<GOAL>r • mk m s = mk (r • m) s
<VAR>R✝ : Type u<VAR>S : Type v<VAR>a b : R✝<VAR>n m : ℕ<VAR>inst✝⁵ : Semiring R✝<VAR>p✝ q r : R✝[X]<VAR>R : Type u_1<VAR>A : Type u_2<VAR>M : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R A<VAR>inst✝ : Module R M<VAR>f : ℕ → A →ₗ[R] M<VAR>c : R<VAR>p : A[X]<GOAL>∑ n ∈ p.support, (f n) ((c • p).coeff n) = (RingHom.id R) c • p.sum fun x x_1 => (f x) x_1
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>h : X ≃ₜ Y<VAR>s : Set X<GOAL>IsClosed (⇑h '' s) ↔ IsClosed s
<VAR>X Y : SimplexCategory<VAR>x✝ : IsIsomorphic X Y<VAR>I : X ≅ Y<GOAL>Fintype.card (Fin (X.len + 1)) = Fintype.card (Fin (Y.len + 1))
<VAR>X Y : SimplexCategory<VAR>x✝ : IsIsomorphic X Y<VAR>I : X ≅ Y<GOAL>Fin (X.len + 1) ≃ Fin (Y.len + 1)
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>I J K L : Ideal R<VAR>inst✝ : IsDomain R<VAR>x : R<VAR>hx : x ≠ 0<GOAL>span {x} * I = span {x} * J ↔ I = J
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>h : p.divX = 0<GOAL>p = C (p.coeff 0)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>h : p = C (p.coeff 0)<GOAL>p.divX = 0
<VAR>m n k : ℕ<GOAL>(m + n * k).gcd n = m.gcd n
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>HasSum (fun n => 1 / ↑n ^ (2 * k)) ((-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)!)
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>(fun n => 1 / ↑n ^ (2 * k)) = fun n => 1 / ↑n ^ (2 * k) * Real.cos (2 * π * ↑n * 0)
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>(-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! = (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * Polynomial.eval 0 (Polynomial.map (algebraMap ℚ ℝ) (Polynomial.bernoulli (2 * k)))
<VAR>k : ℕ<VAR>hk : k ≠ 0<GOAL>(-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! = (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2<GOAL>(-1) ^ (k + 1) * 2 ^ (2 * k - 1) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! = (-1) ^ (k + 1) * (2 * π) ^ (2 * k) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
<VAR>k : ℕ<VAR>hk : k ≠ 0<VAR>this : 2 ^ (2 * k - 1) = 2 ^ (2 * k) / 2<GOAL>(-1) ^ (k + 1) * (2 ^ (2 * k) / 2) * π ^ (2 * k) * ↑(bernoulli (2 * k)) / ↑(2 * k)! = (-1) ^ (k + 1) * (2 ^ (2 * k) * π ^ (2 * k)) / 2 / ↑(2 * k)! * ↑(bernoulli (2 * k))
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<GOAL>0 ≤ a ^ 2
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>0 ≤ a ^ 2
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a ≤ 0<GOAL>0 ≤ a ^ 2
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a ≤ 0<VAR>b : α<VAR>hab : 0 = a + b<GOAL>0 ≤ a ^ 2
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : LinearOrder α<VAR>a✝ b✝ c d : α<VAR>inst✝⁴ : IsRightCancelAdd α<VAR>inst✝³ : ZeroLEOneClass α<VAR>inst✝² : ExistsAddOfLE α<VAR>inst✝¹ : PosMulMono α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>a : α<VAR>ha : a ≤ 0<VAR>b : α<VAR>hab : 0 = a + b<GOAL>(fun x => x + a * b) (b ^ 2) = (fun x => x + a * b) (a ^ 2)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (id '' s)
<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 α<GOAL>f =O[l] g ↔ ∃ c, ∀ᶠ (x : α) in l, ‖f x‖ ≤ c * ‖g x‖
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>this : IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔ IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi (a * 0)) volume<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>this : IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔ IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>this : IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔ IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume<VAR>h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → E<VAR>s : ℂ<VAR>a : ℝ<VAR>ha : 0 < a<VAR>this : IntegrableOn (fun x => (fun t => ↑t ^ (s - 1) • f t) (a * x)) (Ioi 0) volume ↔ IntegrableOn (fun t => ↑t ^ (s - 1) • f t) (Ioi 0) volume<VAR>h1 : EqOn (fun t => ↑(a * t) ^ (s - 1) • f (a * t)) (↑a ^ (s - 1) • fun t => ↑t ^ (s - 1) • f (a * t)) (Ioi 0)<VAR>h2 : ↑a ^ (s - 1) ≠ 0<GOAL>MellinConvergent (fun t => f (a * t)) s ↔ MellinConvergent f s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(𝓤 α).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : UniformGroup α<VAR>ι : Sort u_3<VAR>p : ι → Prop<VAR>U : ι → Set α<VAR>h : (𝓝 1).HasBasis p U<GOAL>(Filter.comap (fun x => x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<GOAL>(s + 1).partialGamma X = s * s.partialGamma X - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : ∫ (y : ℝ) in 0 ..X, -(↑(rexp (-y)) * ↑y ^ s) + ↑(rexp (-y)) * (s * ↑y ^ (s - 1)) = (ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : -∫ (y : ℝ) in 0 ..X, -(↑(rexp (-y)) * ↑y ^ s) + ↑(rexp (-y)) * (s * ↑y ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<GOAL>∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<GOAL>(∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) + (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s - (ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)<GOAL>(∫ (x : ℝ) in 0 ..X, s * ↑(rexp (-x)) * ↑x ^ (s - 1)) + (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s - (ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s
<VAR>s : ℂ<VAR>hs : 0 < s.re<VAR>X : ℝ<VAR>hX : 0 ≤ X<VAR>F_der_I : ∀ x ∈ Ioo 0 X, HasDerivAt (fun x => ↑(rexp (-x)) * ↑x ^ s) (-(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) x<VAR>cont : Continuous fun x => (ofReal' ∘ fun y => rexp (-y)) x * ↑x ^ s<VAR>der_ible : IntervalIntegrable (fun x => -(↑(rexp (-x)) * ↑x ^ s) + ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) volume 0 X<VAR>int_eval : (∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ s) + -∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * (s * ↑x ^ (s - 1)) = -((ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s - (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s)<VAR>this : (fun x => ↑(rexp (-x)) * (s * ↑x ^ (s - 1))) = fun x => s * ↑(rexp (-x)) * ↑x ^ (s - 1)<VAR>t : ∫ (x : ℝ) in 0 ..X, s * (↑(rexp (-x)) * ↑x ^ (s - 1)) = s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)<GOAL>(∫ (x : ℝ) in 0 ..X, s * ↑(rexp (-x)) * ↑x ^ (s - 1)) + (ofReal' ∘ fun y => rexp (-y)) 0 * ↑0 ^ s - (ofReal' ∘ fun y => rexp (-y)) X * ↑X ^ s = (s * ∫ (x : ℝ) in 0 ..X, ↑(rexp (-x)) * ↑x ^ (s - 1)) - ↑(rexp (-X)) * ↑X ^ s