ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>A : Type u₁<VAR>inst✝⁵ : Category.{v₁, u₁} A<VAR>B : Type u₂<VAR>inst✝⁴ : Category.{v₂, u₂} B<VAR>T : Type u₃<VAR>inst✝³ : Category.{v₃, u₃} T<VAR>A' : Type u_1<VAR>B' : Type u_2<VAR>T' : Type u_3<VAR>inst✝² : Category.{?u.20583, u_1} A'<VAR>inst✝¹ : Category.{?u.20587, u_2} B'<VAR>inst✝ : Category.{?u.20591, u_3} T'<VAR>L : A ⥤ T<VAR>R : B ⥤ T<VAR>L₁ L₂ L₃ : A ⥤ T<VAR>R₁ R₂ R₃ : B ⥤ T<VAR>X Y : Comma L₁ R₁<VAR>l : X.left ≅ Y.left<VAR>r : X.right ≅ Y.right<VAR>h : autoParam (L₁.map l.hom ≫ Y.hom = X.hom ≫ R₁.map r.hom) _auto✝<GOAL>X.hom = X.hom ≫ R₁.map (r.hom ≫ r.inv)
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(⇑(IsometryEquiv.vaddConst c) ∘ fun x => r • x) '' ball 0 1 = ball c r
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>P : Type u_2<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>c : P<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>ball ((IsometryEquiv.vaddConst c) 0) ‖r‖ = ball c r
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b✝ c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>a b : G<VAR>ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s<VAR>hb : ∀ (n : G), n ∈ s ↔ b * n * b⁻¹ ∈ s<VAR>n : G<GOAL>n ∈ s ↔ a * b * n * (a * b)⁻¹ ∈ s
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a✝ a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>a : G<VAR>ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s<VAR>n : G<GOAL>n ∈ s ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CommGroup β<VAR>s : Set α<VAR>t u : Finset α<VAR>d : ℕ<VAR>a : α<GOAL>¬MulDissociated s ↔ ∃ t u, ↑t ⊆ s ∧ ↑u ⊆ s ∧ Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a ≤ b<VAR>h : lfpApprox f x a ∈ fixedPoints ⇑f<GOAL>lfpApprox f x b = lfpApprox f x a
<VAR>α : Type u<VAR>inst✝ : CompleteLattice α<VAR>f : α →o α<VAR>x : α<VAR>a b : Ordinal.{u}<VAR>h_init : x ≤ f x<VAR>h_ab : a ≤ b<VAR>h : f (lfpApprox f x a) = lfpApprox f x a<GOAL>lfpApprox f x b = lfpApprox f x a
<VAR>n : ℕ<VAR>n2 : 2 < n<GOAL>4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
<VAR>n2 : 2 < 2 ^ 0<GOAL>4 ∣ 2 ^ 0 ∨ ∃ p, Prime p ∧ p ∣ 2 ^ 0 ∧ Odd p
<VAR>n2 : 2 < 2 ^ (0 + 1)<GOAL>4 ∣ 2 ^ (0 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (0 + 1) ∧ Odd p
<VAR>k : ℕ<VAR>n2 : 2 < 2 ^ (k + 1 + 1)<GOAL>4 ∣ 2 ^ (k + 1 + 1) ∨ ∃ p, Prime p ∧ p ∣ 2 ^ (k + 1 + 1) ∧ Odd p
<VAR>n : ℕ<VAR>n2 : 2 < n<VAR>p : ℕ<VAR>hp : Prime p<VAR>hdvd : p ∣ n<VAR>hodd : Odd p<GOAL>4 ∣ n ∨ ∃ p, Prime p ∧ p ∣ n ∧ Odd p
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidableEq α<VAR>x y : α<GOAL>(count x) (of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y
<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>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>∫ (v : ι → ℝ), cexp (-∑ i : ι, b i * ↑(v i) ^ 2 + ∑ i : ι, c i * ↑(v i)) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
<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>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>∫ (v : ι → ℝ), ∏ x : ι, cexp (-b x * ↑(v x) ^ 2 + c x * ↑(v x)) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
<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>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<GOAL>∏ i : ι, ∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = ∏ i : ι, (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
<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>ι : Type u_2<VAR>inst✝ : Fintype ι<VAR>b : ι → ℂ<VAR>hb : ∀ (i : ι), 0 < (b i).re<VAR>c : ι → ℂ<VAR>i : ι<VAR>this : (-b i).re < 0<GOAL>∫ (x : ℝ), cexp (-b i * ↑x ^ 2 + c i * ↑x) = (↑π / b i) ^ (1 / 2) * cexp (c i ^ 2 / (4 * b i))
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝³ : NonAssocSemiring α<VAR>inst✝² : Fintype m<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq m<VAR>x : α<VAR>v : m → α<VAR>x✝ : m<GOAL>(v ᵥ* diagonal fun x_1 => x) x✝ = (MulOpposite.op x • v) x✝
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a b : R<VAR>hab : a ≤ b<VAR>c : R<GOAL>star c * a * c ≤ star c * b * c
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a b : R<VAR>hab : ∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), b = a + p<VAR>c : R<GOAL>∃ p ∈ AddSubmonoid.closure (range fun s => star s * s), star c * b * c = star c * a * c + p
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a c p : R<VAR>hp : p ∈ AddSubmonoid.closure (range fun s => star s * s)<GOAL>∃ p_1 ∈ AddSubmonoid.closure (range fun s => star s * s), star c * (a + p) * c = star c * a * c + p_1
<VAR>R : Type u<VAR>inst✝³ : NonUnitalSemiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>a c p : R<VAR>hp : 0 ≤ p<GOAL>∃ p_1, 0 ≤ p_1 ∧ star c * (a + p) * c = star c * a * c + p_1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>op : β → β → β<VAR>hc : Std.Commutative op<VAR>ha : Std.Associative op<VAR>f : α → β<VAR>b : β<VAR>s : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>s₁ s₂ : Finset α<VAR>b₁ b₂ : β<GOAL>op (Multiset.fold op b₁ (Multiset.map f (s₁ ∪ s₂).val)) (Multiset.fold op b₂ (Multiset.map f (s₁ ∩ s₂).val)) = op (Multiset.fold op b₂ (Multiset.map f s₁.val)) (Multiset.fold op b₁ (Multiset.map f s₂.val))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : TopologicalSpace α<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝⁴ : (i : ι) → TopologicalSpace (π i)<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : TopologicalSpace γ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : One β<VAR>f : α → β<VAR>s : Set α<VAR>hs : ∀ a ∈ frontier s, f a = 1<VAR>hf : Continuous f<GOAL>Continuous (s.mulIndicator f)
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : [x-[ℝ]y] ⊆ s<GOAL>[x-[ℝ]x + (y - x)] ⊆ s
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ u✝ : Multiset α<VAR>a b : α<VAR>s t u : Multiset α<GOAL>s + t ∩ u = (s + t) ∩ (s + u)
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : ι → R<VAR>x : M<GOAL>(∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : ι → R<GOAL>(∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0
<VAR>G : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>α : Sort u_4<VAR>β : Sort u_5<VAR>ι : Sort u_6<VAR>inst✝⁵ : CommMonoid M✝<VAR>inst✝⁴ : CommMonoid N<VAR>R : Type u_7<VAR>M : Type u_8<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : NoZeroSMulDivisors R M<VAR>f : ι → R<VAR>x : M<VAR>hx : x ≠ 0<GOAL>(∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • 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<GOAL>{ f // ∀ (x y : M), f x * f y = 0 } ≃ { fg // (∀ (x y : M), fg.2 x * fg.2 y = 0) ∧ (∀ (r : R') (x : M), fg.2 (r •> x) = fg.1 r * fg.2 x) ∧ ∀ (r : R') (x : M), fg.2 (x <• r) = fg.2 x * fg.1 r }
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<VAR>f : ↑Γ(X, U)<VAR>hf₁ : X.basicOpen f ≤ V<VAR>hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<VAR>f : ↑Γ(X, U)<VAR>hf₁ : X.basicOpen f ≤ V<VAR>hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f<VAR>g : ↑Γ(X, V)<VAR>hg₁ : X.basicOpen g ≤ X.basicOpen f<VAR>hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<VAR>f : ↑Γ(X, U)<VAR>hf₁ : X.basicOpen f ≤ V<VAR>hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f<VAR>g : ↑Γ(X, V)<VAR>hg₁ : X.basicOpen g ≤ X.basicOpen f<VAR>hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g<VAR>f' : ↑Γ(X, U)<VAR>hf' : X.basicOpen f' = X.basicOpen ((X.presheaf.map (homOfLE hf₁).op) g)<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>X Y : Scheme<VAR>U : X.Opens<VAR>hU : IsAffineOpen U<VAR>f✝ : ↑Γ(X, U)<VAR>V : X.Opens<VAR>hV : IsAffineOpen V<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ U ⊓ V<VAR>f : ↑Γ(X, U)<VAR>hf₁ : X.basicOpen f ≤ V<VAR>hf₂ : ↑⟨x, ⋯⟩ ∈ X.basicOpen f<VAR>g : ↑Γ(X, V)<VAR>hg₁ : X.basicOpen g ≤ X.basicOpen f<VAR>hg₂ : ↑⟨x, hf₂⟩ ∈ X.basicOpen g<VAR>f' : ↑Γ(X, U)<VAR>hf' : X.basicOpen f' = X.toRingedSpace.basicOpen g<GOAL>∃ f g, X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>u v w : V<VAR>p : G.Walk u v<GOAL>v ∈ p.toSubgraph.verts
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : NonUnitalNonAssocRing R<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<GOAL>TopologicalRing R
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : NonUnitalNonAssocRing R<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<VAR>h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)<GOAL>TopologicalRing R
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : NonUnitalNonAssocRing R<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<VAR>h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)<GOAL>Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : NonUnitalNonAssocRing R<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<VAR>h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)<GOAL>∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
<VAR>R : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝³ : NonUnitalNonAssocRing R<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalAddGroup R<VAR>norm : R → 𝕜<VAR>norm_nonneg : ∀ (x : R), 0 ≤ norm x<VAR>norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y<VAR>nhds_basis : (𝓝 0).HasBasis (fun x => 0 < x) fun ε => {x | norm x < ε}<VAR>h0 : ∀ (f : R → R), ∀ c ≥ 0, (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)<GOAL>∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>s t : LowerSet α<VAR>a : α<VAR>f : (i : ι) → κ i → LowerSet α<GOAL>(⨆ i, ⨆ j, f i j).compl = ⨆ i, ⨆ j, (f i j).compl
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t✝ t₁ t₂ u t s s' : Set α<GOAL>t.ite s s' ∩ t = s ∩ t
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>h0 : n = n.minFac * 0<GOAL>¬0 < n
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>h0 : n = n.minFac * 0<GOAL>¬0 < 0
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>h1 : n = n.minFac * 1<GOAL>n.minFac ≤ n / n.minFac
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>h1 : n = n.minFac<GOAL>n.minFac ≤ n / n.minFac
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : n < 2<VAR>h1 : n = n.minFac<GOAL>n.minFac ≤ n / n.minFac
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>x : ℕ<VAR>hx : n = n.minFac * (x + 2)<GOAL>n.minFac ≤ n.minFac * (x + 2) / n.minFac
<VAR>n✝ n : ℕ<VAR>pos : 0 < n<VAR>np : ¬Prime n<VAR>x : ℕ<VAR>hx : n = n.minFac * (x + 2)<GOAL>n.minFac ≤ x + 2
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>rid : f ∈ asIdeal f_deg hm q<VAR>e_1✝ : ↑(CommRingCat.of (A⁰_ f)) = HomogeneousLocalization 𝒜 (Submonoid.powers f)<GOAL>1 = HomogeneousLocalization.mk { deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>rid : f ∈ asIdeal f_deg hm q<VAR>e_1✝ : ↑(CommRingCat.of (A⁰_ f)) = HomogeneousLocalization 𝒜 (Submonoid.powers f)<GOAL>1 = Localization.mk ↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.num ⟨↑{ deg := m * m, num := ⟨(proj 𝒜 m) f ^ m, ⋯⟩, den := ⟨f ^ m, ⋯⟩, den_mem := ⋯ }.den, ⋯⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>rid : f ∈ asIdeal f_deg hm q<VAR>e_1✝ : ↑(CommRingCat.of (A⁰_ f)) = HomogeneousLocalization 𝒜 (Submonoid.powers f)<GOAL>1 = Localization.mk (↑(((decompose 𝒜) f) m) ^ m) ⟨f ^ m, ⋯⟩
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>q : ↑↑(Spec A⁰_ f).toPresheafedSpace<VAR>rid : f ∈ asIdeal f_deg hm q<VAR>e_1✝ : ↑(CommRingCat.of (A⁰_ f)) = HomogeneousLocalization 𝒜 (Submonoid.powers f)<GOAL>1 = Localization.mk (f ^ m) ⟨f ^ m, ⋯⟩
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<VAR>h : b = a⁻¹ * c<GOAL>a * b = c
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>p : (ι → ℝ) → Box ι → Prop<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<GOAL>(∀ J ∈ π.biUnionTagged πi, p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
<VAR>ι : Type u_1<VAR>I J : Box ι<VAR>p : (ι → ℝ) → Box ι → Prop<VAR>π : Prepartition I<VAR>πi : (J : Box ι) → TaggedPrepartition J<GOAL>(∀ (J : Box ι), (∃ J' ∈ π, J ∈ πi J') → p ((π.biUnionTagged πi).tag J) J) ↔ ∀ J ∈ π, ∀ J' ∈ πi J, p ((πi J).tag J') J'
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>⋃₀ ↑(hC.diffFinset₀ hs hI) ⊆ s
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>I : Finset (Set α)<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>hI : ↑I ⊆ C<GOAL>s \ ⋃₀ ↑I ⊆ s
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : ¬AEMeasurable f μ<GOAL>μ.tilted f = 0
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : ¬AEMeasurable f μ<GOAL>¬Integrable (fun x => rexp (f x)) μ
<VAR>α : Type u_1<VAR>mα : MeasurableSpace α<VAR>μ : Measure α<VAR>f : α → ℝ<VAR>hf : ¬AEMeasurable f μ<GOAL>¬AEMeasurable (fun x => rexp (f x)) μ
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Ioi a, g' x ≤ 0<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>IntegrableOn g' (Ioi a) volume
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>g g' : ℝ → ℝ<VAR>a b l : ℝ<VAR>m : E<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>hderiv : ∀ x ∈ Ici a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Ioi a, g' x ≤ 0<VAR>hg : Tendsto g atTop (𝓝 l)<GOAL>ContinuousWithinAt g (Ici a) a
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝ : Group G<VAR>a b : G<GOAL>(fun b => b * a) ((fun b => b / a) b) = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>M : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>Q : Type u_9<VAR>G : Type u_10<VAR>H : Type u_11<VAR>inst✝ : Group G<VAR>a b : G<GOAL>(fun b => b / a) ((fun b => b * a) b) = b
<VAR>n : ℕ<GOAL>(fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>n : ℕ<VAR>this : ((fun x => Complex.exp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) ∘ Complex.ofReal') =O[𝓝 0] ((fun x => x ^ n) ∘ Complex.ofReal')<GOAL>(fun x => rexp x - ∑ i ∈ Finset.range n, x ^ i / ↑i !) =O[𝓝 0] fun x => x ^ n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>T' : Triangle C<VAR>φ : (j : J) → T' ⟶ T j<GOAL>T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j => (φ j).hom₁) = (Pi.lift fun j => (φ j).hom₃) ≫ (Pi.map fun j => (T j).mor₃) ≫ inv (piComparison (shiftFunctor C 1) fun j => (T j).obj₁)
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>inst✝⁴ : HasShift C ℤ<VAR>T₁ T₂ T₃ : Triangle C<VAR>J : Type u_1<VAR>T : J → Triangle C<VAR>inst✝³ : HasProduct fun j => (T j).obj₁<VAR>inst✝² : HasProduct fun j => (T j).obj₂<VAR>inst✝¹ : HasProduct fun j => (T j).obj₃<VAR>inst✝ : HasProduct fun j => (shiftFunctor C 1).obj (T j).obj₁<VAR>T' : Triangle C<VAR>φ : (j : J) → T' ⟶ T j<GOAL>(T'.mor₃ ≫ (shiftFunctor C 1).map (Pi.lift fun j => (φ j).hom₁) ≫ piComparison (shiftFunctor C 1) fun j => (T j).obj₁) = (Pi.lift fun j => (φ j).hom₃) ≫ Pi.map fun j => (T j).mor₃
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>P : Submodule ℕ M<VAR>x✝ : P.FG<VAR>S : Finset M<VAR>hS : span ℕ ↑S = P<GOAL>AddSubmonoid.closure ↑S = P.toAddSubmonoid
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>P : Submodule ℕ M<VAR>x✝ : P.FG<VAR>S : Finset M<VAR>hS : AddSubmonoid.closure ↑S = P.toAddSubmonoid<GOAL>span ℕ ↑S = P
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x✝ y x : V<GOAL>arccos (⟪0, x⟫_ℝ / (‖0‖ * ‖x‖)) = π / 2
<VAR>α✝ : Type u_1<VAR>G✝ : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Inv G✝<VAR>inst✝⁴ : MeasurableSpace G✝<VAR>inst✝³ : MeasurableInv G✝<VAR>m : MeasurableSpace α<VAR>f✝ : α → G✝<VAR>μ : Measure α<VAR>G : Type u_4<VAR>inst✝² : Group G<VAR>inst✝¹ : MeasurableSpace G<VAR>inst✝ : MeasurableInv G<VAR>f : α → G<VAR>h : AEMeasurable (fun x => (f x)⁻¹) μ<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>f^[n + minimalPeriod f x] x = f^[n] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>f^[n] (f^[minimalPeriod f x] x) = f^[n] x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f fa : α → α<VAR>fb : β → β<VAR>x y : α<VAR>m n : ℕ<GOAL>f^[minimalPeriod f x] x = x
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M k = ⊥<GOAL>∃ k, ∀ (x : L), (toEnd R L M) x ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M k = ⊥<GOAL>∀ (x : L), (toEnd R L M) x ^ k = 0
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M k = ⊥<VAR>x : L<VAR>m : M<GOAL>((toEnd R L M) x ^ k) m = 0 m
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>k✝ : ℕ<VAR>N : LieSubmodule R L M<VAR>M₂ : Type w₁<VAR>inst✝³ : AddCommGroup M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : LieRingModule L M₂<VAR>inst✝ : LieModule R L M₂<VAR>k : ℕ<VAR>hM : lowerCentralSeries R L M k = ⊥<VAR>x : L<VAR>m : M<GOAL>(⇑((toEnd R L M) x))^[k] m ∈ lowerCentralSeries R L M k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>M : Type u_3<VAR>inst✝² : AddCommMonoid M<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : OrderedAddCommMonoid M<VAR>s✝ : SignedMeasure α<VAR>i j : Set α<VAR>s : SignedMeasure α<GOAL>∃ i, MeasurableSet i ∧ restrict 0 i ≤ restrict s i ∧ restrict s iᶜ ≤ restrict 0 iᶜ