ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<GOAL>∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ = ∫ (x : E), ∑ x_1 ∈ s, g x • (a x_1 • fun x => lineDeriv ℝ f x (v x_1)) x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<GOAL>∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ = ∫ (x : E), ∑ x_1 ∈ s, g x • (a x_1 • fun x => lineDeriv ℝ f x (v x_1)) x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<GOAL>∫ (x : E), g x • lineDeriv ℝ f x (∑ i ∈ s, a i • v i) ∂μ = ∑ i ∈ s, ∫ (a_1 : E), g a_1 • (a i • fun x => lineDeriv ℝ f x (v i)) a_1 ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<GOAL>∫ (x : E), lineDeriv ℝ f x (∑ i ∈ s, a i • v i) * g x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), lineDeriv ℝ f x (v i) * g x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<GOAL>∫ (x : E), (∑ i ∈ s, a i * (fderiv ℝ g x) (v i)) * f x ∂μ = ∑ i ∈ s, a i * ∫ (x : E), (fderiv ℝ g x) (v i) * f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<GOAL>∀ i ∈ s, Integrable (fun x => a i * ((fderiv ℝ g x) (v i) * f x)) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<VAR>i : ι<VAR>_hi : i ∈ s<VAR>L : (E →L[ℝ] ℝ) → ℝ := fun f => f (v i)<GOAL>Integrable (fun x => a i * ((L ∘ fderiv ℝ g) x * f x)) μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<VAR>i : ι<VAR>_hi : i ∈ s<VAR>L : (E →L[ℝ] ℝ) → ℝ := fun f => f (v i)<GOAL>Continuous fun x => (L ∘ fderiv ℝ g) x * f x
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : MeasurableSpace E<VAR>inst✝³ : BorelSpace E<VAR>F : Type u_2<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>C D : ℝ≥0<VAR>f g✝ : E → ℝ<VAR>s✝ : Set E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hf : LipschitzWith C f<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>a : ι → ℝ<VAR>v : ι → E<VAR>g : E → ℝ<VAR>g_smooth : ContDiff ℝ ⊤ g<VAR>g_comp : HasCompactSupport g<VAR>A : ∀ i ∈ s, Integrable (fun x => g x • (a i • fun x => lineDeriv ℝ f x (v i)) x) μ<VAR>i : ι<VAR>_hi : i ∈ s<VAR>L : (E →L[ℝ] ℝ) → ℝ := fun f => f (v i)<GOAL>HasCompactSupport fun x => (L ∘ fderiv ℝ g) x * f x
<VAR>α : Type u_1<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : DecidableEq α<VAR>A B✝ C : Finset α<VAR>hA : A.Nonempty<VAR>B : Finset α<VAR>n : ℕ<GOAL>↑(B ^ n).card ≤ (↑(A * B).card / ↑A.card) ^ n * ↑A.card
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq H<VAR>f : G →ₙ* H<VAR>hf : ∀ ⦃a b c d : G⦄, a * b = c * d → f a = f c ∧ f b = f d → a = c ∧ b = d<VAR>h : UniqueMul (Finset.image (⇑f) A) (Finset.image (⇑f) B) (f a0) (f b0)<VAR>a b : G<VAR>ha : a ∈ A<VAR>hb : b ∈ B<VAR>ab : a * b = a0 * b0<GOAL>f a * f b = f a0 * f b0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : T2Space β<GOAL>StronglyMeasurable f ↔ ∃ c, f = fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : T2Space β<VAR>hα : IsEmpty α<GOAL>StronglyMeasurable f ↔ ∃ c, f = fun x => c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : Countable ι<VAR>f g : α → β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : Nonempty β<VAR>inst✝ : T2Space β<VAR>hα : Nonempty α<GOAL>StronglyMeasurable f ↔ ∃ c, f = fun x => c
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>h : S = ⊤<VAR>x : A<GOAL>x ∈ ⊤
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S : NonUnitalStarSubalgebra R A<VAR>h : ∀ (x : A), x ∈ S<VAR>x : A<GOAL>x ∈ S ↔ x ∈ ⊤
<VAR>β : Type w<VAR>α✝ : Type w₂<VAR>γ : Type w₃<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>f : α✝ → C<VAR>g : β → C<VAR>inst✝ : HasProduct f<VAR>e : β ≃ α✝<VAR>iso : (j : β) → g j ≅ f (e j)<VAR>this : HasLimit ((Discrete.equivalence e).functor ⋙ Discrete.functor f)<VAR>α : Discrete.functor g ≅ (Discrete.equivalence e).functor ⋙ Discrete.functor f<GOAL>HasProduct g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atTop atTop<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atTop (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atTop atTop<GOAL>f a ∘ qs ≤ ↑(hf.stieltjesFunction a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atTop atTop<VAR>x : ℝ<GOAL>(f a ∘ qs) x ≤ ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x - 1 < ↑q ∧ ↑q < x<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atTop atTop<VAR>x : ℝ<GOAL>↑(hf.stieltjesFunction a) ↑(qs x) ≤ ↑(hf.stieltjesFunction a) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>IsPiSystem (⋃ a, {Ici ↑a})
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort y<VAR>s t u : Set α<GOAL>⋃ a, {Ici ↑a} = Ici '' (Rat.cast '' univ)
<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>x : Set ℝ<GOAL>x ∈ ⋃ a, {Ici ↑a} ↔ x ∈ Ici '' (Rat.cast '' univ)
<VAR>α : Type u_1<VAR>inst✝ : Group α<VAR>s✝ t s : Subgroup α<GOAL>Nat.card ↥s ∣ Nat.card α
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g✝ f : NormedAddGroupHom V₁ V₂<VAR>K : AddSubgroup V₂<VAR>C C' : ℝ<VAR>h : f.SurjectiveOnWith K C<VAR>H : C ≤ C'<VAR>g : V₁<VAR>k_in : f g ∈ K<VAR>hg : ‖g‖ ≤ C * ‖f g‖<GOAL>∃ g_1, f g_1 = f g ∧ ‖g_1‖ ≤ C' * ‖f g‖
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f✝ g✝ f : NormedAddGroupHom V₁ V₂<VAR>K : AddSubgroup V₂<VAR>C C' : ℝ<VAR>h : f.SurjectiveOnWith K C<VAR>H : C ≤ C'<VAR>g : V₁<VAR>k_in : f g ∈ K<VAR>hg : ‖g‖ ≤ C * ‖f g‖<GOAL>‖g‖ ≤ C' * ‖f g‖
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<GOAL>¬IsField (𝓞 K)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<VAR>h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))<GOAL>¬IsField (𝓞 K)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝¹ : Field K<VAR>inst✝ : Field L<VAR>nf : NumberField K<VAR>h_inj : Injective ⇑(algebraMap ℤ (𝓞 K))<VAR>hf : IsField (𝓞 K)<GOAL>False
<VAR>a b c : EReal<VAR>h₁ : c ≠ ⊥<VAR>h₂ : c ≠ ⊤<VAR>h₃ : c ≠ 0<GOAL>a * c * (b * c)⁻¹ = a * b⁻¹
<VAR>a b c : EReal<VAR>h₁ : c ≠ ⊥<VAR>h₂ : c ≠ ⊤<VAR>h₃ : c ≠ 0<GOAL>a * (c * (b⁻¹ * c⁻¹)) = a * b⁻¹
<VAR>a b c : EReal<VAR>h₁ : c ≠ ⊥<VAR>h₂ : c ≠ ⊤<VAR>h₃ : c ≠ 0<GOAL>c * (b⁻¹ * c⁻¹) = b⁻¹
<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>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2<GOAL>(fun p => ∑ i ∈ u, A i p.1 - ∑ i ∈ u, A i p.2 - (∑ i ∈ u, A' i) (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2
<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>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, (fun p => A i p.1 - A i p.2 - (A' i) (p.1 - p.2)) =o[𝓝 (x, x)] fun p => p.1 - p.2<VAR>x✝ : E × E<GOAL>∑ i ∈ u, A i x✝.1 - ∑ i ∈ u, A i x✝.2 - (∑ i ∈ u, A' i) (x✝.1 - x✝.2) = ∑ i ∈ u, (A i x✝.1 - A i x✝.2 - (A' i) (x✝.1 - x✝.2))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>f : R →+* S<VAR>x y : 𝕎 R<GOAL>mapFun (⇑f) (-x) = -mapFun (⇑f) x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>s✝ s₁ s₂ : Finset ι<VAR>i : ι<VAR>a✝ : α<VAR>f g : ι → α<VAR>inst✝ : CommSemiring α<VAR>a b : α<VAR>s : Finset ι<GOAL>∑ t ∈ s.powerset, a ^ t.card * b ^ (s.card - t.card) = (a + b) ^ s.card
<VAR>α : Type u_1<VAR>inst✝ : TopologicalSpace α<VAR>s : Set EReal<GOAL>(∃ i, True ∧ Ioi ↑i ⊆ s) ↔ ∃ y, Ioi ↑y ⊆ s
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSemisimpleRing R<VAR>I : Ideal R<GOAL>∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSemisimpleRing R<VAR>I J : Ideal R<VAR>h : IsCompl I J<GOAL>∃ e, IsIdempotentElem e ∧ I = Ideal.span {e}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>S : Type u_3<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : Ring S<VAR>M : Type u_4<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>m : Submodule R M<VAR>N : Type u_5<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>inst✝ : IsSemisimpleRing R<VAR>J : Ideal R<VAR>f : Module.End R R<VAR>idem : IsIdempotentElem f<VAR>h : IsCompl (LinearMap.range f) J<GOAL>∃ e, IsIdempotentElem e ∧ LinearMap.range f = Ideal.span {e}
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>g g' : G<VAR>f : ℤ → M<VAR>hf : HasProd f m<VAR>this : Injective Int.negSucc<GOAL>HasProd (fun n => f ↑n * f (Int.negSucc n)) m
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>g g' : G<VAR>f : ℤ → M<VAR>hf : HasProd f m<VAR>this : Injective Int.negSucc<VAR>u : Finset ℤ<GOAL>∃ v, ∀ (v' : Finset ℕ), v ⊆ v' → ∃ u', u ⊆ u' ∧ ∏ x ∈ u', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>g g' : G<VAR>f : ℤ → M<VAR>hf : HasProd f m<VAR>this : Injective Int.negSucc<VAR>u : Finset ℤ<VAR>v' : Finset ℕ<VAR>hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'<VAR>x : ℤ<VAR>hx : x ∈ u<GOAL>x ∈ image Nat.cast v' ∪ image Int.negSucc v'
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝ : CommGroup G<VAR>g g' : G<VAR>f : ℤ → M<VAR>hf : HasProd f m<VAR>this : Injective Int.negSucc<VAR>u : Finset ℤ<VAR>v' : Finset ℕ<VAR>hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'<GOAL>∏ x ∈ image Nat.cast v' ∪ image Int.negSucc v', f x = ∏ b ∈ v', f ↑b * f (Int.negSucc b)
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
<VAR>p : ℕ<VAR>hp : Nat.Prime p<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hdiv : p ∣ 0<GOAL>(expand R p) (cyclotomic 0 R) = cyclotomic (0 * p) R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hzero : n > 0<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hzero : n > 0<VAR>this : NeZero n<GOAL>(expand R p) (cyclotomic n R) = cyclotomic (n * p) R
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hzero : n > 0<VAR>this : NeZero n<GOAL>(expand ℤ p) (cyclotomic n ℤ) = cyclotomic (n * p) ℤ
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hzero : n > 0<VAR>this : NeZero n<GOAL>cyclotomic (n * p) ℤ ∣ (expand ℤ p) (cyclotomic n ℤ)
<VAR>p n : ℕ<VAR>hp : Nat.Prime p<VAR>hdiv : p ∣ n<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>hzero : n > 0<VAR>this : NeZero n<GOAL>((expand ℤ p) (cyclotomic n ℤ)).natDegree ≤ (cyclotomic (n * p) ℤ).natDegree
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<GOAL>dist x y ≤ dist x z + dist y z
<VAR>n : ℕ<VAR>x : ℤ × ℤ<GOAL>x ∈ box 0 ↔ max x.1.natAbs x.2.natAbs = 0
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<GOAL>x ∈ box (n + 1) ↔ max x.1.natAbs x.2.natAbs = n + 1
<VAR>n✝ : ℕ<VAR>x : ℤ × ℤ<VAR>n : ℕ<GOAL>((-1 ≤ x.1 + ↑n ∧ -1 ≤ x.2 + ↑n) ∧ x.1 ≤ ↑n + 1 ∧ x.2 ≤ ↑n + 1) ∧ (-↑n ≤ x.1 → -↑n ≤ x.2 → x.1 ≤ ↑n → ↑n < x.2) ↔ max x.1.natAbs x.2.natAbs = n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : Nonempty α<GOAL>l.Subsingleton ↔ ∃ a, l ≤ pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Nonempty α<GOAL>⊥.Subsingleton ↔ ∃ a, ⊥ ≤ pure a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : Filter α<VAR>inst✝ : Nonempty α<VAR>hbot : l.NeBot<GOAL>l.Subsingleton ↔ ∃ a, l ≤ pure a
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>(rename f) ((monomial d) r) = (monomial (Finsupp.mapDomain f d)) r
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>((algebraMap R (MvPolynomial τ R)) r * d.prod fun i k => (X ∘ f) i ^ k) = C r * d.prod fun a m => X (f a) ^ m
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>∀ (b : τ), X b ^ 0 = 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>α : Type u_3<VAR>R : Type u_4<VAR>S : Type u_5<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : σ → τ<VAR>d : σ →₀ ℕ<VAR>r : R<GOAL>∀ (b : τ) (m₁ m₂ : ℕ), X b ^ (m₁ + m₂) = X b ^ m₁ * X b ^ m₂
<VAR>z : ℂ<GOAL>↑z.im = (z - (starRingEnd ℂ) z) / (2 * I)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>(span ℕ s).toAddSubmonoid = AddSubmonoid.closure s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>(span ℕ s).toAddSubmonoid ≤ AddSubmonoid.closure s
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>span ℕ s ≤ AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s)
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s✝ t s : Set M<GOAL>s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))
<VAR>R : Type u_1<VAR>inst✝⁶ : Semiring R<VAR>p✝ : R[X]<VAR>r : R<VAR>p q : R[X]<VAR>S : Type u_2<VAR>inst✝⁵ : NonAssocSemiring S<VAR>inst✝⁴ : Module R S<VAR>inst✝³ : IsScalarTower R S S<VAR>inst✝² : SMulCommClass R S S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : NatPowAssoc S<VAR>x : S<VAR>m n : ℕ<GOAL>p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
<VAR>F : Type u_1<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>Z' : Type x<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<GOAL>∀ {x y : C(X, Y)}, x.Homotopic y → y.Homotopic x