ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>G' : Type u_7<VAR>G'' : Type u_8<VAR>inst✝³ : NormedLatticeAddCommGroup G''<VAR>inst✝² : NormedSpace ℝ G''<VAR>inst✝¹ : NormedLatticeAddCommGroup G'<VAR>inst✝ : NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α →ₛ G'<VAR>hf : 0 ≤ f<VAR>hfi : Integrable (↑f) μ<VAR>i : G'<VAR>hi : i ∈ Set.range ↑f<VAR>h0 : ¬i = 0<VAR>y : α<VAR>hy : ↑f y = i<GOAL>0 ≤ i
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis R S<VAR>y : S<VAR>a✝ : Nontrivial S<GOAL>∃ f, y = (aeval pb.gen) f
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : Ring S<VAR>inst✝⁵ : Algebra R S<VAR>A : Type u_4<VAR>B : Type u_5<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : IsDomain B<VAR>inst✝¹ : Algebra A B<VAR>K : Type u_6<VAR>inst✝ : Field K<VAR>pb : PowerBasis R S<VAR>y : S<VAR>a✝ : Nontrivial S<VAR>f : R[X]<VAR>left✝ : f.natDegree < pb.dim<VAR>hf : y = (aeval pb.gen) f<GOAL>∃ f, y = (aeval pb.gen) f
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hsb : IsVonNBounded ℝ s<VAR>hst : Convex ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ∈ interior s<VAR>y : E<VAR>hy : y ∈ interior t<GOAL>∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t
<VAR>E : Type u_1<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module ℝ E<VAR>inst✝³ : TopologicalSpace E<VAR>inst✝² : T1Space E<VAR>inst✝¹ : TopologicalAddGroup E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>s✝ t✝ s t : Set E<VAR>hsc : Convex ℝ s<VAR>hsb : IsVonNBounded ℝ s<VAR>hst : Convex ℝ t<VAR>htb : IsVonNBounded ℝ t<VAR>x : E<VAR>hx : x ∈ interior s<VAR>y : E<VAR>hy : y ∈ interior t<VAR>h : E ≃ₜ E := gaugeRescaleHomeomorph (-x +ᵥ s) (-y +ᵥ t) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯<GOAL>∃ e, ⇑e '' interior s = interior t ∧ ⇑e '' closure s = closure t
<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>g : E → F<VAR>c : ℝ≥0<VAR>hg : LipschitzWith c g<VAR>g0 : g 0 = 0<VAR>f : ↥(Lp E p μ)<GOAL>‖hg.compLp g0 f‖ ≤ ↑c * ‖f‖
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<GOAL>eval₂ f g (p + q) = eval₂ f g p + eval₂ f g q
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>d : 𝔸'<GOAL>HasStrictFDerivAt (fun y => c y * d) (d • c') x
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>d : 𝔸'<GOAL>d • c' = c'.smulRight d
<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>𝔸 : Type u_6<VAR>𝔸' : Type u_7<VAR>inst✝³ : NormedRing 𝔸<VAR>inst✝² : NormedCommRing 𝔸'<VAR>inst✝¹ : NormedAlgebra 𝕜 𝔸<VAR>inst✝ : NormedAlgebra 𝕜 𝔸'<VAR>a b : E → 𝔸<VAR>a' b' : E →L[𝕜] 𝔸<VAR>c d✝ : E → 𝔸'<VAR>c' d' : E →L[𝕜] 𝔸'<VAR>hc : HasStrictFDerivAt c c' x<VAR>d : 𝔸'<VAR>z : E<GOAL>(d • c') z = (c'.smulRight d) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f : ℕ → ℕ → α<VAR>h : Primrec (Nat.unpaired f)<GOAL>Primrec₂ f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>n : ℕ<VAR>Y : ComposableArrows D n<GOAL>Y ∈ (L.mapComposableArrows n).essImage
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{u_4, u_2} D<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : W.HasRightCalculusOfFractions<VAR>n : ℕ<VAR>Y : ComposableArrows D n<VAR>this : L.EssSurj<GOAL>Y ∈ (L.mapComposableArrows n).essImage
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>S : Set L<VAR>inst✝ : Finite ↑S<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>FiniteDimensional K ↥(adjoin K S)
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>S : Set L<VAR>inst✝ : Finite ↑S<VAR>hS : ∀ x ∈ S, IsIntegral K x<GOAL>FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)
<VAR>F : Type u_1<VAR>inst✝⁷ : Field F<VAR>E : Type u_2<VAR>inst✝⁶ : Field E<VAR>inst✝⁵ : Algebra F E<VAR>α : E<VAR>K : Type u<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra F K<VAR>L : Type u_3<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>S : Set L<VAR>inst✝ : Finite ↑S<VAR>hS : ∀ x ∈ S, IsIntegral K x<VAR>this : ∀ (x : ↑S), FiniteDimensional K ↥K⟮↑x⟯<GOAL>FiniteDimensional K ↥(⨆ i, K⟮↑i⟯)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0<GOAL>N = ⊥
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0<GOAL>∀ x ∈ N, x = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>rank_eq : ∀ {m : ℕ} (v : Fin m → ↥N), LinearIndependent R (Subtype.val ∘ v) → m = 0<VAR>x : M<VAR>hx : x ∈ N<GOAL>x = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ N<VAR>x_ne : x ≠ 0<GOAL>∃ m v, LinearIndependent R (Subtype.val ∘ v) ∧ m ≠ 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ N<VAR>x_ne : x ≠ 0<GOAL>LinearIndependent R (Subtype.val ∘ fun x_1 => ⟨x, hx⟩)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ N<VAR>x_ne : x ≠ 0<GOAL>∀ (g : Fin 1 → R), ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => ⟨x, hx⟩) i = 0 → ∀ (i : Fin 1), g i = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ N<VAR>x_ne : x ≠ 0<VAR>g : Fin 1 → R<VAR>sum_eq : ∑ i : Fin 1, g i • (Subtype.val ∘ fun x_1 => ⟨x, hx⟩) i = 0<VAR>val✝ : ℕ<VAR>hi : val✝ < 1<GOAL>g ⟨val✝, hi⟩ = 0
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁵ : Semiring R<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommMonoid M'<VAR>inst✝¹ : Module R M'<VAR>b✝ b₁ : Basis ι R M<VAR>i : ι<VAR>c : R<VAR>x✝ : M<VAR>inst✝ : NoZeroDivisors R<VAR>b : Basis ι R M<VAR>N : Submodule R M<VAR>x : M<VAR>hx : x ∈ N<VAR>x_ne : x ≠ 0<VAR>g : Fin 1 → R<VAR>val✝ : ℕ<VAR>hi : val✝ < 1<VAR>sum_eq : g 0 • (Subtype.val ∘ fun x_1 => ⟨x, hx⟩) 0 = 0<GOAL>g ⟨val✝, hi⟩ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<GOAL>Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>h : Finite ↑(s ∪ t)<GOAL>Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s t : Set α<VAR>h : Infinite ↑(s ∪ t)<GOAL>Nat.card ↑(s ∪ t) ≤ Nat.card ↑s + Nat.card ↑t
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>IsCompl s.direction (mk' p s.directionᗮ).direction
<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>s : AffineSubspace ℝ P<VAR>inst✝¹ : Nonempty ↥s<VAR>inst✝ : HasOrthogonalProjection s.direction<VAR>p : P<GOAL>IsCompl s.direction s.directionᗮ
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>w.IsReal ↔ ComplexEmbedding.IsReal w.embedding
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>w : InfinitePlace K<GOAL>w.IsReal → ComplexEmbedding.IsReal w.embedding
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>K : Type u_2<VAR>inst✝¹ : Field K<VAR>F : Type u_3<VAR>inst✝ : Field F<VAR>φ : K →+* ℂ<VAR>hφ : ComplexEmbedding.IsReal φ<GOAL>ComplexEmbedding.IsReal (mk φ).embedding
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<GOAL>⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<VAR>this : Finite ↑s<GOAL>⋃ i ∈ s, f i ≤ᶠ[l] ⋃ i ∈ s, g i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>l : Filter α<VAR>ι : Type u_2<VAR>s : Set ι<VAR>hs : s.Finite<VAR>f g : ι → Set α<VAR>hle : ∀ i ∈ s, f i ≤ᶠ[l] g i<VAR>this : Finite ↑s<GOAL>⋃ x, f ↑x ≤ᶠ[l] ⋃ x, g ↑x
<VAR>v : Multiset ℕ<VAR>h : ∀ p ∈ v, Nat.Prime p<GOAL>↑(ofNatMultiset v h).prod = v.prod
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>ε : ℝ≥0∞<VAR>εpos : ε ≠ 0<GOAL>∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>ε : ℝ≥0∞<VAR>εpos : ε ≠ 0<VAR>δ : ℕ → ℝ≥0∞<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>hδ : ∑' (i : ℕ), δ i < ε<GOAL>∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : BorelSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.WeaklyRegular<VAR>f : α → ℝ≥0∞<VAR>hf : Measurable f<VAR>ε : ℝ≥0∞<VAR>εpos : ε ≠ 0<VAR>δ : ℕ → ℝ≥0∞<VAR>δpos : ∀ (i : ℕ), 0 < δ i<VAR>hδ : ∑' (i : ℕ), δ i < ε<VAR>this : ∀ (n : ℕ), ∃ g, (∀ (x : α), ↑(SimpleFunc.eapproxDiff f n) x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), ↑(g x) ∂μ ≤ ∫⁻ (x : α), ↑(↑(SimpleFunc.eapproxDiff f n) x) ∂μ + δ n<GOAL>∃ g, (∀ (x : α), f x ≤ g x) ∧ LowerSemicontinuous g ∧ ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ + ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>f : α → β<VAR>h : s ⊆ t<VAR>h' : t.ncard ≤ s.ncard<VAR>ht : autoParam t.Finite _auto✝<GOAL>t.encard ≤ s.encard
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsAlgebraic F E<GOAL>Algebra.IsSeparable F ↥(separableClosure F E) ∧ IsPurelyInseparable (↥(separableClosure F E)) E
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContDiffOn 𝕜 (↑(n + 1)) f s ↔ DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<GOAL>DifferentiableOn 𝕜 f s ∧ ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : o ∩ insert x s ⊆ u<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this : ContDiffWithinAt 𝕜 (↑n) f' (s ∩ o) x<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this : ContDiffWithinAt 𝕜 (↑n) f' s x<GOAL>ContDiffWithinAt 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s x
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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 uX<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>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>n : ℕ<VAR>hs : UniqueDiffOn 𝕜 s<VAR>H : ContDiffOn 𝕜 (↑(n + 1)) f s<VAR>x : E<VAR>hx : x ∈ s<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>f' : E → E →L[𝕜] F<VAR>hff' : ∀ x ∈ u, HasFDerivWithinAt f (f' x) u x<VAR>hf' : ContDiffWithinAt 𝕜 (↑n) f' u x<VAR>o : Set E<VAR>o_open : IsOpen o<VAR>xo : x ∈ o<VAR>ho : s ∩ o ⊆ u<VAR>this : ContDiffWithinAt 𝕜 (↑n) f' s x<GOAL>(fun y => fderivWithin 𝕜 f s y) =ᶠ[𝓝[s] x] f'