ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I J : Ideal R<VAR>hIJ : I ≤ J<VAR>x : R<GOAL>(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<GOAL>SameRay R (x -ᵥ x) (y -ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>hx : x ∈ s<GOAL>SameRay R 0 (y -ᵥ x)
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : Summable fun x => ‖term f s x‖<GOAL>∃ C, ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ s.re
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : Summable fun x => ‖term f s x‖<VAR>H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖<GOAL>False
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : Summable fun x => ‖term f s x‖<VAR>H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖<GOAL>False
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : Summable fun x => ‖term f s x‖<VAR>H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖<VAR>this : ‖term f s n‖ ≤ ∑' (i : ℕ), ‖term f s i‖<GOAL>False
<VAR>f : ℕ → ℂ<VAR>s : ℂ<VAR>h : Summable fun x => ‖term f s x‖<VAR>H : ∀ (C : ℝ), ∃ n, n ≠ 0 ∧ C * ↑n ^ s.re < ‖f n‖<VAR>n : ℕ<VAR>hn₀ : n ≠ 0<VAR>hn : (∑' (n : ℕ), ‖term f s n‖) * ↑n ^ s.re < ‖f n‖<VAR>this : ‖f n‖ ≤ (∑' (i : ℕ), ‖term f s i‖) * ↑n ^ s.re<GOAL>False
<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>h : -2 * ↑π ≠ 0<GOAL>HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) ↑(sinKernel (↑a) t)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>h : -2 * ↑π ≠ 0<GOAL>HasSum (fun n => -I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t))) (jacobiTheta₂' (↑a) (I * ↑t) / (-2 * ↑π))
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>h : -2 * ↑π ≠ 0<VAR>n : ℤ<GOAL>-I * ↑n * cexp (2 * ↑π * I * ↑a * ↑n) * ↑(rexp (-π * ↑n ^ 2 * t)) = jacobiTheta₂'_term n (↑a) (I * ↑t) / (-2 * ↑π)
<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>h : -2 * ↑π ≠ 0<VAR>n : ℤ<GOAL>-2 * ↑π * (-I * ↑n) * cexp (2 * ↑π * I * ↑a * ↑n + -↑π * ↑n ^ 2 * ↑t) = 2 * ↑π * I * ↑n * cexp (2 * ↑π * I * ↑n * ↑a + ↑π * I * ↑n ^ 2 * (I * ↑t))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ p : MvPolynomial σ R<GOAL>IsWeightedHomogeneous w p 0 ↔ weightedTotalDegree w p = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ p : MvPolynomial σ R<GOAL>(∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ s ∈ p.support, (weight w) s = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ p : MvPolynomial σ R<GOAL>∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → (weight w) a = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → (weight w) m = 0
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>S : DiscreteQuotient X<VAR>g : C(Y, Z)<VAR>f : C(X, Y)<VAR>A B : DiscreteQuotient Y<VAR>h : A ≤ B<GOAL>comap f A ≤ comap f B
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<GOAL>weightedTotalDegree w p = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<GOAL>(∀ ⦃d : σ →₀ ℕ⦄, coeff d p ≠ 0 → (weight w) d = 0) ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<GOAL>∀ (a : σ →₀ ℕ), coeff a p ≠ 0 → (weight w) a = 0 ↔ a ∈ p.support → ∀ (x : σ), a x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>coeff m p ≠ 0 → (weight w) m = 0 ↔ m ∈ p.support → ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>coeff m p ≠ 0 → (weight w) m = 0 ↔ coeff m p ≠ 0 → ∀ (x : σ), m x = 0
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<GOAL>coeff m p ≠ 0 → ((weight w) m = 0 ↔ ∀ (x : σ), m x = 0)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>σ : Type u_3<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid M<VAR>w : σ → M<VAR>φ : MvPolynomial σ R<VAR>hw : NonTorsionWeight w<VAR>p : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>a✝ : coeff m p ≠ 0<GOAL>(weight w) m = 0 ↔ ∀ (x : σ), m x = 0
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>S : Set (HeightOneSpectrum R)<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x✝ : Kˣ<GOAL>x✝ ∈ {x | ∀ v ∉ S, v.valuation ↑x = 1} ↔ x✝ ∈ ↑(⨅ v, ⨅ (_ : v ∉ S), v.valuation.valuationSubring.unitGroup)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hfm : StronglyMeasurableAtFilter f l μ<VAR>hμ : μ.FiniteAtFilter l<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>C : ℝ<VAR>hC : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hfm✝ : StronglyMeasurableAtFilter f l μ<VAR>hμ✝ : μ.FiniteAtFilter l<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>C : ℝ<VAR>hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>hμ : μ s < ⊤<VAR>hC : ∀ x ∈ s, ‖f x‖ ≤ C<GOAL>IntegrableAtFilter f l μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hfm✝ : StronglyMeasurableAtFilter f l μ<VAR>hμ✝ : μ.FiniteAtFilter l<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>C : ℝ<VAR>hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>hμ : μ s < ⊤<VAR>hC : ∀ x ∈ s, ‖f x‖ ≤ C<GOAL>∀ᵐ (x : α) ∂μ.restrict s, ‖f x‖ ≤ C
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s✝ t : Set α<VAR>μ ν : Measure α<VAR>l✝ l' l : Filter α<VAR>inst✝ : l.IsMeasurablyGenerated<VAR>hfm✝ : StronglyMeasurableAtFilter f l μ<VAR>hμ✝ : μ.FiniteAtFilter l<VAR>hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f)<VAR>C : ℝ<VAR>hC✝ : ∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, ‖f x‖ ≤ C<VAR>s : Set α<VAR>hsl : s ∈ l<VAR>hsm : MeasurableSet s<VAR>hfm : AEStronglyMeasurable f (μ.restrict s)<VAR>hμ : μ s < ⊤<VAR>hC : ∀ x ∈ s, ‖f x‖ ≤ C<GOAL>∀ᵐ (x : α) ∂μ, x ∈ s → ‖f x‖ ≤ C
<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>IsClopen s ↔ frontier s = ∅
<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>closure s = s ∧ interior s = s ↔ closure s ⊆ interior s
<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<VAR>h : closure s ⊆ interior s<GOAL>closure s = s ∧ interior s = s
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>s : Set A<GOAL>centralizer R s.centralizer.centralizer = centralizer R s
<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝⁴ : CommSemiring R<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra R B<VAR>S : Subalgebra R A<VAR>s : Set A<GOAL>↑(centralizer R s.centralizer.centralizer) = ↑(centralizer R s)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>hg : Differentiable 𝕜 g<GOAL>(Differentiable 𝕜 fun y => f y - g y) ↔ Differentiable 𝕜 f
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : Preadditive C<VAR>X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<VAR>T U : C<VAR>f : T ⟶ X<VAR>g : T ⟶ Y<VAR>h : X ⟶ U<VAR>i : Y ⟶ U<GOAL>lift f g ≫ desc h i = f ≫ h + g ≫ i
<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 + m • p) b = toIcoMod hp a b + m • p
<VAR>q a b c : ℚ<GOAL>0 + a = a
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>↑(ℜ (I • a)) = ↑(-ℑ a)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<GOAL>(pmap f l h).get? n = Option.pmap f (l.get? n) ⋯
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>l : List α<VAR>h : ∀ (a : α), a ∈ l → p a<VAR>n : ℕ<GOAL>(pmap f l h)[n]? = Option.pmap f l[n]? ⋯
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type x<VAR>inst✝³ : DecidableEq α<VAR>inst✝² : DecidableEq β<VAR>inst✝¹ : DecidableEq γ<VAR>inst✝ : Subsingleton α<VAR>a b i j : α<GOAL>(j ∈ if i = a then some b else none) ↔ j ∈ some i
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>c : ℝ<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<GOAL>mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * mixedEmbedding.norm x
<VAR>α β : Sort u<VAR>inst✝ : FastSubsingleton α<VAR>h₂ : α = β<VAR>a : α<VAR>b : β<GOAL>HEq a b
<VAR>α β : Sort u<VAR>inst✝ : FastSubsingleton α<VAR>h₂ : α = β<VAR>a : α<VAR>b : β<VAR>this : Subsingleton α<GOAL>HEq a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>f : α → β<VAR>h : ∀ (s : Set β), IsCompact s → IsCompact (f ⁻¹' s)<VAR>s : Set β<VAR>hs : s ∈ cocompact β<VAR>t : Set β<VAR>ht : IsCompact t<VAR>hts : tᶜ ⊆ s<GOAL>(f ⁻¹' t)ᶜ ⊆ f ⁻¹' s
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<GOAL>((aeval f) F).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<GOAL>(Finsupp.sum F fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<GOAL>fold max 0 (natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) F.support ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<GOAL>(natDegree ∘ fun i => (fun s a => (algebraMap R R[X]) a * s.prod fun n e => f n ^ e) i (F i)) d ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<GOAL>(Polynomial.C (F d) * d.prod fun n e => f n ^ e).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<GOAL>(d.prod fun n e => f n ^ e).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<GOAL>∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<VAR>this : ∑ i ∈ d.support, d i * n ≤ m * n<GOAL>∑ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ m * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<VAR>this : ∑ i ∈ d.support, d i * n ≤ m * n<GOAL>∀ i ∈ d.support, ((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<VAR>this : ∑ i ∈ d.support, d i * n ≤ m * n<VAR>i : σ<GOAL>((fun n e => f n ^ e) i (d i)).natDegree ≤ d i * n
<VAR>R✝ : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R✝<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R✝ M<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>m n : ℕ<VAR>F : MvPolynomial σ R<VAR>hF : F.totalDegree ≤ m<VAR>f : σ → R[X]<VAR>hf : ∀ (i : σ), (f i).natDegree ≤ n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ F.support<VAR>this : ∑ i ∈ d.support, d i * n ≤ m * n<VAR>i : σ<GOAL>d i * (f i).natDegree ≤ d i * n
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasGradientAt g g' u<GOAL>HasDerivAt g ((starRingEnd 𝕜) g') u
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>g : 𝕜 → 𝕜<VAR>g' u : 𝕜<VAR>L' : Filter 𝕜<VAR>h : HasDerivAt g (((toDual 𝕜 𝕜) g') 1) u<GOAL>HasDerivAt g ((starRingEnd 𝕜) g') u
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, 0 ≤ x<GOAL>0 ≤ sInf S
<VAR>hS : ∀ x ∈ ∅, 0 ≤ x<GOAL>0 ≤ sInf ∅
<VAR>S : Set ℝ<VAR>hS : ∀ x ∈ S, 0 ≤ x<VAR>hS₂ : S.Nonempty<GOAL>0 ≤ sInf S
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x : α<VAR>s : Set G<VAR>hs : s ∈ 𝓝 1<GOAL>∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalGroup G<VAR>inst✝ : TopologicalSpace α<VAR>f : α → G<VAR>s✝ : Set α<VAR>x : α<VAR>s : Set G<VAR>hs : s ∈ 𝓝 1<VAR>this : (fun p => p.1 * p.2⁻¹) ⁻¹' s ∈ 𝓝 (1, 1)<GOAL>∃ V ∈ 𝓝 1, ∀ v ∈ V, ∀ w ∈ V, v / w ∈ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u✝ : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m₁ : α → γ → α'<VAR>m₂ : β → γ → β'<VAR>n' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)<VAR>s : Set ε<VAR>t₁ : Set α'<VAR>u : Set α<VAR>hu : u ∈ f<VAR>w₁ : Set γ<VAR>hw₁ : w₁ ∈ h<VAR>ht₁ : image2 m₁ u w₁ ⊆ t₁<VAR>t₂ : Set β'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>v : Set β<VAR>hv : v ∈ g<VAR>w₂ : Set γ<VAR>hw₂ : w₂ ∈ h<VAR>ht₂ : image2 m₂ v w₂ ⊆ t₂<GOAL>s ∈ map₂ m (map₂ n f g) h
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u✝ : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m₁ : α → γ → α'<VAR>m₂ : β → γ → β'<VAR>n' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)<VAR>s : Set ε<VAR>t₁ : Set α'<VAR>u : Set α<VAR>hu : u ∈ f<VAR>w₁ : Set γ<VAR>hw₁ : w₁ ∈ h<VAR>ht₁ : image2 m₁ u w₁ ⊆ t₁<VAR>t₂ : Set β'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>v : Set β<VAR>hv : v ∈ g<VAR>w₂ : Set γ<VAR>hw₂ : w₂ ∈ h<VAR>ht₂ : image2 m₂ v w₂ ⊆ t₂<GOAL>image2 m (image2 n u v) (w₁ ∩ w₂) ⊆ s
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u✝ : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m₁ : α → γ → α'<VAR>m₂ : β → γ → β'<VAR>n' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)<VAR>s : Set ε<VAR>t₁ : Set α'<VAR>u : Set α<VAR>hu : u ∈ f<VAR>w₁ : Set γ<VAR>hw₁ : w₁ ∈ h<VAR>ht₁ : image2 m₁ u w₁ ⊆ t₁<VAR>t₂ : Set β'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>v : Set β<VAR>hv : v ∈ g<VAR>w₂ : Set γ<VAR>hw₂ : w₂ ∈ h<VAR>ht₂ : image2 m₂ v w₂ ⊆ t₂<GOAL>image2 m₁ u (w₁ ∩ w₂) ⊆ t₁
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m✝ : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s✝ s₁ s₂ : Set α<VAR>t t₁✝ t₂✝ : Set β<VAR>u✝ : Set γ<VAR>v✝ : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>m : δ → γ → ε<VAR>n : α → β → δ<VAR>m₁ : α → γ → α'<VAR>m₂ : β → γ → β'<VAR>n' : α' → β' → ε<VAR>h_distrib : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m₁ a c) (m₂ b c)<VAR>s : Set ε<VAR>t₁ : Set α'<VAR>u : Set α<VAR>hu : u ∈ f<VAR>w₁ : Set γ<VAR>hw₁ : w₁ ∈ h<VAR>ht₁ : image2 m₁ u w₁ ⊆ t₁<VAR>t₂ : Set β'<VAR>hs : image2 n' t₁ t₂ ⊆ s<VAR>v : Set β<VAR>hv : v ∈ g<VAR>w₂ : Set γ<VAR>hw₂ : w₂ ∈ h<VAR>ht₂ : image2 m₂ v w₂ ⊆ t₂<GOAL>image2 m₂ v (w₁ ∩ w₂) ⊆ t₂
<VAR>m n k : ℕ+<VAR>h : k.Coprime n<GOAL>(k * m).gcd n = m.gcd n
<VAR>m n k : ℕ+<VAR>h : k.Coprime n<GOAL>↑((k * m).gcd n) = ↑(m.gcd n)
<VAR>m n k : ℕ+<VAR>h : k.Coprime n<GOAL>(↑k * ↑m).gcd ↑n = (↑m).gcd ↑n
<VAR>m n k : ℕ+<VAR>h : k.Coprime n<GOAL>(↑k).Coprime ↑n
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<VAR>hb : Isometry Subtype.val<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<VAR>hb : Isometry Subtype.val<VAR>A : dist p q = hausdorffDist ↑p ↑q<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<VAR>hb : Isometry Subtype.val<VAR>A : dist p q = hausdorffDist ↑p ↑q<VAR>I : ↑p = range Subtype.val<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q
<VAR>X : Type u<VAR>inst✝ : MetricSpace X<VAR>p q : NonemptyCompacts X<VAR>ha : Isometry Subtype.val<VAR>hb : Isometry Subtype.val<VAR>A : dist p q = hausdorffDist ↑p ↑q<VAR>I : ↑p = range Subtype.val<VAR>J : ↑q = range Subtype.val<GOAL>dist p.toGHSpace q.toGHSpace ≤ dist p q