ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : S<VAR>s : ↥S⁰<GOAL>IsIntegral K (mk' L x s)
<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>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : S<VAR>s : ↥S⁰<GOAL>IsIntegral K ((algebraMap S L) x * mk' L 1 s)
<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>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : S<VAR>s : ↥S⁰<GOAL>(algebraMap K L).IsIntegralElem ((algebraMap S L) x)
<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>K✝ : Type u_5<VAR>inst✝¹⁴ : CommRing A<VAR>inst✝¹³ : IsDomain A<VAR>R : Type u_6<VAR>S : Type u_7<VAR>K : Type u_8<VAR>L : Type u_9<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : CommRing S<VAR>inst✝¹⁰ : Field K<VAR>inst✝⁹ : CommRing L<VAR>inst✝⁸ : Algebra R S<VAR>inst✝⁷ : Algebra R K<VAR>inst✝⁶ : Algebra R L<VAR>inst✝⁵ : Algebra S L<VAR>inst✝⁴ : Algebra K L<VAR>inst✝³ : IsScalarTower R S L<VAR>inst✝² : IsScalarTower R K L<VAR>inst✝¹ : IsFractionRing S L<VAR>inst✝ : Algebra.IsIntegral R S<VAR>x : S<VAR>s : ↥S⁰<GOAL>(algebraMap K L).IsIntegralElem (mk' L 1 s)
<VAR>u v m n✝ : ℤ<VAR>n : ℕ<GOAL>Even ↑n ↔ Even n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>h : b ≠ 0<GOAL>b * (a / b) + a % b < b * (a / b) + b
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : M'<GOAL>∃ a, Function.uncurry (mk' f) a = x
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>x : M'<VAR>m : M<VAR>s : ↥S<VAR>e : s • x = f m<GOAL>∃ a, Function.uncurry (mk' f) a = x
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : IndepSet t t κ μα<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t<GOAL>∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t<VAR>a : α<VAR>ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t<GOAL>(κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t<VAR>a : α<VAR>ha : (κ a) (t ∩ t) = (κ a) t * (κ a) t<VAR>h0 : ¬(κ a) t = 0<VAR>h_top : ¬(κ a) t = ⊤<GOAL>(κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → MeasurableSpace Ω<VAR>m m0 : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μα : Measure α<VAR>μ : Measure Ω<VAR>t : Set Ω<VAR>h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t<VAR>a : α<VAR>ha : 1 = (κ a) t<VAR>h0 : ¬(κ a) t = 0<VAR>h_top : ¬(κ a) t = ⊤<GOAL>(κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ⊤
<VAR>K : Type u_1<VAR>F : Type u_2<VAR>R : Type u_3<VAR>inst✝³ : DivisionRing K<VAR>Γ₀ : Type u_4<VAR>Γ'₀ : Type u_5<VAR>Γ''₀ : Type u_6<VAR>inst✝² : LinearOrderedCommMonoidWithZero Γ''₀<VAR>inst✝¹ : Ring R<VAR>inst✝ : LinearOrderedCommGroupWithZero Γ₀<VAR>v✝ : Valuation R Γ₀<VAR>x✝ y z : R<VAR>v : Valuation K Γ₀<VAR>x : K<VAR>h : x ≠ 0<GOAL>v x ≤ 1 ↔ 1 ≤ v x⁻¹
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>h : #↑(⋃ a, ⋃ (h : a ∈ s), t a h) < c<VAR>a : α<VAR>ha : a ∈ s<GOAL>#↑(t a ha) < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>h : #↑(⋃ x, t ↑x ⋯) < c<VAR>a : α<VAR>ha : a ∈ s<GOAL>#↑(t a ha) < c
<VAR>α✝ : Type u_1<VAR>r : α✝ → α✝ → Prop<VAR>α β : Type u<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>c : Cardinal.{u}<VAR>h : #↑(⋃ x, t ↑x ⋯) < c<VAR>a : α<VAR>ha : a ∈ s<VAR>this : ∀ (i : ↑s), #↑(t ↑i ⋯) < c<GOAL>#↑(t a ha) < c
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a b c d : G₀<VAR>h : a = 0 → b = 0<GOAL>a * b / a = b
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>f.SurjectiveOnStalks ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<GOAL>(∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x) ↔ ∀ (I : Ideal S), I ≠ ⊤ → ∀ (s : S), ∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x<VAR>I : Ideal S<VAR>hI : I ≠ ⊤<VAR>s : S<GOAL>∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x<VAR>I : Ideal S<VAR>hI : I ≠ ⊤<VAR>s : S<VAR>M : Ideal S<VAR>hM : M.IsMaximal<VAR>hIM : I ≤ M<GOAL>∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<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>T : Type u_3<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>g : S →+* T<VAR>f : R →+* S<VAR>H : ∀ (P : Ideal S), P.IsPrime → ∀ (s : S), ∃ x r, ∃ c ∉ P, f r ∉ P ∧ c * f r * s = c * f x<VAR>I : Ideal S<VAR>hI : I ≠ ⊤<VAR>s : S<VAR>M : Ideal S<VAR>hM : M.IsMaximal<VAR>hIM : I ≤ M<VAR>x r : R<VAR>c : S<VAR>hc : c ∉ M<VAR>hr : f r ∉ M<VAR>e : c * f r * s = c * f x<GOAL>∃ x r, ∃ c ∉ I, f r ∉ I ∧ c * f r * s = c * f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>r : ℝ≥0<GOAL>(r • s).toJordanDecomposition = r • s.toJordanDecomposition
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>r : ℝ≥0<GOAL>(r • s).toJordanDecomposition.toSignedMeasure = (r • s.toJordanDecomposition).toSignedMeasure
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<GOAL>f =ᶠ[𝓝 t₀] g
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : ∀ y ∈ ball t₀ ε, (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y<GOAL>f =ᶠ[𝓝 t₀] g
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : ∀ y ∈ ball t₀ ε, (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y<GOAL>∃ s ∈ 𝓝 t₀, EqOn f g s
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : ∀ y ∈ ball t₀ ε, (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y<GOAL>EqOn f g (ball t₀ ε)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>v : ℝ → E → E<VAR>s : ℝ → Set E<VAR>K : ℝ≥0<VAR>f g f' g' : ℝ → E<VAR>a b t₀ εf εg δ : ℝ<VAR>hv : ∀ (t : ℝ), LipschitzOnWith K (v t) (s t)<VAR>hf : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt f (v t (f t)) t ∧ f t ∈ s t<VAR>hg : ∀ᶠ (t : ℝ) in 𝓝 t₀, HasDerivAt g (v t (g t)) t ∧ g t ∈ s t<VAR>heq : f t₀ = g t₀<VAR>ε : ℝ<VAR>hε : ε > 0<VAR>h : ∀ y ∈ Ioo (t₀ - ε) (t₀ + ε), (HasDerivAt f (v y (f y)) y ∧ f y ∈ s y) ∧ HasDerivAt g (v y (g y)) y ∧ g y ∈ s y<GOAL>EqOn f g (Ioo (t₀ - ε) (t₀ + ε))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>sinZeta (↑x) (2 * ↑k + 1) = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1))) = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / 2 / ↑(2 * k + 1)! = (-1) ^ (k + 1) / (2 * ↑k + 1) / (2 * ↑k + 1).Gammaℂ
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (2 * (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * ↑k + 1) / ((2 * ↑k + 1) * 2 * Complex.Gamma (2 * ↑k + 1))
<VAR>k : ℕ<VAR>x : ℝ<VAR>hk : k ≠ 0<VAR>hx : x ∈ Icc 0 1<VAR>this : ↑(2 * k + 1)! = (2 * ↑k + 1) * Complex.Gamma (2 * ↑k + 1)<GOAL>(-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (2 * ↑(2 * k + 1) * Complex.Gamma ↑(2 * k + 1)) = (-1) ^ (k + 1) * (2 * ↑π) ^ (2 * k + 1) / (↑(2 * k + 1) * 2 * Complex.Gamma ↑(2 * k + 1))
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>ht : NullMeasurableSet t (μ.restrict s)<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>motive : ℤ → Prop<VAR>zero : motive 0<VAR>one : motive 1<VAR>add_two : ∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)<VAR>neg_add_one : ∀ (n : ℕ), motive (-↑n) → motive (-↑n + 1) → motive (-↑n - 1)<VAR>n : ℕ<VAR>hn : motive (-↑n)<VAR>hnm : motive (-↑n + 1)<GOAL>motive (Int.negSucc n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<GOAL>Continuous f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<GOAL>∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>δ : ℝ≥0<VAR>δ0 : δ > 0<VAR>hδ : ↑δ * C < ε<GOAL>∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>δ : ℝ≥0<VAR>δ0 : δ > 0<VAR>hδ : C * ↑δ < ε<GOAL>∀ᶠ (x_1 : α) in 𝓝 x, f x_1 ∈ Icc (f x - ε) (f x + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>δ : ℝ≥0<VAR>δ0 : δ > 0<VAR>hδ : C * ↑δ < ε<VAR>y : α<VAR>hy : y ∈ EMetric.closedBall x ↑δ<GOAL>f y ∈ Icc (f x - ε) (f x + ε)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>δ : ℝ≥0<VAR>δ0 : δ > 0<VAR>hδ : C * ↑δ < ε<VAR>y : α<VAR>hy : y ∈ EMetric.closedBall x ↑δ<GOAL>edist x y ≤ ↑δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : α → ℝ≥0∞<VAR>C : ℝ≥0∞<VAR>hC : C ≠ ⊤<VAR>h : ∀ (x y : α), f x ≤ f y + C * edist x y<VAR>x : α<VAR>ε : ℝ≥0∞<VAR>ε0 : ε > 0<VAR>δ : ℝ≥0<VAR>δ0 : δ > 0<VAR>hδ : C * ↑δ < ε<VAR>y : α<VAR>hy : y ∈ EMetric.closedBall x ↑δ<GOAL>edist y x ≤ ↑δ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Lattice α<VAR>inst✝² : Group α<VAR>a✝ : α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a : α<GOAL>a⁻ᵐ = (a ⊓ 1)⁻¹
<VAR>R : Type u_1<VAR>inst✝¹² : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : Module R M<VAR>N : Type u_3<VAR>inst✝⁹ : AddCommMonoid N<VAR>inst✝⁸ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁷ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁶ : OrderedCommSemiring S<VAR>inst✝⁵ : Algebra S R<VAR>inst✝⁴ : Module S M<VAR>inst✝³ : SMulPosMono S R<VAR>inst✝² : IsScalarTower S R M<VAR>a : S<VAR>F : Type u_6<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : LinearMapClass F R M N<VAR>f : F<VAR>hf : Function.Injective ⇑f<GOAL>SameRay R (f x) (f y) ↔ SameRay R x y
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : Semiring S<VAR>inst✝⁶ : Algebra R S<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module S M<VAR>inst✝² : IsScalarTower R S M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>b : Basis ι S M<VAR>c : Basis κ R N<VAR>m : M<VAR>n : N<VAR>i : ι<VAR>j : κ<GOAL>((b.tensorProduct c).repr (m ⊗ₜ[R] n)) (i, j) = (c.repr n) j • (b.repr m) i
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a✝ b : R<VAR>n✝ : ℕ<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : IsDomain R<VAR>p q : R[X]<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Algebra T S<VAR>inst✝ : NoZeroSMulDivisors T S<VAR>a : T<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>(C a * X ^ n).aroots S = n • {0}
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x<VAR>hsub : insert x₀ (K ∩ s) ⊆ s<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝⁴ : LinearOrder α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : ClosedIicTopology α<VAR>s : Set β<VAR>f : β → α<VAR>hf : ContinuousOn f s<VAR>hsc : IsClosed s<VAR>x₀ : β<VAR>h₀ : x₀ ∈ s<VAR>hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x<VAR>K : Set β<VAR>hK : IsCompact K<VAR>hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x<VAR>hsub : insert x₀ (K ∩ s) ⊆ s<VAR>x : β<VAR>hx : x ∈ insert x₀ (K ∩ s)<VAR>hxf : ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y<GOAL>∃ x ∈ s, IsMinOn f s x
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<GOAL>HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)<GOAL>HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)<GOAL>HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (completedCosZeta (↑a) s)
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)<GOAL>HasSum (fun n => s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2) (mellin (fun t => (↑(cosKernel (↑a) t) - 1) / 2) (s / 2))
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)<GOAL>Summable fun i => ‖c i‖ / |↑i| ^ s.re
<VAR>a : ℝ<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>c : ℤ → ℂ := fun n => cexp (2 * ↑π * I * ↑a * ↑n) / 2<VAR>hF : ∀ (t : ℝ), 0 < t → HasSum (fun n => if ↑n = 0 then 0 else c n * ↑(rexp (-π * ↑n ^ 2 * t))) ((↑(cosKernel (↑a) t) - 1) / 2)<VAR>n : ℤ<GOAL>s.Gammaℝ * cexp (2 * ↑π * I * ↑a * ↑n) / ↑|n| ^ s / 2 = s.Gammaℝ * c n / ↑|↑n| ^ s
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>x✝¹ x✝ : ↑X<GOAL>g (1 ⊗ₜ[R] (x✝¹ + x✝)) = g (1 ⊗ₜ[R] x✝¹) + g (1 ⊗ₜ[R] x✝)
<VAR>R✝ : Type u₁<VAR>S✝ : Type u₂<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : CommRing S✝<VAR>f✝ : R✝ →+* S✝<VAR>R : Type u₁<VAR>S : Type u₂<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>X : ModuleCat R<VAR>Y : ModuleCat S<VAR>g : (extendScalars f).obj X ⟶ Y<VAR>r : R<VAR>x : ↑X<VAR>this✝ : Module R S := Module.compHom S f<VAR>this : Module R ↑Y := Module.compHom (↑Y) f<GOAL>g (1 ⊗ₜ[R] (r • x)) = f r • g (1 ⊗ₜ[R] x)