ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : StrictOrderedCommRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>s : AffineSubspace R P<VAR>x y : P<VAR>v : V<VAR>hv : v ∈ s.direction<GOAL>s.SOppSide (v +ᵥ x) y ↔ s.SOppSide x y
<VAR>σ : Type u_1<VAR>R : Type u_2<VAR>τ : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>e : σ ≃ τ<VAR>h : ((rename ⇑e) φ).IsSymmetric<GOAL>φ.IsSymmetric
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : LocallyFiniteOrderBot ι<VAR>inst✝³ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>inst✝ : DecidableEq ι<GOAL>(gramSchmidtOrthonormalBasis h f).toBasis.det f = ∏ i : ι, ⟪(gramSchmidtOrthonormalBasis h f) i, f i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁸ : RCLike 𝕜<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>inst✝⁵ : LinearOrder ι<VAR>inst✝⁴ : LocallyFiniteOrderBot ι<VAR>inst✝³ : IsWellOrder ι fun x x_1 => x < x_1<VAR>inst✝² : Fintype ι<VAR>inst✝¹ : FiniteDimensional 𝕜 E<VAR>h : finrank 𝕜 E = Fintype.card ι<VAR>f : ι → E<VAR>inst✝ : DecidableEq ι<VAR>x✝ : ι<VAR>a✝ : x✝ ∈ Finset.univ<GOAL>⟪(gramSchmidtOrthonormalBasis h f) x✝, f x✝⟫_𝕜 = (gramSchmidtOrthonormalBasis h f).toBasis.toMatrix f x✝ x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : NormedRing 𝕜<VAR>f✝ f g : α → 𝕜<VAR>c : ℝ<VAR>hg : Integrable g μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>Integrable (fun x => f x * g x) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : NormedRing 𝕜<VAR>f✝ f g : α → 𝕜<VAR>c : ℝ<VAR>hg : Integrable g μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<GOAL>∀ᵐ (a : α) ∂μ, ‖f a * g a‖ ≤ (c • fun a => ‖g a‖) a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : NormedRing 𝕜<VAR>f✝ f g : α → 𝕜<VAR>c : ℝ<VAR>hg : Integrable g μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>x : α<VAR>hx : ‖f x‖ ≤ c<GOAL>‖f x * g x‖ ≤ (c • fun a => ‖g a‖) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝³ : MeasurableSpace δ<VAR>inst✝² : NormedAddCommGroup β<VAR>inst✝¹ : NormedAddCommGroup γ<VAR>𝕜 : Type u_5<VAR>inst✝ : NormedRing 𝕜<VAR>f✝ f g : α → 𝕜<VAR>c : ℝ<VAR>hg : Integrable g μ<VAR>hf : AEStronglyMeasurable f μ<VAR>hf_bound : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ c<VAR>x : α<VAR>hx : ‖f x‖ ≤ c<GOAL>‖f x * g x‖ ≤ c * ‖g x‖
<VAR>N : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝² : Group N<VAR>inst✝¹ : Group G<VAR>inst✝ : Group H<VAR>φ : G →* MulAut N<VAR>g : G<VAR>n : N<GOAL>inl ((φ g)⁻¹ n) = inr g⁻¹ * inl n * inr g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>l : List α<VAR>inst✝ : Fintype α<VAR>x : α<VAR>hx : x ∈ l.formPerm.support<VAR>hx' : x ∈ {x | l.formPerm x ≠ x}<GOAL>x ∈ l.toFinset
<VAR>𝕜 : Type u_1<VAR>inst✝³ : OrderedSemiring 𝕜<VAR>E : Type u_2<VAR>inst✝² : AddCommMonoid E<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : Module 𝕜 E<VAR>K : ProperCone 𝕜 E<GOAL>0 ∈ ↑K
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H✝ K : Subgroup G<VAR>S T : Set G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<VAR>H'' : Subgroup ↥H := comap H.subtype H'<VAR>this : H' = map H.subtype H''<GOAL>∃ S, ↑(map H.subtype H'') * S = ↑H ∧ Nat.card ↥(map H.subtype H'') * Nat.card ↑S = Nat.card ↥H
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H✝ K : Subgroup G<VAR>S✝ T : Set G<VAR>H' H : Subgroup G<VAR>h : H' ≤ H<VAR>H'' : Subgroup ↥H := comap H.subtype H'<VAR>this : H' = map H.subtype H''<VAR>S : Set ↥H<VAR>cmem : S ∈ rightTransversals ↑H''<GOAL>∃ S, ↑(map H.subtype H'') * S = ↑H ∧ Nat.card ↥(map H.subtype H'') * Nat.card ↑S = Nat.card ↥H
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => p * z ^ (p - 1) * (1 - ε z) + z ^ (p - 1) / log z ^ 2) ~[atTop] fun z => p * z ^ (p - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => p * z ^ (p - 1) * (1 - ε z)) ~[atTop] fun z => p * z ^ (p - 1)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(fun z => z ^ (p - 1) / log z ^ 2) =o[atTop] fun z => p * z ^ (p - 1)
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>inst✝¹ : UniformSpace F<VAR>inst✝ : UniformAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<GOAL>instUniformSpace σ F 𝔖₁ ≤ instUniformSpace σ F 𝔖₂
<VAR>𝕜₁ : Type u_1<VAR>𝕜₂ : Type u_2<VAR>inst✝⁸ : NormedField 𝕜₁<VAR>inst✝⁷ : NormedField 𝕜₂<VAR>σ : 𝕜₁ →+* 𝕜₂<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module 𝕜₁ E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : AddCommGroup F<VAR>inst✝² : Module 𝕜₂ F<VAR>𝔖₁ 𝔖₂ : Set (Set E)<VAR>inst✝¹ : UniformSpace F<VAR>inst✝ : UniformAddGroup F<VAR>h : 𝔖₂ ⊆ 𝔖₁<GOAL>UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖₁) ≤ UniformSpace.comap DFunLike.coe (UniformOnFun.uniformSpace E F 𝔖₂)
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : Fintype α<VAR>s t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq α<VAR>h : s.card = t.card<GOAL>(fun x => x + t.dens) (s \ t).dens = (fun x => x + t.dens) (t \ s).dens
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<VAR>v : Set E<VAR>v_nhd : v ∈ 𝓝[insert x s] x<VAR>vs : v ⊆ insert x s<VAR>hv : ContDiffOn 𝕜 (↑m) f v<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<VAR>v : Set E<VAR>v_nhd : v ∈ 𝓝[insert x s] x<VAR>vs : v ⊆ insert x s<VAR>hv : ContDiffOn 𝕜 (↑m) f v<VAR>xmem : x ∈ f ⁻¹' u ∩ v<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<VAR>v : Set E<VAR>v_nhd : v ∈ 𝓝[insert x s] x<VAR>vs : v ⊆ insert x s<VAR>hv : ContDiffOn 𝕜 (↑m) f v<VAR>xmem : x ∈ f ⁻¹' u ∩ v<VAR>this : f ⁻¹' u ∈ 𝓝[insert x s] x<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<VAR>v : Set E<VAR>v_nhd : v ∈ 𝓝[insert x s] x<VAR>vs : v ⊆ insert x s<VAR>hv : ContDiffOn 𝕜 (↑m) f v<VAR>xmem : x ∈ f ⁻¹' u ∩ v<VAR>this : f ⁻¹' u ∈ 𝓝[insert x s] x<VAR>Z : ∃ u_1 ∈ 𝓝[insert x (f ⁻¹' u ∩ v)] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u_1<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<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>s : Set E<VAR>t : Set F<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>hg : ContDiffWithinAt 𝕜 n g t (f x)<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>st : s ⊆ f ⁻¹' t<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set F<VAR>u_nhd : u ∈ 𝓝[insert (f x) t] f x<VAR>left✝ : u ⊆ insert (f x) t<VAR>hu : ContDiffOn 𝕜 (↑m) g u<VAR>v : Set E<VAR>v_nhd : v ∈ 𝓝[insert x s] x<VAR>vs : v ⊆ insert x s<VAR>hv : ContDiffOn 𝕜 (↑m) f v<VAR>xmem : x ∈ f ⁻¹' u ∩ v<VAR>this✝ : f ⁻¹' u ∈ 𝓝[insert x s] x<VAR>Z : ∃ u_1 ∈ 𝓝[insert x (f ⁻¹' u ∩ v)] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u_1<VAR>this : 𝓝[f ⁻¹' u ∩ v] x = 𝓝[insert x s] x<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (g ∘ f) p u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<GOAL>μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<GOAL>μ.rnDeriv (ν + ν') =ᶠ[ae ν] μ.rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<GOAL>(μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')<GOAL>(μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν<GOAL>(μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν<GOAL>(μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν<VAR>h₃ : (μ.singularPart ν').rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν<GOAL>(μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν ν' : Measure α<VAR>inst✝² : SigmaFinite μ<VAR>inst✝¹ : SigmaFinite ν<VAR>inst✝ : SigmaFinite ν'<VAR>hνν' : ν ⟂ₘ ν'<VAR>h_ac : ν ≪ ν + ν'<VAR>h₁ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν') =ᶠ[ae (ν + ν')] (μ.singularPart ν').rnDeriv (ν + ν') + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv (ν + ν')<VAR>h₂ : (μ.singularPart ν' + ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν =ᶠ[ae ν] (μ.singularPart ν').rnDeriv ν + (ν'.withDensity (μ.rnDeriv ν')).rnDeriv ν<GOAL>μ.singularPart ν' ⟂ₘ ν'
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<GOAL>IsJacobson R[X]
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<GOAL>∀ (P : Ideal R[X]), P.IsPrime → P.jacobson = P
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<VAR>J : Ideal (↥R')[X] := map (mapRingHom i) I<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<VAR>J : Ideal (↥R')[X] := map (mapRingHom i) I<VAR>h_surj : Function.Surjective ⇑(mapRingHom i)<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<VAR>J : Ideal (↥R')[X] := map (mapRingHom i) I<VAR>h_surj : Function.Surjective ⇑(mapRingHom i)<VAR>this : J.IsPrime<GOAL>I.jacobson = I
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<VAR>J : Ideal (↥R')[X] := map (mapRingHom i) I<VAR>h_surj : Function.Surjective ⇑(mapRingHom i)<VAR>this : J.IsPrime<GOAL>J.jacobson = J
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : IsDomain S<VAR>Rₘ : Type u_3<VAR>Sₘ : Type u_4<VAR>inst✝¹ : CommRing Rₘ<VAR>inst✝ : CommRing Sₘ<VAR>hR : IsJacobson R<VAR>I : Ideal R[X]<VAR>hI : I.IsPrime<VAR>R' : Subring (R[X] ⧸ I) := ((Quotient.mk I).comp C).range<VAR>i : R →+* ↥R' := ((Quotient.mk I).comp C).rangeRestrict<VAR>hi : Function.Surjective ⇑i<VAR>hi' : RingHom.ker (mapRingHom i) ≤ I<VAR>R'_jacob : IsJacobson ↥R'<VAR>J : Ideal (↥R')[X] := map (mapRingHom i) I<VAR>h_surj : Function.Surjective ⇑(mapRingHom i)<VAR>this : J.IsPrime<GOAL>∀ (x : ↥R'), C x ∈ J → x = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedCommMonoidWithZero α<VAR>a b c d x y z : α<VAR>n : ℕ<GOAL>0 ≤ a
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb : limsup v f ≤ b<GOAL>limsup (u + v) f ≤ a + b
<VAR>α✝ : Type u_1<VAR>inst✝ : TopologicalSpace α✝<VAR>α : Type u_2<VAR>f : Filter α<VAR>u v : α → EReal<VAR>a b : EReal<VAR>ha : limsup u f < a<VAR>hb✝ : limsup v f ≤ b<VAR>hb : limsup v f < b<GOAL>limsup (u + v) f ≤ a + b