ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>h : HasFDerivWithinAt f f' s x<VAR>α : Type u_6<VAR>l : Filter α<VAR>c : α → 𝕜<VAR>d : α → E<VAR>v : E<VAR>dtop : ∀ᶠ (n : α) in l, x + d n ∈ s<VAR>clim : Tendsto (fun n => ‖c n‖) l atTop<VAR>cdlim : Tendsto (fun n => c n • d n) l (𝓝 v)<VAR>tendsto_arg : Tendsto (fun n => x + d n) l (𝓝[s] x)<VAR>this✝⁴ : (fun y => f y - f x - f' (y - x)) =o[𝓝[s] x] fun y => y - x<VAR>this✝³ : (fun n => f (x + d n) - f x - f' (x + d n - x)) =o[l] fun n => x + d n - x<VAR>this✝² : (fun n => f (x + d n) - f x - f' (d n)) =o[l] d<VAR>this✝¹ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun n => c n • d n<VAR>this✝ : (fun n => c n • (f (x + d n) - f x - f' (d n))) =o[l] fun x => 1<VAR>L1 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n))) l (𝓝 0)<VAR>L2 : Tendsto (fun n => f' (c n • d n)) l (𝓝 (f' v))<VAR>L3 : Tendsto (fun n => c n • (f (x + d n) - f x - f' (d n)) + f' (c n • d n)) l (𝓝 (0 + f' v))<VAR>this : (fun n => c n • (f (x + d n) - f x - f' (d n)) + f' (c n • d n)) = fun n => c n • (f (x + d n) - f x)<GOAL>Tendsto (fun n => c n • (f (x + d n) - f x)) l (𝓝 (f' v))
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.8704, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.8711, u_2} D<VAR>ι : Type u_3<VAR>F G : Discrete ι ⥤ C<VAR>α : F ⟶ G<VAR>i : ι<GOAL>IsPullback (F.map { down := { down := ⋯ } }) (α.app { as := i }) (α.app { as := i }) (G.map { down := { down := ⋯ } })
<VAR>J : Type v'<VAR>inst✝³ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝¹ : Category.{?u.8704, u_1} K<VAR>D : Type u_2<VAR>inst✝ : Category.{?u.8711, u_2} D<VAR>ι : Type u_3<VAR>F G : Discrete ι ⥤ C<VAR>α : F ⟶ G<VAR>i : ι<GOAL>IsPullback (𝟙 (F.obj { as := i })) (α.app { as := i }) (α.app { as := i }) (𝟙 (G.obj { as := i }))
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<GOAL>Function.Bijective ⇑(ofTensorProduct I M)
<VAR>R✝ : Type u_1<VAR>inst✝¹⁰ : CommRing R✝<VAR>I✝ : Ideal R✝<VAR>M✝ : Type u_2<VAR>inst✝⁹ : AddCommGroup M✝<VAR>inst✝⁸ : Module R✝ M✝<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommGroup N<VAR>inst✝⁶ : Module R✝ N<VAR>R : Type u<VAR>inst✝⁵ : CommRing R<VAR>I : Ideal R<VAR>M : Type u<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : IsNoetherianRing R<VAR>ι : Type<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<VAR>f : (ι → R) →ₗ[R] M<VAR>hf : Function.Surjective ⇑f<VAR>this : IsIso (ModuleCat.ofHom (ofTensorProduct I M))<GOAL>Function.Bijective ⇑(ofTensorProduct I M)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k✝ k : Set G<VAR>x✝¹ : { x // x ∈ ↑(closure k) }<VAR>x : G<VAR>hx : x ∈ ↑(closure k)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>⟨x, hx⟩ ∈ closure (Subtype.val ⁻¹' k)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k✝ k : Set G<VAR>x✝¹ : { x // x ∈ ↑(closure k) }<VAR>x : G<VAR>hx : x ∈ ↑(closure k)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>g : G<VAR>hg : g ∈ k<GOAL>⟨g, ⋯⟩ ∈ closure (Subtype.val ⁻¹' k)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k✝ k : Set G<VAR>x✝¹ : { x // x ∈ ↑(closure k) }<VAR>x : G<VAR>hx : x ∈ ↑(closure k)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<GOAL>⟨1, ⋯⟩ ∈ closure (Subtype.val ⁻¹' k)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k✝ k : Set G<VAR>x✝¹ : { x // x ∈ ↑(closure k) }<VAR>x : G<VAR>hx : x ∈ ↑(closure k)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>g₁ : G<VAR>g₂ : g₁ ∈ closure k<VAR>hg₁ : G<VAR>hg₂ : hg₁ ∈ closure k<GOAL>⟨g₁, g₂⟩ ∈ closure (Subtype.val ⁻¹' k) → ⟨hg₁, hg₂⟩ ∈ closure (Subtype.val ⁻¹' k) → ⟨g₁ * hg₁, ⋯⟩ ∈ closure (Subtype.val ⁻¹' k)
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k✝ k : Set G<VAR>x✝¹ : { x // x ∈ ↑(closure k) }<VAR>x : G<VAR>hx : x ∈ ↑(closure k)<VAR>x✝ : ⟨x, hx⟩ ∈ ⊤<VAR>g : G<VAR>hg : g ∈ closure k<GOAL>⟨g, hg⟩ ∈ closure (Subtype.val ⁻¹' k) → ⟨g⁻¹, ⋯⟩ ∈ closure (Subtype.val ⁻¹' k)
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>h : IsNilpotent (a - b)<GOAL>IsNilpotent ((aeval a) P - (aeval b) P)
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>h : IsNilpotent (a - b)<GOAL>IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
<VAR>R✝ : Type u_1<VAR>r : R✝<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>P : R[X]<VAR>a b : S<VAR>h : IsNilpotent (a - b)<VAR>c : S<VAR>hc : eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P) = c * (a - b)<GOAL>IsNilpotent (eval a (map (algebraMap R S) P) - eval b (map (algebraMap R S) P))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>f✝ g✝ : α → E<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α → G'<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>setToFun μ T hT f ≤ setToFun μ T hT g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>f✝ g✝ : α → E<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α → G'<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<GOAL>0 ≤ setToFun μ T hT (g - f)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>f✝ g✝ : α → E<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α → G'<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>a : α<VAR>ha : f a ≤ g a<GOAL>0 a ≤ (g - f) a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>inst✝¹⁰ : NormedAddCommGroup F<VAR>inst✝⁹ : NormedSpace ℝ F<VAR>inst✝⁸ : NormedAddCommGroup F'<VAR>inst✝⁷ : NormedSpace ℝ F'<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁵ : CompleteSpace F<VAR>T✝ T' T'' : Set α → E →L[ℝ] F<VAR>C✝ C' C'' : ℝ<VAR>f✝ g✝ : α → E<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝⁴ : NormedLatticeAddCommGroup G''<VAR>inst✝³ : NormedSpace ℝ G''<VAR>inst✝² : CompleteSpace G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α → G'<VAR>hf : Integrable f μ<VAR>hg : Integrable g μ<VAR>hfg : f ≤ᶠ[ae μ] g<VAR>a : α<VAR>ha : f a ≤ g a<GOAL>f a ≤ g a
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁴ : NormedAddCommGroup E<VAR>inst✝¹³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹¹ : TopologicalSpace M<VAR>inst✝¹⁰ : ChartedSpace H M<VAR>E' : Type u_5<VAR>inst✝⁹ : NormedAddCommGroup E'<VAR>inst✝⁸ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁷ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁶ : TopologicalSpace M'<VAR>inst✝⁵ : ChartedSpace H' M'<VAR>E'' : Type u_8<VAR>inst✝⁴ : NormedAddCommGroup E''<VAR>inst✝³ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝² : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝¹ : TopologicalSpace M''<VAR>inst✝ : ChartedSpace H'' M''<VAR>f f₀ f₁ : M → M'<VAR>x : M<VAR>s t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>Is : SmoothManifoldWithCorners I M<VAR>I's : SmoothManifoldWithCorners I' M'<VAR>I''s : SmoothManifoldWithCorners I'' M''<VAR>f' f₀' f₁' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)<VAR>g' : TangentSpace I' (f x) →L[𝕜] TangentSpace I'' (g (f x))<VAR>h : ¬MDifferentiableAt I I' f x<GOAL>mfderiv I I' f x = 0
<VAR>C : Type u_1<VAR>inst✝⁸ : Category.{u_5, u_1} C<VAR>D : Type u_2<VAR>inst✝⁷ : Category.{?u.42059, u_2} D<VAR>E : Type u_3<VAR>inst✝⁶ : Category.{?u.42066, u_3} E<VAR>M : Type u_4<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : HasShift E M<VAR>X Y Z T : C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : ∀ (a : M), (shiftFunctor C a).Additive<VAR>a b c : M<VAR>α : ShiftedHom X Y a<VAR>β : ShiftedHom Y Z b<VAR>h : b + a = c<GOAL>α.comp (-β) h = -α.comp β h
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective (⇑f ∘ ⇑(renameEquiv R e))<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective ⇑f'<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective ⇑f'<VAR>this : (f'.comp MvPolynomial.C).IsIntegral<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective ⇑f'<VAR>this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp MvPolynomial.C)).IsIntegral<GOAL>(f.comp MvPolynomial.C).IsIntegral
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective ⇑f'<VAR>this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp MvPolynomial.C)).IsIntegral<GOAL>MvPolynomial.C = (renameEquiv R e).toRingEquiv.toRingHom.comp MvPolynomial.C
<VAR>n : ℕ<VAR>R : Type u_1<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsJacobson R<VAR>σ : Type u_2<VAR>inst✝¹ : _root_.Finite σ<VAR>S : Type u_3<VAR>inst✝ : Field S<VAR>f : MvPolynomial σ R →+* S<VAR>hf : Function.Surjective ⇑f<VAR>val✝ : Fintype σ<VAR>e : Fin (Fintype.card σ) ≃ σ<VAR>f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom<VAR>hf' : Function.Surjective ⇑f'<VAR>this : (f.comp ((renameEquiv R e).toRingEquiv.toRingHom.comp MvPolynomial.C)).IsIntegral<VAR>x : R<GOAL>MvPolynomial.C x = ((renameEquiv R e).toRingEquiv.toRingHom.comp MvPolynomial.C) x
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a b : α<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : s.Results b n<GOAL>m = n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a b : α<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : s.Results b n<VAR>this : s.Terminates<GOAL>m = n
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a b : α<VAR>m n : ℕ<VAR>h1 : s.Results a m<VAR>h2 : s.Results b n<VAR>this✝ this : s.Terminates<GOAL>m = n
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<GOAL>closure L = ⊤
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<GOAL>⊤ ≤ closure L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<VAR>f : C(X, ℝ)<GOAL>f ∈ closure L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ x ∈ Metric.ball f ε, x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : L.SeparatesPointsStrongly<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<GOAL>∃ x, dist x f < ε ∧ x ∈ L
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>L : Set C(X, ℝ)<VAR>nA : L.Nonempty<VAR>inf_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊓ g ∈ L<VAR>sup_mem : ∀ f ∈ L, ∀ g ∈ L, f ⊔ g ∈ L<VAR>sep : ∀ (v : X → ℝ) (x y : X), ∃ f ∈ L, f x = v x ∧ f y = v y<VAR>f : C(X, ℝ)<VAR>ε : ℝ<VAR>pos : 0 < ε<VAR>nX : Nonempty X<VAR>g : X → X → C(X, ℝ)<VAR>hg : ∀ (x y : X), g x y ∈ L<VAR>w₁ : ∀ (x y : X), (g x y) x = f x<VAR>w₂ : ∀ (x y : X), (g x y) y = f y<VAR>U : X → X → Set X := fun x y => {z | f z - ε < (g x y) z}<VAR>U_nhd_y : ∀ (x y : X), U x y ∈ 𝓝 y<VAR>ys : X → Finset X := fun x => ⋯.choose<VAR>ys_w : ∀ (x : X), ⋃ y ∈ ys x, U x y = ⊤ := fun x => Exists.choose_spec (CompactSpace.elim_nhds_subcover (U x) (U_nhd_y x))<VAR>ys_nonempty : ∀ (x : X), (ys x).Nonempty<VAR>h : X → ↑L := fun x => ⟨(ys x).sup' ⋯ fun y => g x y, ⋯⟩<VAR>lt_h : ∀ (x z : X), f z - ε < ↑(h x) z<VAR>h_eq : ∀ (x : X), ↑(h x) x = f x<VAR>W : X → Set X := fun x => {z | ↑(h x) z < f z + ε}<VAR>W_nhd : ∀ (x : X), W x ∈ 𝓝 x<GOAL>∃ x, dist x f < ε ∧ x ∈ L