ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>α : Type u_7<VAR>inst✝⁸ : LinearOrderedField R<VAR>inst✝⁷ : LinearOrderedField R'<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : AddCommGroup F<VAR>inst✝⁴ : LinearOrderedAddCommGroup α<VAR>inst✝³ : Module R E<VAR>inst✝² : Module R F<VAR>inst✝¹ : Module R α<VAR>inst✝ : OrderedSMul R α<VAR>s : Set E<VAR>i j : ι<VAR>c : R<VAR>t : Finset ι<VAR>w : ι → R<VAR>z : ι → E<VAR>hne : i ≠ j<GOAL>{i, j}.centerMass w z = (w i / (w i + w j)) • z i + (w j / (w i + w j)) • z j
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>χ : DirichletCharacter ℂ 0<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hN : N ≠ 0<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hN : N ≠ 0<VAR>hχ : LSeriesSummable (fun n => χ ↑n) s<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hN : N ≠ 0<VAR>hχ : LSeriesSummable (fun n => χ ↑n) s<VAR>hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hN : N ≠ 0<VAR>hχ : LSeriesSummable (fun n => χ ↑n) s<VAR>hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re<VAR>hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s<GOAL>L ((fun n => χ ↑n) * fun n => ↑(Λ n)) s = -deriv (L fun n => χ ↑n) s / L (fun n => χ ↑n) s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>hN : N ≠ 0<VAR>hχ : LSeriesSummable (fun n => χ ↑n) s<VAR>hs' : (abscissaOfAbsConv fun n => χ ↑n) < ↑s.re<VAR>hΛ : LSeriesSummable ((fun n => χ ↑n) * fun n => ↑(Λ n)) s<GOAL>L ((fun n => χ ↑n) * fun n => Complex.log ↑n) s = L (logMul fun n => χ ↑n) s
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_2<VAR>π : ι → Type u_3<VAR>r : α → α → Prop<VAR>inst✝ : Preorder α<VAR>f : ℤ → α<VAR>hf : Antitone f<VAR>n a : ℤ<VAR>h1 : f (n + 1) < f a<VAR>h2 : f a < f n<GOAL>False
<VAR>x✝ y✝ z x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<GOAL>x ^ y = rexp (log x * y) * cos (y * π)
<VAR>x✝ y✝ z x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<GOAL>(Complex.exp (Complex.log ↑x * ↑y)).re = rexp (log x * y) * cos (y * π)
<VAR>x✝ y✝ z x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<GOAL>¬↑x = 0
<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>f : E → F<VAR>x : E<GOAL>HasFDerivWithinAt f 0 {x} x
<VAR>z τ : ℂ<GOAL>jacobiTheta₂ (z + 1) τ = jacobiTheta₂ z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>jacobiTheta₂_term n (z + 1) τ = jacobiTheta₂_term n z τ
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>hf : Function.Injective f<GOAL>((rename f) φ).IsHomogeneous n ↔ φ.IsHomogeneous n
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>f : σ → τ<VAR>hf : Function.Injective f<VAR>h : ((rename f) φ).IsHomogeneous n<VAR>d : σ →₀ ℕ<VAR>hd : coeff d φ ≠ 0<GOAL>(weight 1) d = n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<GOAL>⟪0, 0⟫_𝕜 = 0
<VAR>θ : ℝ<VAR>h0 : 0 ≤ θ<VAR>hpi : θ ≤ π<GOAL>0 ≤ (↑θ).sign
<VAR>θ : ℝ<VAR>h0 : 0 ≤ θ<VAR>hpi : θ ≤ π<GOAL>0 ≤ (↑θ).sin
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Cofix F α<GOAL>mk x.dest = x
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x : Cofix F α<GOAL>∀ (x y : Cofix F α), (fun x y => x = mk y.dest) x y → (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> x.dest = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> (mk y.dest).dest = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> (TypeVec.id ::: corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$> (TypeVec.id ::: fun i => i.dest) <$$> y.dest = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(TypeVec.id ::: (Quot.mk fun x y => x = mk y.dest) ∘ corec fun x => (TypeVec.id ::: fun i => i.dest) <$$> x) <$$> (TypeVec.id ::: fun i => i.dest) <$$> y.dest = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) <$$> y.dest = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest) <$$> y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(TypeVec.id ::: ((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) = (TypeVec.id ::: Quot.mk fun x y => x = mk y.dest)
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝ x y : Cofix F α<VAR>h : x = mk y.dest<GOAL>(((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) = Quot.mk fun x y => x = mk y.dest
<VAR>n : ℕ<VAR>F : TypeVec.{u} (n + 1) → Type u<VAR>q : MvQPF F<VAR>α : TypeVec.{u} n<VAR>x✝¹ x✝ y : Cofix F α<VAR>h : x✝ = mk y.dest<VAR>x : Cofix F α<GOAL>(((Quot.mk fun x y => x = mk y.dest) ∘ mk) ∘ fun i => i.dest) x = Quot.mk (fun x y => x = mk y.dest) x
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i✝ j i : ι<GOAL>Lagrange.basis {i} v i = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : OrderedCommSemiring α<VAR>inst✝³ : StrictOrderedSemiring β<VAR>inst✝² : Algebra α β<VAR>inst✝¹ : SMulPosMono α β<VAR>inst✝ : SMulPosReflectLE α β<VAR>a₁ a₂ : α<GOAL>(algebraMap α β) a₁ ≤ (algebraMap α β) a₂ ↔ a₁ ≤ a₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<GOAL>s.sdiff t ⊔ lowerClosure t = s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a✝ : α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<VAR>a : α<VAR>ha : a ∈ ↑s<GOAL>a ∈ ↑(s.sdiff t ⊔ lowerClosure t)
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>v : ι → F<VAR>i : ι<GOAL>nodalWeight s v i = (eval (v i) (nodal (s.erase i) v))⁻¹
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝¹ : X → ↑F X<VAR>xs : Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<VAR>f✝ : F.B a → F.M<VAR>hp : IsPath xs (f✝ i)<VAR>h : M.mk ⟨a, f⟩ = M.mk ⟨a, f✝⟩<GOAL>IsPath xs (f i)
<VAR>F : PFunctor.{u}<VAR>X : Type u_1<VAR>f✝ : X → ↑F X<VAR>xs : Path F<VAR>a : F.A<VAR>f : F.B a → F.M<VAR>i : F.B a<VAR>hp : IsPath xs (f i)<VAR>h : M.mk ⟨a, f⟩ = M.mk ⟨a, f⟩<GOAL>IsPath xs (f i)
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring R₁<VAR>inst✝⁶ : AddCommMonoid M₁<VAR>inst✝⁵ : Module R₁ M₁<VAR>inst✝⁴ : CommSemiring R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<VAR>x : M₂<GOAL>(B 0) x = 0
<VAR>a b m n✝ p✝ n p : ℕ<VAR>hp : Prime p<VAR>hn : n ≠ 0<VAR>h : p ∣ n<GOAL>0 < n.factorization p
<VAR>α : Type u_1<VAR>n : ℤ<GOAL>↑↑n.natAbs = ↑↑n.natAbs
<VAR>α : Type u_1<VAR>n : ℤ<GOAL>↑↑n.natAbs = |↑n|
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>(∑' (i : ℕ), x ^ i) * (1 - x) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))<GOAL>(∑' (i : ℕ), x ^ i) * (1 - x) = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))<VAR>this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, x ^ i * (1 - x)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<VAR>this✝ : HasSum (fun i => x ^ i * (1 - x)) ((∑' (b : ℕ), x ^ b) * (1 - x))<VAR>this : Tendsto (fun n => 1 - x ^ n) atTop (𝓝 1)<VAR>x✝ : ℕ<GOAL>1 - x ^ x✝ = ∑ i ∈ Finset.range x✝, x ^ i * (1 - x)
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a x : α<GOAL>x ∈ Ioi a ↔ a < x
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : a ∈ ball b r<GOAL>a ^ n ∈ ball (b ^ n) (n • r)
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ‖a / b‖ < r<GOAL>‖(a / b) ^ n‖ < n • r
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : ‖a / b‖ < r<GOAL>↑n * ‖a / b‖ < n • r
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>h : ‖a / b‖ < r<VAR>hn : 0 < ↑n<GOAL>↑n * ‖a / b‖ < n • r
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>n : ℕ<VAR>h : ‖a / b‖ < r<VAR>hn : 0 < ↑n<GOAL>↑n * ‖a / b‖ < ↑n * r
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>t.prod.leadingCoeff = (Multiset.map (fun f => f.leadingCoeff) t).prod
<VAR>R : Type u<VAR>ι : Type w<VAR>s : Finset ι<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : NoZeroDivisors R<VAR>f : ι → R[X]<VAR>t : Multiset R[X]<GOAL>(Multiset.map (⇑leadingCoeffHom) t).prod = (Multiset.map (fun f => f.leadingCoeff) t).prod
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₁ d₂ d₃ : ManyOneDegree<GOAL>d₁ ≤ d₂ → d₂ ≤ d₃ → d₁ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₂ d₃ : ManyOneDegree<VAR>p✝ : Set ℕ<GOAL>of p✝ ≤ d₂ → d₂ ≤ d₃ → of p✝ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>d₃ : ManyOneDegree<VAR>p✝¹ p✝ : Set ℕ<GOAL>of p✝¹ ≤ of p✝ → of p✝ ≤ d₃ → of p✝¹ ≤ d₃
<VAR>α : Type u<VAR>inst✝⁵ : Primcodable α<VAR>inst✝⁴ : Inhabited α<VAR>β : Type v<VAR>inst✝³ : Primcodable β<VAR>inst✝² : Inhabited β<VAR>γ : Type w<VAR>inst✝¹ : Primcodable γ<VAR>inst✝ : Inhabited γ<VAR>p✝² p✝¹ p✝ : Set ℕ<GOAL>of p✝² ≤ of p✝¹ → of p✝¹ ≤ of p✝ → of p✝² ≤ of p✝
<VAR>x✝ y x : ℝ<GOAL>log x ≠ 0 ↔ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y : S<GOAL>eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y : S<VAR>cast_succ : ↑d + 1 = ↑d.succ<GOAL>eval (1 + y) ((monomial d) (↑d + 1)) - eval y ((monomial d) (↑d + 1)) = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y : S<VAR>cast_succ : ↑d + 1 = ↑d.succ<GOAL>↑d.succ * ∑ m ∈ range (d + 1), y ^ m * 1 ^ (d - m) * ↑(d.choose m) - ↑d.succ * y ^ d = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y : S<VAR>cast_succ : ↑d + 1 = ↑d.succ<GOAL>↑d.succ * ∑ x ∈ range (d + 1), ↑(d.choose x) * y ^ x - ↑d.succ * y ^ d = ∑ x_1 ∈ range (d + 1), ↑((d + 1).choose x_1) * (↑x_1 * y ^ (x_1 - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y : S<VAR>cast_succ : ↑d + 1 = ↑d.succ<GOAL>∑ i ∈ range d, ↑d.succ * (↑(d.choose i) * y ^ i) = ∑ k ∈ range d, ↑((d + 1).choose (k + 1)) * (↑(k + 1) * y ^ (k + 1 - 1))
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r : R[X]<VAR>x : R<VAR>inst✝ : CommRing S<VAR>d : ℕ<VAR>y✝ : S<VAR>cast_succ : ↑d + 1 = ↑d.succ<VAR>y : ℕ<VAR>_hy : y ∈ range d<GOAL>↑d.succ * (↑(d.choose y) * y✝ ^ y) = ↑((d + 1).choose (y + 1)) * (↑(y + 1) * y✝ ^ (y + 1 - 1))
<VAR>K : Type u<VAR>A : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra K A<VAR>x : A<GOAL>IsAlgebraic K x ↔ IsIntegral K x
<VAR>K : Type u<VAR>A : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra K A<VAR>x : A<GOAL>IsAlgebraic K x → IsIntegral K x
<VAR>K : Type u<VAR>A : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra K A<VAR>x : A<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>hpx : (aeval x) p = 0<GOAL>IsIntegral K x
<VAR>K : Type u<VAR>A : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra K A<VAR>x : A<VAR>p : K[X]<VAR>hp : p ≠ 0<VAR>hpx : (aeval x) p = 0<GOAL>eval₂ (algebraMap K A) x (p * C p.leadingCoeff⁻¹) = 0
<VAR>n : ℕ<GOAL>(treesOfNumNodesEq n).card = catalan n
<GOAL>(treesOfNumNodesEq 0).card = catalan 0
<VAR>n : ℕ<VAR>ih : ∀ m ≤ n, (treesOfNumNodesEq m).card = catalan m<GOAL>(treesOfNumNodesEq n.succ).card = catalan n.succ
<VAR>n : ℕ<VAR>ih : ∀ m ≤ n, (treesOfNumNodesEq m).card = catalan m<GOAL>∑ u ∈ antidiagonal n, (pairwiseNode (treesOfNumNodesEq u.1) (treesOfNumNodesEq u.2)).card = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2
<VAR>n : ℕ<VAR>ih : ∀ m ≤ n, (treesOfNumNodesEq m).card = catalan m<GOAL>∀ x ∈ antidiagonal n, ∀ y ∈ antidiagonal n, x ≠ y → Disjoint (pairwiseNode (treesOfNumNodesEq x.1) (treesOfNumNodesEq x.2)) (pairwiseNode (treesOfNumNodesEq y.1) (treesOfNumNodesEq y.2))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : finrank ℝ E = n<VAR>x : Orientation ℝ E (Fin n)<GOAL>(Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : finrank ℝ E = n<VAR>x : Orientation ℝ E (Fin n)<VAR>this : Nonempty (Fin n)<GOAL>(Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace ℝ E<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h : finrank ℝ E = n<VAR>x : Orientation ℝ E (Fin n)<VAR>this✝ : Nonempty (Fin n)<VAR>this : FiniteDimensional ℝ E<GOAL>(Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁵ : Semiring R₁<VAR>inst✝²⁴ : Semiring R₂<VAR>inst✝²³ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝²² : TopologicalSpace M₁<VAR>inst✝²¹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝²⁰ : TopologicalSpace M'₁<VAR>inst✝¹⁹ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁸ : TopologicalSpace M₂<VAR>inst✝¹⁷ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁶ : TopologicalSpace M₃<VAR>inst✝¹⁵ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹⁴ : TopologicalSpace M₄<VAR>inst✝¹³ : AddCommMonoid M₄<VAR>inst✝¹² : Module R₁ M₁<VAR>inst✝¹¹ : Module R₁ M'₁<VAR>inst✝¹⁰ : Module R₂ M₂<VAR>inst✝⁹ : Module R₃ M₃<VAR>inst✝⁸ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>F : Type u_9<VAR>inst✝⁷ : Module R₁ M₂<VAR>inst✝⁶ : TopologicalSpace R₁<VAR>inst✝⁵ : ContinuousSMul R₁ M₂<VAR>inst✝⁴ : ContinuousSMul R₁ M₁<VAR>α : Type u_10<VAR>inst✝³ : Monoid α<VAR>inst✝² : DistribMulAction α M₁<VAR>inst✝¹ : ContinuousConstSMul α M₁<VAR>inst✝ : SMulCommClass R₁ α M₁<VAR>c : α<VAR>x : M₁<GOAL>(toSpanSingleton R₁ (c • x)) 1 = (c • toSpanSingleton R₁ x) 1
<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✝⁶ : OrderedRing 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>x y z : P<VAR>v : V<GOAL>v +ᵥ z ∈ affineSegment R (v +ᵥ x) (v +ᵥ y) ↔ z ∈ affineSegment R x y
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : α → E<VAR>hf : Memℒp f p μ<GOAL>↑‖Memℒp.toLp f hf‖₊ = eLpNorm f 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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ V = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<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>ps : Set P<VAR>n : ℕ<VAR>inst✝ : FiniteDimensional ℝ V<VAR>hd : finrank ℝ ↥⊤.direction = n<VAR>hc : Cospherical ps<VAR>this : Nonempty ↥⊤<GOAL>∃ c, ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>x ∈ Icc a b ∪ Ici c ↔ x ∈ Ici (min a c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>a a₁ a₂ b b₁ b₂ c d : α<VAR>h₁ : c ≤ b<VAR>x : α<GOAL>a ≤ x ∧ x ≤ b ∨ c ≤ x ↔ a ≤ x ∨ c ≤ x
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>v : E<VAR>hv : v ∈ (eigenspace T μ)ᗮ<VAR>w : E<VAR>hw : w ∈ eigenspace T μ<GOAL>⟪w, T v⟫_𝕜 = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>T : E →ₗ[𝕜] E<VAR>hT : T.IsSymmetric<VAR>μ : 𝕜<VAR>v : E<VAR>hv : v ∈ (eigenspace T μ)ᗮ<VAR>w : E<VAR>hw : w ∈ eigenspace T μ<VAR>this : T w = μ • w<GOAL>⟪w, T v⟫_𝕜 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)
<VAR>G : Type w<VAR>inst✝² : TopologicalSpace G<VAR>μ : Content G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>h : ∀ (g : G) {K : Compacts G}, (fun s => ↑(μ.toFun s)) (Compacts.map (fun b => g * b) ⋯ K) = (fun s => ↑(μ.toFun s)) K<VAR>g : G<VAR>U : Opens G<GOAL>μ.innerContent ((Opens.comap (Homeomorph.mulLeft g).toContinuousMap) U) = μ.innerContent U
<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 : α<GOAL>toIocDiv hp a b • p - b = -toIocMod hp a b
<VAR>L : Language<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝³ : L.Structure M<VAR>inst✝² : L.Structure N<VAR>inst✝¹ : L.Structure P<VAR>inst✝ : L.Structure Q<VAR>f : M ↪ₑ[L] N<VAR>φ : L.Sentence<GOAL>M ⊨ φ ↔ N ⊨ φ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hst : _root_.Disjoint s (t.erase a)<GOAL>_root_.Disjoint s t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>ha : a ∉ s<VAR>hst : _root_.Disjoint s (t.erase a)<GOAL>a ∉ t.erase a ∧ _root_.Disjoint s (t.erase a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ ∫⁻ (a : α), f a ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ 1 * μ {x | 1 ≤ f x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>s : Set α<VAR>hs : ∀ x ∈ s, 1 ≤ f x<GOAL>μ s ≤ μ {x | 1 ≤ f x}
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>S.Exact ↔ Epi (imageToKernel' S.f S.g ⋯)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Abelian C<VAR>S : ShortComplex C<GOAL>Epi (kernel.lift S.g S.f ⋯) ↔ Epi (imageToKernel' S.f S.g ⋯)