ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I J : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsNoetherianRing R<VAR>inst✝ : Nontrivial M<VAR>x : M<VAR>hx : x ≠ 0<VAR>P : Ideal R<VAR>hP : IsAssociatedPrime P M<VAR>right✝ : (Submodule.span R {x}).annihilator ≤ P<GOAL>(associatedPrimes R M).Nonempty
<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>q : ℕ<VAR>hF : ExpChar F q<VAR>x : E<VAR>x✝ : ∃ n y, minpoly F x = (expand F (q ^ n)) (X - C y)<VAR>n : ℕ<VAR>y : F<VAR>h : minpoly F x = (expand F (q ^ n)) (X - C y)<GOAL>(minpoly F x).natSepDegree = 1
<VAR>m n✝ n : ℕ<VAR>a : ZMod (n + 1)<GOAL>a.val = 0 ↔ a = 0
<VAR>m n✝ n : ℕ<VAR>a : ZMod (n + 1)<GOAL>a.val = 0 ↔ ↑a = ↑0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜<VAR>i : ι<GOAL>⟪b i, x⟫_𝕜 = ⟪b i, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜<VAR>i : ι<GOAL>(starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = ⟪b i, y⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : InnerProductSpace 𝕜 E<VAR>ι : Type u_3<VAR>x y : E<VAR>b : Basis ι 𝕜 E<VAR>h : ∀ (i : ι), ⟪x, b i⟫_𝕜 = ⟪y, b i⟫_𝕜<VAR>i : ι<GOAL>(starRingEnd 𝕜) ⟪x, b i⟫_𝕜 = (starRingEnd 𝕜) ⟪y, b i⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<GOAL>ConvexOn 𝕜 s f
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁷ : OrderedSemiring 𝕜<VAR>inst✝⁶ : AddCommMonoid E<VAR>inst✝⁵ : AddCommMonoid F<VAR>inst✝⁴ : OrderedAddCommMonoid α<VAR>inst✝³ : OrderedAddCommMonoid β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : LinearOrder E<VAR>s : Set E<VAR>f : E → β<VAR>hs : Convex 𝕜 s<VAR>hf : ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → x < y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → f (a • x + b • y) ≤ a • f x + b • f y<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>hxy : x ≠ y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>f (a • x + b • y) ≤ a • f x + b • f y
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u₁<VAR>inst✝ : Category.{v₁, u₁} D<VAR>F✝ F : C ⥤ D<VAR>X Y : C<VAR>α : X ≅ Y<VAR>f : Aut X<GOAL>(F.mapIso (α.conjAut f)).hom = ((F.mapIso α).conjAut (F.mapIso f)).hom
<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>h : ContDiffAt 𝕜 (↑n) f x<GOAL>∀ᶠ (y : E) in 𝓝 x, ContDiffAt 𝕜 (↑n) f y
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ (n + 1)
<VAR>β : Type u_1<VAR>G : Type u_2<VAR>M : Type u_3<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Preorder M<VAR>inst✝ : CovariantClass M M (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>x : M<VAR>hx : 1 ≤ x<VAR>n : ℕ<GOAL>1 ≤ x ^ n * x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<GOAL>Primrec (Function.uncurry f) ↔ Primrec₂ f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>σ : Type u_3<VAR>inst✝² : Primcodable α<VAR>inst✝¹ : Primcodable β<VAR>inst✝ : Primcodable σ<VAR>f : α → β → σ<GOAL>(Primrec fun p => f p.1 p.2) ↔ Primrec₂ f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>r : R<GOAL>toTensorAlgebra (DirectSum.GAlgebra.toFun r) = (algebraMap R (TensorAlgebra R M)) r
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_4, u_1} C<VAR>inst✝² : Category.{?u.85033, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝¹ : W.HasLeftCalculusOfFractions<VAR>E : Type u_3<VAR>inst✝ : Category.{u_5, u_3} E<VAR>F : C ⥤ E<VAR>hF : W.IsInvertedBy F<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>Hom.map ((Q W).map f) F hF = 𝟙 (F.obj X) ≫ F.map f ≫ 𝟙 (F.obj Y)
<VAR>a n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>hs : Sorted (fun x x_1 => x < x_1) n.bitIndices<GOAL>Sorted (fun x x_1 => x < x_1) (bit b n).bitIndices
<VAR>a n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>hs : Sorted (fun x x_1 => x < x_1) n.bitIndices<GOAL>List.Pairwise (fun a b => a < b) n.bitIndices
<VAR>α : Type u_1<VAR>l r₁ r₂ : ℕ<VAR>h₁ : r₁ ≤ r₂<VAR>h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l<VAR>H : BalancedSz l r₁<GOAL>BalancedSz l r₂
<VAR>α : Type u_1<VAR>l r₁ r₂ : ℕ<VAR>h₁ : r₁ ≤ r₂<VAR>h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l<VAR>H : BalancedSz l r₁<VAR>h : ¬l + r₂ ≤ 1<GOAL>l ≤ delta * r₂ ∧ r₂ ≤ delta * l
<VAR>α : Type u_1<VAR>l r₁ r₂ : ℕ<VAR>h₁ : r₁ ≤ r₂<VAR>h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ delta * l<VAR>H : BalancedSz l r₁<VAR>h : ¬l + r₂ ≤ 1<GOAL>l ≤ delta * r₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>X : SimplicialObject C<VAR>s : Splitting X<VAR>inst✝ : HasZeroMorphisms C<VAR>Δ : SimplexCategoryᵒᵖ<VAR>A B : IndexSet Δ<VAR>h : B ≠ A<GOAL>((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 => if h : B_1 = B then eqToHom ⋯ else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>∃ g, eLpNorm (f - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<GOAL>∃ g, eLpNorm (f - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<VAR>hf' : Memℒp f' p μ<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<VAR>hf' : Memℒp f' p μ<VAR>f'meas : Measurable f'<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<VAR>hf' : Memℒp f' p μ<VAR>f'meas : Measurable f'<VAR>this : SeparableSpace ↑(Set.range f' ∪ {0})<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<VAR>hf' : Memℒp f' p μ<VAR>f'meas : Measurable f'<VAR>this : SeparableSpace ↑(Set.range f' ∪ {0})<VAR>n : ℕ<VAR>hn : eLpNorm (↑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n) - f') p μ < ε<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E✝ : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : MeasurableSpace E✝<VAR>inst✝² : NormedAddCommGroup E✝<VAR>inst✝¹ : NormedAddCommGroup F<VAR>q : ℝ<VAR>p : ℝ≥0∞<VAR>E : Type u_7<VAR>inst✝ : NormedAddCommGroup E<VAR>f : β → E<VAR>μ : Measure β<VAR>hf : Memℒp f p μ<VAR>hp_ne_top : p ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<VAR>f' : β → E := AEStronglyMeasurable.mk f ⋯<VAR>hf' : Memℒp f' p μ<VAR>f'meas : Measurable f'<VAR>this : SeparableSpace ↑(Set.range f' ∪ {0})<VAR>n : ℕ<VAR>hn : eLpNorm (f' - ↑(approxOn f' f'meas (Set.range f' ∪ {0}) 0 ⋯ n)) p μ < ε<GOAL>∃ g, eLpNorm (f' - ↑g) p μ < ε ∧ Memℒp (↑g) p μ
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<GOAL>(∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
<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>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ = ↑(π / 2)<VAR>hs : (∡ p₃ p₁ p₂).sign = 1<GOAL>(∡ p₃ p₁ p₂).tan * dist p₁ p₂ = dist p₃ p₂
<VAR>u✝ : Lean.Level<VAR>arg : Q(Type u✝)<VAR>sα✝ : Q(CommSemiring «$arg»)<VAR>u : Lean.Level<VAR>α : Q(Type u)<VAR>sα : Q(CommSemiring «$α»)<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>a a' a₁ a₂ a₃ b b' b₁✝ b₂ b₃ c₁ c₂ b₁ : R<GOAL>a + (b₁ + b₂) = b₁ + (a + b₂)
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>f.neLocus (f - g) = g.support
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : Squarefree n<VAR>t : Finset ℕ<VAR>ht : t ⊆ n.primeFactors<GOAL>∏ a ∈ n.primeFactors \ t, a = n / ∏ a ∈ t, a
<VAR>s : Finset ℕ<VAR>m n✝ p n : ℕ<VAR>hn : Squarefree n<VAR>t : Finset ℕ<VAR>ht : t ⊆ n.primeFactors<GOAL>n = (∏ a ∈ n.primeFactors \ t, a) * ∏ a ∈ t, a
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<GOAL>‖derivWithin f s x‖ = ‖fderivWithin 𝕜 f s x‖
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁴ : Field R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : Module.Finite R L<VAR>inst✝ : LieAlgebra.IsKilling R L<VAR>x : L<VAR>h : (ad R L) x = 0<GOAL>x = 0
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>x w : V<GOAL>𝓕 (fun v => cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑⟪x, v⟫_ℝ)) w = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-↑π ^ 2 * ↑‖x - w‖ ^ 2 / b)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>x w : V<GOAL>∫ (v : V), cexp (-(2 * ↑π * ↑⟪w, v⟫_ℝ * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑⟪x, v⟫_ℝ)) = (↑π / b) ^ (↑(FiniteDimensional.finrank ℝ V) / 2) * cexp (-(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>x w v : V<GOAL>cexp (-(2 * ↑π * ↑⟪w, v⟫_ℝ * I) + (-(b * ↑‖v‖ ^ 2) + 2 * ↑π * I * ↑⟪x, v⟫_ℝ)) = cexp (-b * ↑‖v‖ ^ 2 + 2 * ↑π * I * ↑⟪x - w, v⟫_ℝ)
<VAR>b : ℂ<VAR>V : Type u_1<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : FiniteDimensional ℝ V<VAR>inst✝¹ : MeasurableSpace V<VAR>inst✝ : BorelSpace V<VAR>hb : 0 < b.re<VAR>x w : V<GOAL>-(↑π ^ 2 * ↑‖x - w‖ ^ 2) / b = (2 * ↑π * I) ^ 2 * ↑‖x - w‖ ^ 2 / (4 * b)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖f'‖ ≤ ↑C
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<GOAL>Summable (f_nat k a t)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)<GOAL>Summable (f_nat k a t)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)<GOAL>∀ᶠ (i : ℕ) in atTop, ‖f_nat k a t i‖ ≤ 2 ^ k * (↑i ^ k * rexp (-π * (↑i + a) ^ 2 * t))
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)<GOAL>∀ᶠ (i : ℕ) in atTop, |↑i + a| ^ k ≤ (↑i + ↑i) ^ k
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ht : 0 < t<VAR>this : Summable fun n => ↑n ^ k * rexp (-π * (↑n + a) ^ 2 * t)<VAR>n : ℕ<VAR>hn : ⌈|a|⌉₊ ≤ n<GOAL>|↑n + a| ^ k ≤ (↑n + ↑n) ^ k
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DiscreteValuationRing R<VAR>ϖ : R<VAR>h : maximalIdeal R = span {ϖ}<VAR>e : ϖ = 0<GOAL>maximalIdeal R = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>x : S<GOAL>x ∈ map (RingHom.snd R S) (I.prod J) ↔ x ∈ J
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Semiring S<VAR>I✝ I' : Ideal R<VAR>J✝ J' : Ideal S<VAR>I : Ideal R<VAR>J : Ideal S<VAR>x : S<GOAL>(∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) ↔ x ∈ J
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{u}<VAR>c : Ordinal.{u}<VAR>ho : o.card < c.cof<GOAL>Cardinal.lift.{u, u} o.card < c.cof
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<GOAL>ConvexOn 𝕜 (Ioi 0) fun x => x ^ ↑n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<GOAL>ConvexOn 𝕜 (Ioi 0) fun x => x ^ n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<GOAL>ConvexOn 𝕜 (Ioi 0) fun x => x ^ -[n+1]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<GOAL>ConvexOn 𝕜 (Ioi 0) fun x => x⁻¹ ^ (n + 1)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<GOAL>∀ ⦃x : 𝕜⦄, x ∈ Ioi 0 → ∀ ⦃y : 𝕜⦄, y ∈ Ioi 0 → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → (a • x + b • y)⁻¹ ≤ a • x⁻¹ + b • y⁻¹
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>y : 𝕜<VAR>hy : 0 < y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>1 / (a * x + b * y) ≤ (a * y + b * x) / (x * y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>y : 𝕜<VAR>hy : 0 < y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 ≤ (a * y + b * x) * (a * x + b * y) - 1 * (x * y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>y : 𝕜<VAR>hy : 0 < y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < a * x + b * y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝ : LinearOrderedField 𝕜<VAR>n : ℕ<VAR>x : 𝕜<VAR>hx : 0 < x<VAR>y : 𝕜<VAR>hy : 0 < y<VAR>a b : 𝕜<VAR>ha : 0 < a<VAR>hb : 0 < b<VAR>hab : a + b = 1<GOAL>0 < x * y
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : ∃ α, F⟮α⟯ = ⊤<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>h : ∃ α, F⟮α⟯ = ⊤<VAR>this : FiniteDimensional F E<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : FiniteDimensional F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>f : F[X] := minpoly F α<VAR>G : Type u_2 := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : FiniteDimensional F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>f : F[X] := minpoly F α<VAR>G : Type u_2 := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }<VAR>hfin : Finite G<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : FiniteDimensional F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>f : F[X] := minpoly F α<VAR>G : Type u_2 := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }<VAR>hfin : Finite G<VAR>g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩<GOAL>Finite (IntermediateField F E)
<VAR>F : Type u_1<VAR>E : Type u_2<VAR>inst✝³ : Field F<VAR>inst✝² : Field E<VAR>inst✝¹ : Algebra F E<VAR>inst✝ : Algebra.IsAlgebraic F E<VAR>this : FiniteDimensional F E<VAR>α : E<VAR>hprim : F⟮α⟯ = ⊤<VAR>f : F[X] := minpoly F α<VAR>G : Type u_2 := { g // g.Monic ∧ g ∣ Polynomial.map (algebraMap F E) f }<VAR>hfin : Finite G<VAR>g : IntermediateField F E → G := fun K => ⟨Polynomial.map (algebraMap (↥K) E) (minpoly (↥K) α), ⋯⟩<VAR>hinj : Function.Injective g<GOAL>Finite (IntermediateField F E)
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = (eval r) G<VAR>hnR : ↑n ≤ #R<GOAL>F = G
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = (eval r) G<VAR>hnR : ↑n ≤ #R<GOAL>F - G = 0
<VAR>σ✝ : Type u_1<VAR>τ : Type u_2<VAR>R✝ : Type u_3<VAR>S : Type u_4<VAR>inst✝⁴ inst✝³ : CommSemiring R✝<VAR>inst✝² : CommSemiring S<VAR>φ ψ : MvPolynomial σ✝ R✝<VAR>m n✝ : ℕ<VAR>R : Type u_5<VAR>σ : Type u_6<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>F G : MvPolynomial σ R<VAR>n : ℕ<VAR>hF : F.IsHomogeneous n<VAR>hG : G.IsHomogeneous n<VAR>h : ∀ (r : σ → R), (eval r) F = (eval r) G<VAR>hnR : ↑n ≤ #R<GOAL>∀ (r : σ → R), (eval r) (F - G) = 0
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F G H : C ⥤ Type w<VAR>X Y Z : C<VAR>σ : F ⟶ G<VAR>τ : G ⟶ H<VAR>a : F.obj X<GOAL>F.map (𝟙 X) a = a
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD n.gcd m]<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>↑(if hn : n = 0 then ⟨a, ⋯⟩ else if hm : m = 0 then ⟨b, ⋯⟩ else ⟨((↑n * (n.xgcd m).1 * ↑b + ↑m * (n.xgcd m).2 * ↑a) / ↑(n.gcd m) % ↑(n.lcm m)).toNat, ⋯⟩) < n.lcm m
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD n.gcd m]<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<GOAL>((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat < (↑(n.lcm m)).toNat
<VAR>m n a b c d : ℕ<VAR>h : a ≡ b [MOD n.gcd m]<VAR>hn : n ≠ 0<VAR>hm : m ≠ 0<VAR>lcm_pos : 0 < ↑(n.lcm m)<GOAL>((↑n * (n.gcdA m, n.gcdB m).1 * ↑b + ↑m * (n.gcdA m, n.gcdB m).2 * ↑a) / ↑(n.gcd m) % ↑(↑(n.lcm m)).toNat).toNat < (↑(n.lcm m)).toNat
<VAR>x : ℝ<VAR>hl : -(π / 2) ≤ x<VAR>hu : x ≤ π / 2<GOAL>cos x = √(1 - sin x ^ 2)
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>a a' : α<VAR>s : AList β<GOAL>a' ∈ erase a s ↔ a' ≠ a ∧ a' ∈ s
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255779}<VAR>a : Cardinal.{u_1}<GOAL>a ^< 0 = 0
<VAR>α β : Type u<VAR>c : Cardinal.{?u.255779}<VAR>a : Cardinal.{u_1}<GOAL>IsEmpty ↑(Iio 0)
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ : α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<GOAL>s ∈ image (insert a) (memberSubfamily a 𝒜) ↔ s ∈ filter (fun x => a ∈ x) 𝒜
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ : α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<GOAL>(∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) ↔ s ∈ 𝒜 ∧ a ∈ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ : α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<GOAL>(∃ a_1, (insert a a_1 ∈ 𝒜 ∧ a ∉ a_1) ∧ insert a a_1 = s) → s ∈ 𝒜 ∧ a ∈ s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>𝒜✝ ℬ : Finset (Finset α)<VAR>s✝ : Finset α<VAR>a✝ : α<VAR>𝒜 : Finset (Finset α)<VAR>a : α<VAR>s : Finset α<VAR>x✝ : s ∈ 𝒜 ∧ a ∈ s<VAR>hs : s ∈ 𝒜<VAR>ha : a ∈ s<GOAL>insert a (s.erase a) ∈ 𝒜