ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>m' : MeasurableSpace α<VAR>left✝¹ : CountablyGenerated α<VAR>left✝ : MeasurableSpace.SeparatesPoints α<VAR>m'le : m' ≤ m<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>α : Type u_5<VAR>m : MeasurableSpace α<VAR>inst✝ : CountablySeparated α<VAR>m' : MeasurableSpace α<VAR>left✝³ : CountablyGenerated α<VAR>left✝² : MeasurableSpace.SeparatesPoints α<VAR>m'le : m' ≤ m<VAR>τ : TopologicalSpace α<VAR>left✝¹ : SecondCountableTopology α<VAR>left✝ : T4Space α<VAR>τm' : BorelSpace α<GOAL>∃ τ, SecondCountableTopology α ∧ T4Space α ∧ OpensMeasurableSpace α
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹² : CommSemiring R<VAR>inst✝¹¹ : Nontrivial R<VAR>inst✝¹⁰ : StarRing R<VAR>inst✝⁹ : MetricSpace R<VAR>inst✝⁸ : TopologicalSemiring R<VAR>inst✝⁷ : ContinuousStar R<VAR>inst✝⁶ : NonUnitalRing A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : TopologicalSpace A<VAR>inst✝³ : Module R A<VAR>inst✝² : IsScalarTower R A A<VAR>inst✝¹ : SMulCommClass R A A<VAR>inst✝ : NonUnitalContinuousFunctionalCalculus R p<VAR>f✝ g : R → R<VAR>a✝ : A<VAR>hf : autoParam (ContinuousOn f✝ (σₙ R a✝)) _auto✝<VAR>hf0 : autoParam (f✝ 0 = 0) _auto✝<VAR>hg : autoParam (ContinuousOn g (σₙ R a✝)) _auto✝<VAR>hg0 : autoParam (g 0 = 0) _auto✝<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>f : R → R<VAR>a : A<VAR>ha : ¬p a<GOAL>cfcₙ f a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : α → Part β<VAR>x : Part α<VAR>g : β → γ<GOAL>map g (x.bind f) = x.bind fun y => map g (f y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ✝ : Type u_3<VAR>γ : Type u_4<VAR>f : α → Part β<VAR>x : Part α<VAR>g : β → γ<GOAL>(x.bind fun x => (f x).bind (some ∘ g)) = x.bind fun y => map g (f y)
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝³ : Category.{v', u'} A<VAR>inst✝² : ConcreteCategory A<VAR>F₁ F₂ F₃ : Cᵒᵖ ⥤ A<VAR>f₁ : F₁ ⟶ F₂<VAR>f₂ : F₂ ⟶ F₃<VAR>inst✝¹ : IsLocallySurjective J f₁<VAR>inst✝ : IsLocallyInjective J (f₁ ≫ f₂)<GOAL>IsLocallyInjective J f₂
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : (i : ↑↑s) → β ↑i<VAR>n : ι<VAR>hn : n ∈ s<GOAL>((mk β s) f) n = f ⟨n, hn⟩
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝¹ : (i : ι) → AddCommMonoid (β i)<VAR>inst✝ : DecidableEq ι<VAR>s : Finset ι<VAR>f : (i : ↑↑s) → β ↑i<VAR>n : ι<VAR>hn : n ∈ s<GOAL>(if H : n ∈ s then f ⟨n, H⟩ else 0) = f ⟨n, hn⟩
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<GOAL>A.topologicalClosure = ⊤
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<GOAL>∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<GOAL>∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<GOAL>∀ (x : C(X, 𝕜)), x ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<VAR>h_f_re : I f_re ∈ A.topologicalClosure<VAR>h_f_im : I f_im ∈ A.topologicalClosure<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<VAR>h_f_re : I f_re ∈ A.topologicalClosure<VAR>h_f_im : I f_im ∈ A.topologicalClosure<VAR>this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure.toSubalgebra<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<VAR>h_f_re : I f_re ∈ A.topologicalClosure<VAR>h_f_im : I f_im ∈ A.topologicalClosure<VAR>this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure<GOAL>f ∈ A.topologicalClosure
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<VAR>h_f_re : I f_re ∈ A.topologicalClosure<VAR>h_f_im : I f_im ∈ A.topologicalClosure<VAR>this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure<VAR>a✝ : X<GOAL>f a✝ = (I f_re + RCLike.I • I f_im) a✝
<VAR>𝕜 : Type u_1<VAR>X : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : StarSubalgebra 𝕜 C(X, 𝕜)<VAR>hA : A.SeparatesPoints<VAR>I : C(X, ℝ) →ₗ[ℝ] C(X, 𝕜) := ContinuousLinearMap.compLeftContinuous ℝ X ofRealCLM<VAR>key : LinearMap.range I ≤ (Submodule.restrictScalars ℝ (Subalgebra.toSubmodule A.toSubalgebra)).topologicalClosure<VAR>f : C(X, 𝕜)<VAR>f_re : C(X, ℝ) := { toFun := ⇑re, continuous_toFun := ⋯ }.comp f<VAR>f_im : C(X, ℝ) := { toFun := ⇑im, continuous_toFun := ⋯ }.comp f<VAR>h_f_re : I f_re ∈ A.topologicalClosure<VAR>h_f_im : I f_im ∈ A.topologicalClosure<VAR>this : I f_re + RCLike.I • I f_im ∈ A.topologicalClosure<VAR>a✝ : X<GOAL>(I f_re + RCLike.I • I f_im) a✝ = f a✝
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<GOAL>Nonempty (G →g F)
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<VAR>val✝ : Fintype W<GOAL>Nonempty (G →g F)
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<VAR>val✝ : Fintype W<VAR>this : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')<GOAL>Nonempty (G →g F)
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<VAR>val✝ : Fintype W<VAR>this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')<VAR>this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')<GOAL>Nonempty (G →g F)
<VAR>V : Type u<VAR>W : Type v<VAR>G : SimpleGraph V<VAR>F : SimpleGraph W<VAR>inst✝ : Finite W<VAR>h : (G' : G.Subgraph) → G'.verts.Finite → G'.coe →g F<VAR>val✝ : Fintype W<VAR>this✝ : ∀ (G' : G.Finsubgraphᵒᵖ), Nonempty ((G.finsubgraphHomFunctor F).obj G')<VAR>this : (G' : G.Finsubgraphᵒᵖ) → Fintype ((G.finsubgraphHomFunctor F).obj G')<VAR>u : (j : G.Finsubgraphᵒᵖ) → (G.finsubgraphHomFunctor F).obj j<VAR>hu : u ∈ (G.finsubgraphHomFunctor F).sections<GOAL>Nonempty (G →g F)
<VAR>α : Type u_1<VAR>n : ℕ<VAR>a : α<VAR>l : List α<GOAL>powersetCardAux (n + 1) (a :: l) = powersetCardAux (n + 1) l ++ List.map (cons a) (powersetCardAux n l)
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a b : G<VAR>n : ℤ<GOAL>a * b ^ n * b = a * b ^ (n + 1)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>X ⊆ M.closure Y
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<VAR>hXY : X ⊆ Y<VAR>hX : autoParam (X ⊆ M.E) _auto✝<GOAL>X ⊆ M.closure (Y ∩ M.E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>cmpα : α → α → Ordering<VAR>cmpβ : β → β → Ordering<VAR>f : α → β<VAR>inst✝ : IsMonotone cmpα cmpβ f<VAR>c✝ : RBColor<VAR>a : RBNode α<VAR>x : α<VAR>b : RBNode α<VAR>ax : All (fun x_1 => cmpLT cmpα x_1 x) a<VAR>xb : All (fun x_1 => cmpLT cmpα x x_1) b<VAR>ha : Ordered cmpα a<VAR>hb : Ordered cmpα b<GOAL>Ordered cmpβ (map f (node c✝ a x b))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>h₂ : ComputablePred q<VAR>f : α → β<VAR>c : Computable f<VAR>hf : ∀ (a : α), p a ↔ q (f a)<GOAL>ComputablePred p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>p : α → Prop<VAR>q : β → Prop<VAR>h₂ : ComputablePred q<VAR>f : α → β<VAR>c : Computable f<VAR>hf : ∀ (a : α), p a ↔ q (f a)<GOAL>ComputablePred fun a => q (f a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>p : α → Prop<VAR>f : α → β<VAR>c : Computable f<VAR>g : β → Bool<VAR>hg : Computable g<VAR>h₂ : ComputablePred fun a => g a = true<VAR>hf : ∀ (a : α), p a ↔ (fun a => g a = true) (f a)<GOAL>ComputablePred fun a => (fun a => g a = true) (f a)
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 < z i<GOAL>(∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 < z i<VAR>this : (∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i / z i)⁻¹ ≤ ∏ i ∈ s, z i ^ (fun i => w i / ∑ i ∈ s, w i) i<GOAL>(∑ i ∈ s, w i) / ∑ i ∈ s, w i / z i ≤ (∏ i ∈ s, z i ^ w i) ^ (∑ i ∈ s, w i)⁻¹
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 < z i<GOAL>∀ i ∈ s, 0 < (fun i => w i / ∑ i ∈ s, w i) i
<VAR>ι✝ : Type u<VAR>s✝ : Finset ι✝<VAR>ι : Type u_1<VAR>s : Finset ι<VAR>hs : s.Nonempty<VAR>w z : ι → ℝ<VAR>hw : ∀ i ∈ s, 0 < w i<VAR>hw' : 0 < ∑ i ∈ s, w i<VAR>hz : ∀ i ∈ s, 0 < z i<GOAL>∑ i ∈ s, (fun i => w i / ∑ i ∈ s, w i) i = 1
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<GOAL>(PowerSeries.coeff A (n + 1)) ((PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (exp A - 1)) = (PowerSeries.coeff A (n + 1)) (PowerSeries.X * (rescale t) (exp A))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), (PowerSeries.coeff A (x, n + 1 - x).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (x, n + 1 - x).2) (exp A - 1) + (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).1) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1, n + 1 - (n + 1)).2) (exp A - 1) = t ^ n * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = t ^ n * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = t ^ n * (algebraMap ℚ A) (1 / ↑n !)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>(algebraMap ℚ A) ↑(n + 1)! * ∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = (algebraMap ℚ A) ↑(n + 1)! * (t ^ n * (algebraMap ℚ A) (1 / ↑n !))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>(algebraMap ℚ A) ↑(n + 1)! * ∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = t ^ n * (algebraMap ℚ A) (↑(n + 1)! * (1 / ↑n !))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>(algebraMap ℚ A) ↑(n + 1)! * ∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = t ^ n * (algebraMap ℚ A) (↑((n + 1) * n !) * (1 / ↑n !))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>(algebraMap ℚ A) ↑(n + 1)! * ∑ x ∈ range (n + 1), (PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1) = (aeval t) ((monomial n) (↑n + 1))
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>∑ i ∈ range (n + 1), (algebraMap ℚ A) ↑(n + 1)! * ((PowerSeries.coeff A i) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - i)) (exp A - 1)) = ∑ x ∈ range (n + 1), (aeval t) (↑((n + 1).choose x) • bernoulli x)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<GOAL>∀ x ∈ range (n + 1), (algebraMap ℚ A) ↑(n + 1)! * ((PowerSeries.coeff A x) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - x)) (exp A - 1)) = (aeval t) (↑((n + 1).choose x) • bernoulli x)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<VAR>i : ℕ<VAR>hi : i ∈ range (n + 1)<GOAL>(algebraMap ℚ A) ↑(n + 1)! * ((PowerSeries.coeff A i) (PowerSeries.mk fun n => (aeval t) ((1 / ↑n !) • bernoulli n)) * (PowerSeries.coeff A (n + 1 - i)) (exp A - 1)) = (aeval t) (↑((n + 1).choose i) • bernoulli i)
<VAR>A : Type u_1<VAR>inst✝¹ : CommRing A<VAR>inst✝ : Algebra ℚ A<VAR>t : A<VAR>n : ℕ<VAR>hnp1 : IsUnit ↑(n + 1)!<VAR>i : ℕ<VAR>hi : i ∈ range (n + 1)<GOAL>(algebraMap ℚ A) (↑(n + 1)! * (↑i !)⁻¹ * (↑(n + 1 - i)!)⁻¹) * (aeval t) (bernoulli i) = (algebraMap ℚ A) (↑(n + 1)! / (↑i ! * ↑(n + 1 - i)!)) * (aeval t) (bernoulli i)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : x ∉ tsupport f<GOAL>HasStrictFDerivAt f 0 x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : f =ᶠ[𝓝 x] 0<GOAL>HasStrictFDerivAt f 0 x
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U)<VAR>U : C<VAR>t : (forget A).obj (F.obj (op U))<GOAL>imageSieve f ((f.app (op U)) t) ∈ J.sieves U
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝¹ : Category.{v', u'} A<VAR>inst✝ : ConcreteCategory A<VAR>F G : Cᵒᵖ ⥤ A<VAR>f : F ⟶ G<VAR>H : ∀ (U : Cᵒᵖ), Function.Surjective ⇑(f.app U)<VAR>U : C<VAR>t : (forget A).obj (F.obj (op U))<GOAL>⊤ ∈ J.sieves U
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hg : StrictConcaveOn ℝ s g<VAR>hgc : ContinuousOn g s<VAR>hsc : IsClosed s<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>hgi : Integrable (g ∘ f) μ<GOAL>f =ᶠ[ae μ] const α (⨍ (x : α), f x ∂μ) ∨ ⨍ (x : α), g (f x) ∂μ < g (⨍ (x : α), f x ∂μ)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<GOAL>cofinite = atTop
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<GOAL>cofinite ≤ atTop
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>l : Filter α<VAR>N : ℕ<VAR>x✝ : True<GOAL>Ici N ∈ cofinite
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(aeval x) (hermite n) = (-1) ^ n * deriv^[n] (fun y => Real.exp (-(y ^ 2 / 2))) x / Real.exp (-(x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(aeval x) (hermite n) = (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2))) / Real.exp (-(x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(aeval x) (hermite n) * Real.exp (-x ^ 2 / 2) = (-1) ^ n * ((-1) ^ n * (aeval x) (hermite n) * Real.exp (-x ^ 2 / 2))
<VAR>n : ℕ<VAR>x : ℝ<GOAL>(-1) ^ n ≠ 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>p.mirror.mirror.coeff n = p.coeff n
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a : α<GOAL>⋃ n, Ico (a + n • p) (a + (n + 1) • p) = univ
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<GOAL>∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a ≤ b - toIcoDiv hp a b • p<VAR>hr : b - toIcoDiv hp a b • p < a + p<GOAL>∃ i, b ∈ Ico (a + i • p) (a + (i + 1) • p)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a ≤ b - toIcoDiv hp a b • p<VAR>hr : b - toIcoDiv hp a b • p < a + p<GOAL>b < a + (toIcoDiv hp a b + 1) • p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a ≤ b - toIcoDiv hp a b • p<VAR>hr : b - toIcoDiv hp a b • p < a + p<GOAL>b < a + toIcoDiv hp a b • p + p
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedAddCommGroup α<VAR>inst✝ : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b : α<VAR>hl : a ≤ b - toIcoDiv hp a b • p<VAR>hr : b - toIcoDiv hp a b • p < a + p<GOAL>a + toIcoDiv hp a b • p + p = a + p + toIcoDiv hp a b • p
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u}<GOAL>lift.{max (u + 1) v, u} c < univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u}<VAR>this : lift.{max (u + 1) v, u + 1} (lift.{u + 1, u} c) < lift.{max (u + 1) v, u + 1} univ.{u, u + 1}<GOAL>lift.{max (u + 1) v, u} c < univ.{u, v}
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>c : Cardinal.{u}<VAR>this : lift.{max (u + 1) v, u} c < univ.{u, v}<GOAL>lift.{max (u + 1) v, u} c < univ.{u, v}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n : ℕ<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>a b : R<GOAL>∑ s : Finset (Fin n), a ^ s.card * b ^ (n - s.card) = (a + b) ^ n
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : AddMonoid A<GOAL>closure {0} = ⊥
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Perm α<VAR>s✝ t : Set α<VAR>a b x y : α<VAR>s : Finset α<VAR>hf : f.IsCycleOn ↑s<VAR>ha : a ∈ s<VAR>hb : b ∈ s<GOAL>∃ n < s.card, (f ^ n) a = b
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → β → α<VAR>S : Set β<GOAL>UniformEquicontinuousOn F S ↔ ∀ (i : ι), UniformContinuousOn (F i) S
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>inst✝ : Finite ι<VAR>F : ι → β → α<VAR>S : Set β<GOAL>(∀ (y : ι), ∀ x ∈ 𝓤 α, ∀ᶠ (x_2 : β × β) in 𝓤 β ⊓ 𝓟 (S ×ˢ S), (F y x_2.1, F y x_2.2) ∈ x) ↔ ∀ (i : ι), UniformContinuousOn (F i) S