ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g✝ : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>g : M →ₗ[R] M''<VAR>h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)<VAR>l : M' →ₗ[R] M''<VAR>hl : l ∘ₗ f = g<VAR>x : M<GOAL>(↑(iso S f) ∘ₗ LocalizedModule.mkLinearMap S M) x = f x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>inst✝ : LocallyFiniteOrderBot α<GOAL>Ioo a b ⊆ Iio b
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>G : Type u_4<VAR>M' : Type u_5<VAR>inst✝⁹ : NormedField R<VAR>inst✝⁸ : SeminormedAddCommGroup M<VAR>inst✝⁷ : SeminormedAddCommGroup N<VAR>inst✝⁶ : SeminormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace R M<VAR>inst✝⁴ : NormedSpace R N<VAR>inst✝³ : NormedSpace R G<VAR>inst✝² : NormedAddCommGroup M'<VAR>inst✝¹ : NormedSpace R M'<VAR>f : M →L[R] N<VAR>g : N →L[R] G<VAR>c : R<VAR>inst✝ : Subsingleton M<VAR>f' : M →L[R] N<VAR>x : M<GOAL>‖0 x‖ = ‖x‖
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝²⁶ : CommSemiring S<VAR>inst✝²⁵ : Semiring R<VAR>inst✝²⁴ : CommSemiring R'<VAR>inst✝²³ : AddCommMonoid M<VAR>inst✝²² : Algebra S R<VAR>inst✝²¹ : Algebra S R'<VAR>inst✝²⁰ : Module S M<VAR>inst✝¹⁹ : Module R M<VAR>inst✝¹⁸ : Module Rᵐᵒᵖ M<VAR>inst✝¹⁷ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝¹⁶ : IsScalarTower S R M<VAR>inst✝¹⁵ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝¹⁴ : Module R' M<VAR>inst✝¹³ : Module R'ᵐᵒᵖ M<VAR>inst✝¹² : IsCentralScalar R' M<VAR>inst✝¹¹ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝¹⁰ : Semiring A<VAR>inst✝⁹ : Algebra S A<VAR>inst✝⁸ : Algebra R' A<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R' N<VAR>inst✝⁵ : Module R'ᵐᵒᵖ N<VAR>inst✝⁴ : IsCentralScalar R' N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R' P<VAR>inst✝¹ : Module R'ᵐᵒᵖ P<VAR>inst✝ : IsCentralScalar R' P<VAR>f : M →ₗ[R'] N<VAR>x : tsze R' M<GOAL>((map f) x).snd = f x.snd
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>C₄ : Type u_4<VAR>C₁₂ : Type u_5<VAR>C₂₃ : Type u_6<VAR>inst✝⁵ : Category.{?u.16016, u_1} C₁<VAR>inst✝⁴ : Category.{?u.16020, u_2} C₂<VAR>inst✝³ : Category.{?u.16024, u_3} C₃<VAR>inst✝² : Category.{?u.16028, u_4} C₄<VAR>inst✝¹ : Category.{?u.16032, u_5} C₁₂<VAR>inst✝ : Category.{?u.16036, u_6} C₂₃<VAR>F : C₁ ⥤ C₂₃ ⥤ C₄<VAR>G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃<VAR>X₁ : C₁<VAR>X₂ Y₂ : C₂<VAR>φ✝ : X₂ ⟶ Y₂<VAR>X₃ Y₃ : C₃<VAR>φ : X₃ ⟶ Y₃<GOAL>(F.obj X₁).map ((G₂₃.obj X₂).map φ) ≫ (F.obj X₁).map ((G₂₃.map φ✝).app Y₃) = (F.obj X₁).map ((G₂₃.map φ✝).app X₃) ≫ (F.obj X₁).map ((G₂₃.obj Y₂).map φ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>hf : InjOn f (freeOn E).E<GOAL>(freeOn E).map f hf = freeOn (f '' E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f✝ : α → β<VAR>E I s : Set α<VAR>M : Matroid α<VAR>N : Matroid β<VAR>f : α → β<VAR>hf : InjOn f (freeOn E).E<GOAL>((freeOn E).map f hf)✶ = (freeOn (f '' E))✶
<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>f : E → F<VAR>g : E → G<VAR>hf : ContDiffWithinAt 𝕜 n f s x<VAR>hg : ContDiffWithinAt 𝕜 n g s x<VAR>m : ℕ<VAR>hm : ↑m ≤ n<VAR>u : Set E<VAR>hu : u ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>hp : HasFTaylorSeriesUpToOn (↑m) f p u<VAR>v : Set E<VAR>hv : v ∈ 𝓝[insert x s] x<VAR>q : E → FormalMultilinearSeries 𝕜 E G<VAR>hq : HasFTaylorSeriesUpToOn (↑m) g q v<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) (fun x => (f x, g x)) p u
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (𝓞 K)ˣ<VAR>n : ℕ<GOAL>(algebraMap (𝓞 K) K) ↑(x ^ n) = (algebraMap (𝓞 K) K) ↑x ^ n
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s t : Set α<VAR>d : ℝ≥0∞<GOAL>diam (insert x s) ≤ d ↔ max (⨆ y ∈ s, edist x y) (diam s) ≤ d
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>s : Set E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>μ (sphere x r) = 0
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>s : Set E<VAR>inst✝ : Nontrivial E<VAR>x : E<GOAL>μ (sphere x 0) = 0
<VAR>E : Type u_1<VAR>inst✝⁹ : NormedAddCommGroup E<VAR>inst✝⁸ : NormedSpace ℝ E<VAR>inst✝⁷ : MeasurableSpace E<VAR>inst✝⁶ : BorelSpace E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝⁴ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>s : Set E<VAR>inst✝ : Nontrivial E<VAR>x : E<VAR>r : ℝ<VAR>h : r ≠ 0<GOAL>μ (sphere x r) = 0
<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>N : Type u_5<VAR>inst✝ : Group N<VAR>H : Subgroup G<VAR>f : G →* N<VAR>hf : Injective ⇑f<GOAL>map f H = ⊥ ↔ H = ⊥
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (↑n / ↑d < 0) = true<VAR>h₂ : decide (-1 < ↑n / ↑d) = true<GOAL>Real.log e ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (↑n / ↑d < 0) = true<VAR>h₂ : decide (-1 < ↑n / ↑d) = true<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (↑n / ↑d < 0) = true<VAR>h₂ : decide (-1 < ↑n / ↑d) = true<VAR>h₁' : ↑n / ↑d < 0<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>e : ℝ<VAR>d : ℕ<VAR>n : ℤ<VAR>inv : Invertible ↑d<VAR>eq : e = ↑n * ⅟↑d<VAR>h₁ : decide (↑n / ↑d < 0) = true<VAR>h₂ : decide (-1 < ↑n / ↑d) = true<VAR>h₁' : ↑n / ↑d < 0<VAR>h₂' : -1 < ↑n / ↑d<GOAL>Real.log (↑n / ↑d) ≠ 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.156646, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K : CochainComplex C ℤ<VAR>α : Cochain F K (-1)<VAR>β : G ⟶ K<VAR>eq : δ (-1) 0 α = Cochain.ofHom (φ ≫ β)<VAR>p q : ℤ<VAR>hpq : p + 1 = q<GOAL>(desc φ α β eq).f p = (↑(fst φ)).v p q hpq ≫ α.v q p ⋯ + (snd φ).v p p ⋯ ≫ β.f p
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T3Space X<VAR>x y : X<VAR>h : x ≠ y<GOAL>∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T3Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>U₁ U₂ : Set X<VAR>U₁_op : IsOpen U₁<VAR>U₂_op : IsOpen U₂<VAR>x_in : x ∈ U₁<VAR>y_in : y ∈ U₂<VAR>H : Disjoint U₁ U₂<GOAL>∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T3Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>U₁ U₂ : Set X<VAR>U₁_op : IsOpen U₁<VAR>U₂_op : IsOpen U₂<VAR>x_in : x ∈ U₁<VAR>y_in : y ∈ U₂<VAR>H : Disjoint U₁ U₂<VAR>V₁ : Set X<VAR>V₁_in : V₁ ∈ 𝓝 x<VAR>V₁_closed : IsClosed V₁<VAR>h₁ : V₁ ⊆ U₁<GOAL>∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T3Space X<VAR>x y : X<VAR>h : x ≠ y<VAR>U₁ U₂ : Set X<VAR>U₁_op : IsOpen U₁<VAR>U₂_op : IsOpen U₂<VAR>x_in : x ∈ U₁<VAR>y_in : y ∈ U₂<VAR>H : Disjoint U₁ U₂<VAR>V₁ : Set X<VAR>V₁_in : V₁ ∈ 𝓝 x<VAR>V₁_closed : IsClosed V₁<VAR>h₁ : V₁ ⊆ U₁<VAR>V₂ : Set X<VAR>V₂_in : V₂ ∈ 𝓝 y<VAR>V₂_closed : IsClosed V₂<VAR>h₂ : V₂ ⊆ U₂<GOAL>∃ U₁ ∈ 𝓝 x, ∃ V₁ ∈ 𝓝 x, ∃ U₂ ∈ 𝓝 y, ∃ V₂ ∈ 𝓝 y, IsClosed V₁ ∧ IsClosed V₂ ∧ IsOpen U₁ ∧ IsOpen U₂ ∧ V₁ ⊆ U₁ ∧ V₂ ⊆ U₂ ∧ Disjoint U₁ U₂
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : SeminormedRing 𝕝<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕝 E<VAR>inst✝ : TopologicalSpace E<VAR>p : Seminorm 𝕝 E<VAR>hp : Continuous ⇑p<VAR>r : ℝ<VAR>hr : 0 < r<VAR>this : Tendsto (⇑p) (𝓝 0) (𝓝 0)<GOAL>p.ball 0 r ∈ 𝓝 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<GOAL>∀ (x : β), p x ∧ q x → p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<GOAL>∀ (x : β), p x ∧ q x → q x
<VAR>m n : ℕ<GOAL>↑m < ↑n ↔ m < n
<VAR>R : Type u_1<VAR>n : ℕ<GOAL>(2 * n + 1).choose n ≤ 4 ^ n
<VAR>R : Type u_1<VAR>n : ℕ<VAR>t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i<GOAL>(2 * n + 1).choose n ≤ 4 ^ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>Integrable (fun x => ((κ x) s).toReal) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : α<GOAL>‖((κ x) s).toReal‖ ≤ (IsFiniteKernel.bound κ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>μ : Measure α<VAR>inst✝¹ : IsFiniteMeasure μ<VAR>κ : Kernel α β<VAR>inst✝ : IsFiniteKernel κ<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>x : α<GOAL>(κ x) s ≤ IsFiniteKernel.bound κ
<VAR>α β : Type u<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>ℵ₀ * ↑n = ℵ₀
<VAR>α : Type u<VAR>β✝ : α → Type v<VAR>β : α → Type u<VAR>inst✝ : ∀ (a : α), Finite (β a)<GOAL>max (lift.{u, u} #α) ℵ₀ = max #α ℵ₀
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : CommGroupWithZero G₀<VAR>a✝ b c✝ d a c : G₀<VAR>hb : b ≠ 0<VAR>hd : d ≠ 0<VAR>h : a / b = c / d<GOAL>a * d = c * b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝² : Preorder α<VAR>inst✝¹ : Preorder β<VAR>inst✝ : Preorder γ<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<VAR>a✝ : α<VAR>b✝ : β<VAR>h₀ : ∀ (b : β), Monotone (swap f b)<VAR>h₁ : ∀ (a : α), Antitone (f a)<VAR>a : α<VAR>ha : a ∈ upperBounds s<VAR>b : β<VAR>hb : b ∈ lowerBounds t<GOAL>BddAbove (image2 f s t)
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : Cocone F<VAR>α : Type u<VAR>f : Quot F → α<VAR>hc : IsColimit c<VAR>x : Quot F<GOAL>hc.desc (toCocone f) (desc c x) = f x
<VAR>J : Type v<VAR>inst✝ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>c : Cocone F<VAR>α : Type u<VAR>f : Quot F → α<VAR>hc : IsColimit c<VAR>j : J<VAR>y : F.obj j<GOAL>hc.desc (toCocone f) (desc c (ι F j y)) = f (ι F j y)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>m : ℕ := rootMultiplicity t p<VAR>hm : m = rootMultiplicity t p<GOAL>eval t ((⇑derivative)^[m] p) = m.factorial • eval t (p /ₘ (X - C t) ^ m)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>m : ℕ := rootMultiplicity t p<VAR>hm : m = rootMultiplicity t p<GOAL>eval t ((⇑derivative)^[m] ((X - C t) ^ m * (p /ₘ (X - C t) ^ m))) = m.factorial • eval t (p /ₘ (X - C t) ^ m)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>m : ℕ := rootMultiplicity t p<VAR>hm : m = rootMultiplicity t p<GOAL>eval t (m.choose 0 • ((⇑derivative)^[m - 0] ((X - C t) ^ m) * (⇑derivative)^[0] (p /ₘ (X - C t) ^ m))) = m.factorial • eval t (p /ₘ (X - C t) ^ m)
<VAR>R : Type u<VAR>S : Type v<VAR>k : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommRing R<VAR>p : R[X]<VAR>t : R<VAR>m : ℕ := rootMultiplicity t p<VAR>hm : m = rootMultiplicity t p<GOAL>∀ b ∈ range m.succ, b ≠ 0 → eval t (m.choose b • ((⇑derivative)^[m - b] ((X - C t) ^ m) * (⇑derivative)^[b] (p /ₘ (X - C t) ^ m))) = 0
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>T : F →L[ℝ] F<VAR>hT : (↑T).IsSymmetric<VAR>x₀ : F<GOAL>HasStrictFDerivAt T.reApplyInnerSelf (2 • (innerSL ℝ) (T x₀)) x₀
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>T : F →L[ℝ] F<VAR>hT : (↑T).IsSymmetric<VAR>x₀ : F<VAR>e_7✝ : Real.normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'<GOAL>2 • (innerSL ℝ) (T x₀) = (fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : RCLike 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>T : F →L[ℝ] F<VAR>hT : (↑T).IsSymmetric<VAR>x₀ : F<VAR>e_7✝ : Real.normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup<VAR>he✝ : InnerProductSpace.toNormedSpace = NormedAlgebra.toNormedSpace'<VAR>y : F<GOAL>(2 • (innerSL ℝ) (T x₀)) y = ((fderivInnerCLM ℝ (T x₀, id x₀)).comp (T.prod (ContinuousLinearMap.id ℝ F))) y
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<GOAL>(C a).degree = (C a * T 0).degree
<VAR>R M : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Flat R M<VAR>K N : Type u<VAR>inst✝⁶ : AddCommGroup K<VAR>inst✝⁵ : Module R K<VAR>inst✝⁴ : Finite R K<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Free R N<VAR>inst✝ : Finite R N<VAR>f : K →ₗ[R] N<VAR>x : N →ₗ[R] M<VAR>h : x ∘ₗ f = 0<VAR>this : ∀ (K' : Submodule R K), K'.FG → ∃ κ x_1 a y, x = y ∘ₗ a ∧ K' ≤ ker (a ∘ₗ f)<GOAL>∃ κ x_1 a y, x = y ∘ₗ a ∧ a ∘ₗ f = 0
<VAR>R M : Type u<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : Flat R M<VAR>K N : Type u<VAR>inst✝⁶ : AddCommGroup K<VAR>inst✝⁵ : Module R K<VAR>inst✝⁴ : Finite R K<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>inst✝¹ : Free R N<VAR>inst✝ : Finite R N<VAR>f : K →ₗ[R] N<VAR>x : N →ₗ[R] M<VAR>h : x ∘ₗ f = 0<VAR>this : ∀ (K' : Submodule R K), K'.FG → ∃ κ x_1 a y, x = y ∘ₗ a ∧ K' ≤ ker (a ∘ₗ f)<VAR>x✝³ : Type u<VAR>x✝² : Fintype x✝³<VAR>x✝¹ : N →ₗ[R] x✝³ →₀ R<VAR>x✝ : (x✝³ →₀ R) →ₗ[R] M<GOAL>x✝¹ ∘ₗ f = 0 ↔ ⊤ ≤ ker (x✝¹ ∘ₗ f)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y : R<VAR>h : W.Equation x y<GOAL>Equation (WeierstrassCurve.map W f) (f x) (f y)
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W : Affine R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>x y : R<VAR>h : W.Equation x y<GOAL>f (evalEval x y W.polynomial) = f 0
<VAR>R : Type u₁<VAR>inst✝³ : CommSemiring R<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CharP R p<VAR>S : Type u₂<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CharP S p<VAR>φ : R →+* S<VAR>f : Ring.Perfection R p<VAR>n : ℕ<GOAL>(fun n => φ ((coeff R p n) f)) (n + 1) ^ p = (fun n => φ ((coeff R p n) f)) n
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin n) (Fin (n + 1)) R<VAR>hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>(M.submatrix id j₁.succAbove).det = (↑↑j₁ - ↑↑j₂).negOnePow • (M.submatrix id j₂.succAbove).det
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin n) (Fin (n + 1)) R<VAR>hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0<VAR>j₁ j₂ : Fin (n + 1)<GOAL>∑ j : Fin (n + 1), Mᵀ j = 0
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>M : Matrix (Fin n) (Fin (n + 1)) R<VAR>hv : ∀ (i : Fin n), ∑ j : Fin (n + 1), M i j = 0<VAR>j₁ j₂ : Fin (n + 1)<VAR>x✝ : Fin n<GOAL>(∑ j : Fin (n + 1), Mᵀ j) x✝ = 0 x✝
<VAR>c : Cardinal.{u_1}<GOAL>c ^< ℵ₀ ≤ max c ℵ₀
<VAR>c : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ c<GOAL>c ^< ℵ₀ ≤ max c ℵ₀
<VAR>c : Cardinal.{u_1}<VAR>h : c < ℵ₀<GOAL>c ^< ℵ₀ ≤ max c ℵ₀
<VAR>c : Cardinal.{u_1}<VAR>h : c < ℵ₀<GOAL>∀ x < ℵ₀, c ^ x ≤ max c ℵ₀
<VAR>m n x✝² x✝¹ x✝ : ℕ<VAR>hk : x✝ ≤ x✝¹<GOAL>x✝² <<< (x✝¹ - x✝) = x✝² <<< x✝¹ >>> x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f : CauSeq α abs<VAR>K : α<VAR>H : ∀ (i : ℕ), |↑f i| < K<VAR>i : ℕ<VAR>x✝ : i ≥ 0<GOAL>1 ≤ ↑(const (K + 1) - f) i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>f : CauSeq α abs<VAR>K : α<VAR>H : ∀ (i : ℕ), |↑f i| < K<VAR>i : ℕ<VAR>x✝ : i ≥ 0<GOAL>↑f i ≤ K
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Sort w<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : X<VAR>s✝ s₁ s₂ t : Set X<VAR>p p₁ p₂ : X → Prop<VAR>inst✝ : TopologicalSpace X<VAR>s : Set X<GOAL>IsClosed sᶜ ↔ IsOpen s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>s : PullbackCone f g<VAR>i : 𝒰.J<GOAL>(pullbackP1Iso 𝒰 f g i).hom ≫ Multicoequalizer.π (gluing 𝒰 f g).diagram i = pullback.fst (p1 𝒰 f g) (𝒰.map i)
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<GOAL>(Summable fun k => (↑(u (k + 1)) - ↑(u k)) * f (u k)) ↔ Summable f
<VAR>C : ℕ<VAR>u : ℕ → ℕ<VAR>f : ℕ → ℝ≥0<VAR>hf : ∀ ⦃m n : ℕ⦄, 0 < m → m ≤ n → f n ≤ f m<VAR>h_pos : ∀ (n : ℕ), 0 < u n<VAR>hu_strict : StrictMono u<VAR>hC_nonzero : C ≠ 0<VAR>h_succ_diff : SuccDiffBounded C u<GOAL>∑' (b : ℕ), ↑(↑(u (b + 1)) - ↑(u b)) * ↑(f (u b)) = ⊤ ↔ ∑' (b : ℕ), ↑(f b) = ⊤
<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 ν * ν.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μν : μ ≪ ν<GOAL>AEMeasurable (μ.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μν : μ ≪ ν<GOAL>∀ᵐ (x : α) ∂ν, μ.rnDeriv ν x ≠ ⊤
<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>(ν.withDensity (μ.rnDeriv ν)).rnDeriv κ =ᶠ[ae κ] μ.rnDeriv κ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : CancelCommMonoid α<VAR>s : Finset α<VAR>a : α<GOAL>mulRothNumber (map (mulRightEmbedding a) s) = mulRothNumber s
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.51124, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X✝ Y✝ : HomologicalComplex V c.symm<VAR>f : X✝ ⟶ Y✝<VAR>i j : ι<VAR>x✝ : c.Rel i j<GOAL>(fun i => (f.f i).op) i ≫ X✝.opSymm.d i j = Y✝.opSymm.d i j ≫ (fun i => (f.f i).op) j
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>(1 + X • M.map ⇑C).det = 1 + M.trace • X + (1 + X • M.map ⇑C).det.divX.divX * X ^ 2
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>(1 + X • M.map ⇑C).det = (1 + X • M.map ⇑C).det.divX * X + C 1
<VAR>R : Type u<VAR>inst✝³ : CommRing R<VAR>n G : Type v<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>α β : Type v<VAR>inst✝ : DecidableEq α<VAR>M✝ M : Matrix n n R<GOAL>1 = (1 + X • M.map ⇑C).det.coeff 0
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hfi : IntervalIntegrable f μ a b<VAR>hgi : IntervalIntegrable g μ a b<VAR>hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g<VAR>hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0<GOAL>∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hfi : IntervalIntegrable f μ a b<VAR>hgi : IntervalIntegrable g μ a b<VAR>hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g<VAR>hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0<GOAL>0 < (μ.restrict (Ioc a b)) (support fun x => g x - f x)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hfi : IntervalIntegrable f μ a b<VAR>hgi : IntervalIntegrable g μ a b<VAR>hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g<VAR>hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0<GOAL>0 ≤ᶠ[ae (μ.restrict (Ioc a b))] fun x => g x - f x
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : ℝ → ℝ<VAR>a b : ℝ<VAR>μ : Measure ℝ<VAR>hab : a ≤ b<VAR>hfi : IntervalIntegrable f μ a b<VAR>hgi : IntervalIntegrable g μ a b<VAR>hle : f ≤ᶠ[ae (μ.restrict (Ioc a b))] g<VAR>hlt : (μ.restrict (Ioc a b)) {x | f x < g x} ≠ 0<GOAL>Integrable (fun x => g x - f x) (μ.restrict (Ioc a b))
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : Small.{u, max u v} ↑F.sections<VAR>j j' : J<VAR>f : j ⟶ j'<GOAL>((Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).map f ≫ (fun j u => ↑((equivShrink ↑F.sections).symm u) j) j' = (fun j u => ↑((equivShrink ↑F.sections).symm u) j) j ≫ F.map f
<VAR>J : Type v<VAR>inst✝¹ : Category.{w, v} J<VAR>F : J ⥤ Type u<VAR>inst✝ : Small.{u, max u v} ↑F.sections<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ((Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).obj j<GOAL>(((Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).map f ≫ (fun j u => ↑((equivShrink ↑F.sections).symm u) j) j') x = ((fun j u => ↑((equivShrink ↑F.sections).symm u) j) j ≫ F.map f) x