ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>x' : S<VAR>f : A[X]<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * x') = ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) x'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : Ring S<VAR>inst✝⁸ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : Algebra A B<VAR>K : Type u_6<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra A S<VAR>S' : Type u_7<VAR>inst✝¹ : Ring S'<VAR>inst✝ : Algebra A S'<VAR>pb : PowerBasis A S<VAR>y : S'<VAR>hy : (aeval y) (minpoly A pb.gen) = 0<VAR>f g : A[X]<GOAL>((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f * (aeval pb.gen) g) = ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) f) * ((pb.basis.constr A) fun i => y ^ ↑i) ((aeval pb.gen) g)
<GOAL>Tendsto (fun x => x ^ (-1 / x)) atTop (𝓝 1)
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁.get? n = l₂.get? n<VAR>n : ℕ<GOAL>l₁.get? n = l₂.get? n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁.get? n = l₂.get? n<VAR>n : ℕ<VAR>hn : n < max l₁.length l₂.length<GOAL>l₁.get? n = l₂.get? n
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁✝ l₂✝ l₁ l₂ : List α<VAR>h' : ∀ (n : ℕ), n < max l₁.length l₂.length → l₁.get? n = l₂.get? n<VAR>n : ℕ<VAR>hn : n ≥ max l₁.length l₂.length<GOAL>l₁.get? n = l₂.get? n
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>x y a p : R<VAR>n : ℕ<VAR>hp : Prime p<VAR>hx : x * y = a * p ^ n<GOAL>∃ i j b c, i + j = n ∧ a = b * c ∧ x = b * p ^ i ∧ y = c * p ^ j
<VAR>R : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero R<VAR>p : R<VAR>n : ℕ<VAR>hp : Prime p<VAR>t u : Finset ℕ<VAR>b c : R<VAR>htus : t ∪ u = range n<VAR>htu : Disjoint t u<VAR>hx : (b * ∏ i ∈ t, p) * (c * ∏ i ∈ u, p) = b * c * p ^ n<GOAL>∃ i j b_1 c_1, i + j = n ∧ b * c = b_1 * c_1 ∧ b * ∏ i ∈ t, p = b_1 * p ^ i ∧ c * ∏ i ∈ u, p = c_1 * p ^ j
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(-j).toSignedMeasure i = ↑(-j.toSignedMeasure) i
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ≤ a ⇨ b ↔ a ≤ b
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p✝ q p : R[X]<GOAL>p %ₘ X = C (eval 0 p)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝⁵ : NormedRing R<VAR>inst✝⁴ : NormedAlgebra 𝕜 R<VAR>𝕜' : Type u_4<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : CompleteSpace 𝕜'<VAR>inst✝ : CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>hf : ContDiff 𝕜 n f<VAR>hg : ContDiff 𝕜 n g<VAR>h0 : ∀ (x : E), g x ≠ 0<GOAL>ContDiff 𝕜 n fun x => f x / g x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹⁵ : NormedAddCommGroup D<VAR>inst✝¹⁴ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹³ : NormedAddCommGroup E<VAR>inst✝¹² : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁹ : NormedAddCommGroup G<VAR>inst✝⁸ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup X<VAR>inst✝⁶ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g✝ : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝⁵ : NormedRing R<VAR>inst✝⁴ : NormedAlgebra 𝕜 R<VAR>𝕜' : Type u_4<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : CompleteSpace 𝕜'<VAR>inst✝ : CompleteSpace 𝕜<VAR>f g : E → 𝕜<VAR>n : ℕ∞<VAR>h0 : ∀ (x : E), g x ≠ 0<VAR>hf : ∀ (x : E), ContDiffAt 𝕜 n f x<VAR>hg : ∀ (x : E), ContDiffAt 𝕜 n g x<GOAL>∀ (x : E), ContDiffAt 𝕜 n (fun x => f x / g x) x
<VAR>n : ℕ<VAR>h1 : ble 2 n = true<VAR>h2 : 1 = n % 2<GOAL>3 ≤ n.minFac
<VAR>n : ℕ<VAR>h1 : ble 2 n = true<VAR>h2 : 1 = n % 2<VAR>p : ℕ<VAR>hp : 2 ≤ p<VAR>hpn : p ∣ n<GOAL>3 ≤ p
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))<VAR>h : ∀ (i : ι), (F.val.map (leSupr U i).op) s = (F.val.map (leSupr U i).op) t<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i))) := fun i => (F.val.map (leSupr U i).op) s<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))<VAR>h : ∀ (i : ι), (F.val.map (leSupr U i).op) s = (F.val.map (leSupr U i).op) t<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i))) := fun i => (F.val.map (leSupr U i).op) s<VAR>sf_compatible : IsCompatible F.val U sf<GOAL>s = t
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : ConcreteCategory C<VAR>inst✝² : HasLimits C<VAR>inst✝¹ : ConcreteCategory.forget.ReflectsIsomorphisms<VAR>inst✝ : PreservesLimits ConcreteCategory.forget<VAR>X : TopCat<VAR>F : Sheaf C X<VAR>ι : Type v<VAR>U : ι → Opens ↑X<VAR>s t : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))<VAR>h : ∀ (i : ι), (F.val.map (leSupr U i).op) s = (F.val.map (leSupr U i).op) t<VAR>sf : (i : ι) → (CategoryTheory.forget C).obj (F.val.obj (op (U i))) := fun i => (F.val.map (leSupr U i).op) s<VAR>sf_compatible : IsCompatible F.val U sf<VAR>gl : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))<VAR>gl_uniq : ∀ (y : (CategoryTheory.forget C).obj (F.val.obj (op (iSup U)))), (fun s => IsGluing F.val U sf s) y → y = gl<GOAL>s = t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝² : PseudoEMetricSpace X<VAR>inst✝¹ : PseudoEMetricSpace Y<VAR>inst✝ : PseudoEMetricSpace Z<VAR>e : X ≃ᵈ Y<GOAL>ratio e.symm * ratio e = 1
<VAR>R : Type uR<VAR>M : Type uM<VAR>K : Type uK<VAR>V : Type uV<VAR>ι : Type uι<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : Module R M<VAR>inst✝ : DecidableEq ι<VAR>b : Basis ι R M<VAR>m : M<VAR>a : b.toDual m = 0<GOAL>b.toDual m = b.toDual 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : ℤ → α<VAR>a : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ (i : ℤ), f (i % ↑n) = f i<VAR>hn' : 0 < ↑n<VAR>x✝ : ∃ i, f (i % ↑n) = a<VAR>i : ℤ<VAR>hi : f (i % ↑n) = a<VAR>this : 0 ≤ i % ↑n<GOAL>(i % ↑n).toNat < n ∧ f ↑(i % ↑n).toNat = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : ℤ → α<VAR>a : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ (i : ℤ), f (i % ↑n) = f i<VAR>hn' : 0 < ↑n<VAR>x✝ : ∃ i, f (i % ↑n) = a<VAR>i : ℤ<VAR>hi : f (i % ↑n) = a<VAR>this : 0 ≤ i % ↑n<GOAL>i % ↑n < ↑n ∧ f (i % ↑n) = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : ℤ → α<VAR>a : α<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ∀ (i : ℤ), f (i % ↑n) = f i<VAR>hn' : 0 < ↑n<VAR>x✝ : ∃ i < n, f ↑i = a<VAR>i : ℕ<VAR>hi : i < n<VAR>ha : f ↑i = a<GOAL>f (↑i % ↑n) = a
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hf this : FiniteDimensional k ↥s.direction<GOAL>finrank k ↥(vectorSpan k (insert p ↑s)) ≤ finrank k ↥s.direction + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hf this : FiniteDimensional k ↥s.direction<GOAL>finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hf this : FiniteDimensional k ↥s.direction<VAR>hs : ↑s = ∅<GOAL>finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>s : AffineSubspace k P<VAR>p : P<VAR>hf this : FiniteDimensional k ↥s.direction<VAR>p₀ : P<VAR>hp₀ : p₀ ∈ ↑s<GOAL>finrank k ↥(affineSpan k (insert p ↑(affineSpan k ↑s))).direction ≤ finrank k ↥s.direction + 1
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>A B C : Set α<VAR>D E : Set ↑A<VAR>S : Set (Set α)<VAR>T : Set (Set ↑A)<VAR>s : ι → Set α<VAR>t : ι → Set ↑A<GOAL>A ↓∩ ⋂₀ S = ⋂₀ ((fun x => A ↓∩ x) '' S)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<GOAL>spanNorm R (I * J) = spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<GOAL>spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<VAR>hI : spanNorm R I = ⊤<GOAL>spanNorm R (I * J) ≤ spanNorm R I * spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<VAR>hI : spanNorm R I = ⊤<GOAL>spanNorm R (I * J) ≤ spanNorm R J
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>S : Type u_2<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : IsDomain R<VAR>inst✝² : IsDomain S<VAR>inst✝¹ : Module.Free R S<VAR>inst✝ : Module.Finite R S<VAR>eq_bot_or_top : ∀ (I : Ideal R), I = ⊥ ∨ I = ⊤<VAR>I J : Ideal S<VAR>hI : spanNorm R I = ⊤<VAR>hJ : spanNorm R J = ⊤<GOAL>spanNorm R (I * J) ≤ ⊤
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Preadditive C<VAR>X : SimplicialObject C<VAR>n : ℕ<GOAL>(ChainComplex.of (fun n => X _[n]) (AlternatingFaceMapComplex.objD X) ⋯).d (n + 1) n = AlternatingFaceMapComplex.objD X n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>⨆ n, ↑(eapprox f n) a = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<GOAL>¬f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>h : f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>h : f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k<VAR>q : ℚ<VAR>left✝ : 0 ≤ q<VAR>lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal<VAR>q_lt : ↑(↑q).toNNReal < f a<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>K : Type u_5<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>a : α<VAR>h : f a > ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k<VAR>q : ℚ<VAR>left✝ : 0 ≤ q<VAR>lt_q : ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k < ↑(↑q).toNNReal<VAR>q_lt : ↑(↑q).toNNReal < f a<VAR>this : ↑(↑q).toNNReal ≤ ⨆ k, ⨆ (_ : ennrealRatEmbed k ≤ f a), ennrealRatEmbed k<GOAL>False
<VAR>x y a b : ℝ<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(fun x => x ^ n / (a * rexp x + b)) ∘ log =ᶠ[atTop] fun x => log x ^ n / (a * x + b)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>TopologicalSpace.IsTopologicalBasis (SetLike.coe '' Set.range basicOpen)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>SetLike.coe '' Set.range basicOpen = Set.range fun r => ↑(basicOpen r)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<GOAL>Set.range (SetLike.coe ∘ basicOpen) = Set.range fun r => ↑(basicOpen r)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>x✝¹ : 0 ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>x✝ : IsClosed C<VAR>hsC : contained C 0<GOAL>LinearIndependent ℤ (eval C)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>x✝¹ : 0 ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>x✝ : IsClosed C<VAR>hsC : contained C 0<VAR>this : C ⊆ {fun x => false}<GOAL>LinearIndependent ℤ (eval C)
<VAR>I : Type u<VAR>inst✝¹ : LinearOrder I<VAR>inst✝ : IsWellOrder I fun x x_1 => x < x_1<VAR>C✝ : Set (I → Bool)<VAR>x✝¹ : 0 ≤ Ordinal.type fun x x_1 => x < x_1<VAR>C : Set (I → Bool)<VAR>x✝ : IsClosed C<VAR>hsC : contained C 0<VAR>this : C = ∅ ∨ C = {fun x => false}<GOAL>LinearIndependent ℤ (eval C)
<VAR>f g : ℕ → ℂ<VAR>s : ℂ<GOAL>term (f - g) s = term f s - term g s
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>enumOrd S o ∈ S ∩ Ici (o.blsub fun c x => enumOrd S c)
<VAR>S : Set Ordinal.{u}<VAR>hS : Unbounded (fun x x_1 => x < x_1) S<VAR>o : Ordinal.{u}<GOAL>sInf (S ∩ Ici (o.blsub fun a x => enumOrd S a)) ∈ S ∩ Ici (o.blsub fun c x => enumOrd S c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyCoatomic α<VAR>ha : (Set.Iic a).Infinite<VAR>hfin : {x | x ⋖ a}.Finite<GOAL>∃ b, b ⋖ a ∧ (Set.Iic b).Infinite
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>a : α<VAR>inst✝ : IsStronglyCoatomic α<VAR>ha : (Set.Iic a).Infinite<VAR>hfin : {x | OrderDual.toDual a ⋖ OrderDual.toDual x}.Finite<GOAL>∃ b, OrderDual.toDual a ⋖ OrderDual.toDual b ∧ (Set.Iic b).Infinite
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>hs' : ∀ (n : ℕ), s ≠ -↑n<GOAL>expZeta a (1 - s) = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (↑π * I * s / 2) * hurwitzZeta a s + cexp (-↑π * I * s / 2) * hurwitzZeta (-a) s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>hs' : ∀ (n : ℕ), s ≠ -↑n<GOAL>2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * hurwitzZetaEven a s + I * (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) * hurwitzZetaOdd a s) = (2 * ↑π) ^ (-s) * Complex.Gamma s * (cexp (↑π * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) + cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>hs' : ∀ (n : ℕ), s ≠ -↑n<VAR>x y z : ℂ<GOAL>x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * I ^ 2 * hurwitzZetaOdd a s + x * Complex.Gamma s * z * hurwitzZetaEven a s + x * Complex.Gamma s * z * I ^ 2 * hurwitzZetaOdd a s = x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s + (x * Complex.Gamma s * z * hurwitzZetaEven a s - x * Complex.Gamma s * z * hurwitzZetaOdd a s)
<VAR>a : UnitAddCircle<VAR>s : ℂ<VAR>hs : ∀ (n : ℕ), s ≠ 1 - ↑n<VAR>hs' : ∀ (n : ℕ), s ≠ -↑n<VAR>x y z : ℂ<GOAL>x * Complex.Gamma s * y * hurwitzZetaEven a s - x * Complex.Gamma s * y * -1 * hurwitzZetaOdd a s + x * Complex.Gamma s * z * hurwitzZetaEven a s + x * Complex.Gamma s * z * -1 * hurwitzZetaOdd a s = x * Complex.Gamma s * y * hurwitzZetaEven a s + x * Complex.Gamma s * y * hurwitzZetaOdd a s + (x * Complex.Gamma s * z * hurwitzZetaEven a s - x * Complex.Gamma s * z * hurwitzZetaOdd a s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>s.singularPart μ + μ.withDensityᵥ (s.rnDeriv μ) = s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>(s.toJordanDecomposition.posPart.singularPart μ + μ.withDensity (s.toJordanDecomposition.posPart.rnDeriv μ)).toSignedMeasure - (μ.withDensity (s.toJordanDecomposition.negPart.rnDeriv μ) + s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure = s.toJordanDecomposition.posPart.toSignedMeasure - s.toJordanDecomposition.negPart.toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>AEMeasurable (s.toJordanDecomposition.negPart.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>∫⁻ (x : α), s.toJordanDecomposition.negPart.rnDeriv μ x ∂μ ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>AEMeasurable (s.toJordanDecomposition.posPart.rnDeriv μ) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>s t : SignedMeasure α<VAR>inst✝ : s.HaveLebesgueDecomposition μ<GOAL>∫⁻ (x : α), s.toJordanDecomposition.posPart.rnDeriv μ x ∂μ ≠ ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : p.leadingCoeff ^ 0 ≠ 0<GOAL>(p ^ 0).degree = 0 • p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : 1 ≠ 0<GOAL>(C 1).degree = 0 • p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ (n + 1) ≠ 0<GOAL>(p ^ (n + 1)).degree = (n + 1) • p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ (n + 1) ≠ 0<VAR>h₁ : p.leadingCoeff ^ n ≠ 0<GOAL>(p ^ (n + 1)).degree = (n + 1) • p.degree
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>n : ℕ<VAR>h : p.leadingCoeff ^ (n + 1) ≠ 0<VAR>h₁ : p.leadingCoeff ^ n ≠ 0<VAR>h₂ : (p ^ n).leadingCoeff * p.leadingCoeff ≠ 0<GOAL>(p ^ (n + 1)).degree = (n + 1) • p.degree
<VAR>α : Type u_1<VAR>inst✝¹ : Ring α<VAR>inst✝ : CharZero α<VAR>n✝¹ n✝ : ℤ<VAR>h : decide (n✝¹ = n✝) = false<GOAL>¬↑n✝¹ = ↑n✝
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>h : IsPushout f g inl inr<VAR>Z' X' Y' P' : C<VAR>f' : Z' ⟶ X'<VAR>g' : Z' ⟶ Y'<VAR>inl' : X' ⟶ P'<VAR>inr' : Y' ⟶ P'<VAR>e₁ : Z ≅ Z'<VAR>e₂ : X ≅ X'<VAR>e₃ : Y ≅ Y'<VAR>e₄ : P ≅ P'<VAR>commf : f ≫ e₂.hom = e₁.hom ≫ f'<VAR>commg : g ≫ e₃.hom = e₁.hom ≫ g'<VAR>comminl : inl ≫ e₄.hom = e₂.hom ≫ inl'<VAR>comminr : inr ≫ e₄.hom = e₃.hom ≫ inr'<GOAL>f' ≫ inl' = g' ≫ inr'
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<GOAL>x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<GOAL>x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<VAR>hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))<GOAL>x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<VAR>hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))<VAR>h5 : 0 < x<GOAL>x * (2 * x) ^ √(2 * x) * 4 ^ (2 * x / 3) ≤ 4 ^ x
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<VAR>hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))<VAR>h5 : 0 < x<GOAL>f x ≤ 0
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<VAR>hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))<VAR>h5 : 0 < x<VAR>h : ConcaveOn ℝ (Set.Ioi 0.5) f<GOAL>f x ≤ 0
<VAR>x : ℝ<VAR>x_large : 512 ≤ x<VAR>f : ℝ → ℝ := fun x => log x + √(2 * x) * log (2 * x) - log 4 / 3 * x<VAR>hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3)<VAR>hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / 4 ^ (x / 3))<VAR>h5 : 0 < x<VAR>h : ConcaveOn ℝ (Set.Ioi 0.5) f<GOAL>∃ x1 x2, 0.5 < x1 ∧ x1 < x2 ∧ x2 ≤ x ∧ 0 ≤ f x1 ∧ f x2 ≤ 0
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>x y z : ℝ<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<VAR>this : (fun x => x.1 ^ x.2) =ᶠ[𝓝 p] fun x => rexp (log x.1 * x.2) * cos (x.2 * π)<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * log p.1 - rexp (log p.1 * p.2) * sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ) p