ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁷ : MeasurableSpace X<VAR>μ : Measure X<VAR>𝕜 : Type u_5<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>p : ℝ≥0∞<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : NormedSpace ℝ F<VAR>f : X → ℝ≥0<VAR>f_meas : Measurable f<VAR>g : X → E<VAR>hE : CompleteSpace E<VAR>hg : Integrable g (μ.withDensity fun x => ↑(f x))<GOAL>∀ ⦃f_1 g : X → E⦄, f_1 =ᶠ[ae (μ.withDensity fun x => ↑(f x))] g → Integrable f_1 (μ.withDensity fun x => ↑(f x)) → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) f_1 → (fun g => (∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ) g
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : q.degree < p.degree<GOAL>(p + q).leadingCoeff = p.leadingCoeff
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>h : q.degree < p.degree<GOAL>(q + p).leadingCoeff = p.leadingCoeff
<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>c : ℝ<VAR>li : ℂ ≃ₗᵢ[ℝ] ℂ<GOAL>(∃ map, restrictScalars ℝ map = c • li.toLinearIsometry.toContinuousLinearMap) ∨ ∃ map, restrictScalars ℝ map = (c • li.toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE
<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>c : ℝ<VAR>a : ↥circle<GOAL>(∃ map, restrictScalars ℝ map = c • (rotation a).toLinearIsometry.toContinuousLinearMap) ∨ ∃ map, restrictScalars ℝ map = (c • (rotation a).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE
<VAR>f : ℂ → ℂ<VAR>z : ℂ<VAR>c : ℝ<VAR>a : ↥circle<GOAL>(∃ map, restrictScalars ℝ map = c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap) ∨ ∃ map, restrictScalars ℝ map = (c • (conjLIE.trans (rotation a)).toLinearIsometry.toContinuousLinearMap).comp ↑conjCLE
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝³ : Semiring α<VAR>inst✝² : Semiring β<VAR>b : α<VAR>m n : ℕ<VAR>inst✝¹ : FunLike F α β<VAR>inst✝ : RingHomClass F α β<VAR>f : F<VAR>a : α<GOAL>Odd (f (2 * a + 1))
<VAR>s t : Set ℝ<GOAL>(convexHull ℝ) (⇑equivRealProdLm ⁻¹' s ×ˢ t) = ⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t)
<VAR>s t : Set ℝ<GOAL>⇑equivRealProdLm ⁻¹' (convexHull ℝ) (s ×ˢ t) = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
<VAR>s t : Set ℝ<GOAL>⇑equivRealProdLm ⁻¹' (convexHull ℝ) s ×ˢ (convexHull ℝ) t = (convexHull ℝ) s ×ℂ (convexHull ℝ) t
<VAR>Γ : Subgroup SL(2, ℤ)<VAR>k✝ : ℤ<VAR>f : ℍ → ℂ<VAR>α : Type u_1<VAR>inst✝¹ : SMul α ℂ<VAR>inst✝ : IsScalarTower α ℂ ℂ<VAR>k : ℤ<VAR>A : ↥GL(2, ℝ)⁺<VAR>x✝ : ℍ<GOAL>(0 ∣[k]A) x✝ = 0 x✝
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>P : Set X → Prop := fun x => True<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : NormalSpace X<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hd : Disjoint s t<VAR>P : Set X → Prop := fun x => True<VAR>c : Urysohns.CU P := { C := s, U := tᶜ, P_C := trivial, closed_C := hs, open_U := ⋯, subset := ⋯, hP := ⋯ }<GOAL>∃ f, EqOn (⇑f) 0 s ∧ EqOn (⇑f) 1 t ∧ ∀ (x : X), f x ∈ Icc 0 1
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<VAR>hp' : p ≠ 0<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<VAR>hp' : p ≠ 0<VAR>H₁ : Summable fun i => (f i + g i) ^ p<VAR>H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<VAR>hp' : p ≠ 0<VAR>H₁ : Summable fun i => (f i + g i) ^ p<VAR>H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)<VAR>hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>A B : ℝ≥0<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>hf : HasSum (fun i => f i ^ p) (A ^ p)<VAR>hg : HasSum (fun i => g i ^ p) (B ^ p)<VAR>hp' : p ≠ 0<VAR>H₁ : Summable fun i => (f i + g i) ^ p<VAR>H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)<VAR>hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)<VAR>hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)<GOAL>∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>(adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a)) = α
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>l₁ l₂ : List α<VAR>a : α<GOAL>l₁.diff (a :: l₂) = (l₁.erase a).diff l₂
<VAR>R : Type u_1<VAR>inst✝¹⁰ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : Module R M<VAR>N : Type u_3<VAR>inst✝⁷ : AddCommMonoid N<VAR>inst✝⁶ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁵ : DecidableEq ι<VAR>x y z : M<VAR>S : Type u_5<VAR>inst✝⁴ : OrderedCommSemiring S<VAR>inst✝³ : Algebra S R<VAR>inst✝² : Module S M<VAR>inst✝¹ : SMulPosMono S R<VAR>inst✝ : IsScalarTower S R M<VAR>a : S<VAR>h : SameRay R x y<VAR>ha : 0 ≤ a<VAR>hy : y = 0<GOAL>a • y = 0
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : (⇑φ)^[2] = _root_.id<VAR>g : G<GOAL>φ g = g⁻¹
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>φ : G →* G<VAR>inst✝ : Finite G<VAR>hφ : FixedPointFree ⇑φ<VAR>h2 : (⇑φ)^[2] = _root_.id<VAR>g : G<VAR>key : 1 * g * φ g = 1<GOAL>φ g = g⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s✝ : ι → Set α<VAR>t✝ : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>s : ι → Set α<VAR>h : Directed (fun x x_1 => x ≥ x_1) s<VAR>inst✝ : Nonempty ι<VAR>t : Set α<GOAL>t ∈ ⨅ i, 𝓟 (s i) ↔ ∃ i, True ∧ s i ⊆ t
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>s : Set α<VAR>f : α →₀ M<GOAL>↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>s : Set α<VAR>f : α →₀ M<GOAL>(∀ (x : α), f x ≠ 0 → x ∈ s) ↔ ∀ a ∉ s, f a = 0
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<GOAL>closedBall x ε \ ball x ε = sphere x ε
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝²⁴ : Semiring R₁<VAR>inst✝²³ : Semiring R₂<VAR>inst✝²² : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>inst✝²¹ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁰ : RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>inst✝¹⁹ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝¹⁸ : RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>inst✝¹⁷ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝¹⁶ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝¹⁵ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝¹⁴ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>inst✝¹³ : TopologicalSpace M₁<VAR>inst✝¹² : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹¹ : TopologicalSpace M'₁<VAR>inst✝¹⁰ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝⁹ : TopologicalSpace M₂<VAR>inst✝⁸ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁷ : TopologicalSpace M₃<VAR>inst✝⁶ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁵ : TopologicalSpace M₄<VAR>inst✝⁴ : AddCommMonoid M₄<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : Module R₁ M'₁<VAR>inst✝¹ : Module R₂ M₂<VAR>inst✝ : Module R₃ M₃<VAR>e : M₁ ≃SL[σ₁₂] M₂<VAR>x : M₁<GOAL>(⇑e.symm ∘ ⇑e) x = id x
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<VAR>hc : dslope f c z = 0<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<VAR>hc : dslope f c z ≠ 0<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<VAR>hc : dslope f c z ≠ 0<VAR>g : E →L[ℂ] ℂ<VAR>hg : ‖g‖ = 1<VAR>hgf : g (dslope f c z) = ↑‖dslope f c z‖<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<VAR>hc : dslope f c z ≠ 0<VAR>g : E →L[ℂ] ℂ<VAR>hg : ‖g‖ = 1<VAR>hgf : g (dslope f c z) = ↑‖dslope f c z‖<VAR>hg' : ‖g‖₊ = 1<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R R₁ R₂ : ℝ<VAR>f : ℂ → E<VAR>c z z₀ : ℂ<VAR>hd : DifferentiableOn ℂ f (ball c R₁)<VAR>h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)<VAR>hz : z ∈ ball c R₁<VAR>hR₁ : 0 < R₁<VAR>hR₂ : 0 < R₂<VAR>hc : dslope f c z ≠ 0<VAR>g : E →L[ℂ] ℂ<VAR>hg : ‖g‖ = 1<VAR>hgf : g (dslope f c z) = ↑‖dslope f c z‖<VAR>hg' : ‖g‖₊ = 1<VAR>hg₀ : ‖g‖₊ ≠ 0<GOAL>‖dslope f c z‖ ≤ R₂ / R₁
<VAR>R : Type u_1<VAR>inst✝ : AddGroupWithOne R<VAR>H : ∀ (n : ℕ), ↑n = 0 → n = 0<VAR>m : ℕ<VAR>ih : ∀ (n : ℕ), ↑m = ↑n → m = n<VAR>n : ℕ<VAR>h : ↑(m + 1) = ↑(n + 1)<GOAL>m + 1 = n + 1
<VAR>R : Type u_1<VAR>inst✝ : AddGroupWithOne R<VAR>H : ∀ (n : ℕ), ↑n = 0 → n = 0<VAR>m : ℕ<VAR>ih : ∀ (n : ℕ), ↑m = ↑n → m = n<VAR>n : ℕ<VAR>h : ↑m = ↑n<GOAL>m + 1 = n + 1
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f✝ : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>ha : a ∉ s<VAR>f : α → ℕ<GOAL>multinomial (cons a s ha) f = (f a + ∑ i ∈ s, f i).choose (f a) * multinomial s f
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f✝ : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>ha : a ∉ s<VAR>f : α → ℕ<GOAL>0 < ∏ i ∈ cons a s ha, (f i)!
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<GOAL>(∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<VAR>this : -((∑ i ∈ range n, x ^ i) * (x - 1)) = -(x ^ n - 1)<GOAL>(∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
<VAR>α : Type u<VAR>inst✝ : Ring α<VAR>x : α<VAR>n : ℕ<VAR>this : (∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n<GOAL>(∑ i ∈ range n, x ^ i) * (1 - x) = 1 - x ^ n
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Algebra R A<VAR>S T : Set A<VAR>M✝ N P Q : Submodule R A<VAR>m n✝ : A<VAR>n : ℕ<VAR>M : Submodule R Aᵐᵒᵖ<GOAL>map (↑(opLinearEquiv R).symm) (M ^ n) = map (↑(opLinearEquiv R).symm) M ^ n
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>r : S<VAR>s : Set S<GOAL>absNorm (span {r}) ∣ ((Algebra.norm ℤ) r).natAbs
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s✝ t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<GOAL>s.toFinset.card = 1 ↔ Multiset.card s ≠ 0 ∧ ∃ a, s = Multiset.card s • {a}
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<GOAL>∫ (x : E), ∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) ∂μ = ∫ (x : E), -∫ (t : ℝ), (B (f' (x, t))) (g (x, t)) ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<GOAL>(fun a => ∫ (t : ℝ), (B (f (a, t))) (g' (a, t))) =ᶠ[ae μ] fun a => -∫ (t : ℝ), (B (f' (a, t))) (g (a, t))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>x : E<VAR>hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume<VAR>hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume<VAR>hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume<GOAL>∫ (t : ℝ), (B (f (x, t))) (g' (x, t)) = -∫ (t : ℝ), (B (f' (x, t))) (g (x, t))
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>x : E<VAR>hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume<VAR>hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume<VAR>hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume<GOAL>∀ (x_1 : ℝ), HasDerivAt (fun x_2 => f (x, x_2)) (f' (x, x_1)) x_1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<VAR>x : E<VAR>hf'gx : Integrable (fun y => (B (f' (x, y))) (g (x, y))) volume<VAR>hfg'x : Integrable (fun y => (B (f (x, y))) (g' (x, y))) volume<VAR>hfgx : Integrable (fun y => (B (f (x, y))) (g (x, y))) volume<GOAL>∀ (x_1 : ℝ), HasDerivAt (fun x_2 => g (x, x_2)) (g' (x, x_1)) x_1
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>G : Type u_3<VAR>W : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℝ E<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>inst✝⁷ : NormedSpace ℝ F<VAR>inst✝⁶ : NormedAddCommGroup G<VAR>inst✝⁵ : NormedSpace ℝ G<VAR>inst✝⁴ : NormedAddCommGroup W<VAR>inst✝³ : NormedSpace ℝ W<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : SigmaFinite μ<VAR>f f' : E × ℝ → F<VAR>g g' : E × ℝ → G<VAR>B : F →L[ℝ] G →L[ℝ] W<VAR>hf'g : Integrable (fun x => (B (f' x)) (g x)) (μ.prod volume)<VAR>hfg' : Integrable (fun x => (B (f x)) (g' x)) (μ.prod volume)<VAR>hfg : Integrable (fun x => (B (f x)) (g x)) (μ.prod volume)<VAR>hf : ∀ (x : E × ℝ), HasLineDerivAt ℝ f (f' x) x (0, 1)<VAR>hg : ∀ (x : E × ℝ), HasLineDerivAt ℝ g (g' x) x (0, 1)<GOAL>∫ (x : E), -∫ (t : ℝ), (B (f' (x, t))) (g (x, t)) ∂μ = -∫ (x : E × ℝ), (B (f' x)) (g x) ∂μ.prod volume
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>x : R<GOAL>(laurent r) (C x) = C x
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<GOAL>finrank R M = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<VAR>h✝ : Subsingleton R<GOAL>finrank R M = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<VAR>h✝ : Nontrivial R<GOAL>finrank R M = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<VAR>h✝ : Nontrivial R<VAR>w✝ : Set M<VAR>b : Basis (↑w✝) R M<GOAL>finrank R M = 0
<VAR>R : Type u<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>ι : Type w<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : AddCommGroup M<VAR>inst✝⁷ : AddCommGroup M'<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R M'<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Nontrivial R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : Module.Free R M<VAR>h : ∀ (s : Set M), Basis (↑s) R M → ¬s.Finite<VAR>h✝ : Nontrivial R<VAR>w✝ : Set M<VAR>b : Basis (↑w✝) R M<VAR>this : Infinite ↑w✝<GOAL>finrank R M = 0
<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>h₁ : IsClosed s₁<VAR>h₂ : IsClosed s₂<GOAL>IsClosed (s₁ ∩ s₂)
<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>h₁ : IsOpen s₁ᶜ<VAR>h₂ : IsOpen s₂ᶜ<GOAL>IsOpen (s₁ ∩ s₂)ᶜ
<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>h₁ : IsOpen s₁ᶜ<VAR>h₂ : IsOpen s₂ᶜ<GOAL>IsOpen (s₁ᶜ ∪ s₂ᶜ)
<VAR>C : Type u_1<VAR>inst✝ : Category.{u_2, u_1} C<VAR>n m : ℕ<VAR>F G : ComposableArrows C n<VAR>obj : Fin (n + 1) → C<VAR>mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ<VAR>i : ℕ<VAR>hi : autoParam (i < n) _auto✝<GOAL>((mkOfObjOfMapSucc obj mapSucc).arrow i hi).hom = eqToHom ⋯ ≫ (mk₁ (mapSucc ⟨i, hi⟩)).hom ≫ eqToHom ⋯
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : Zero M<VAR>a✝ a' : α<VAR>b✝ : M<VAR>a x : α<VAR>b : M<GOAL>(single a b) x = 0 ↔ x = a → b = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m : MeasurableSpace Ω<VAR>X : Ω → ℝ<VAR>p : ℕ<VAR>μ : Measure Ω<VAR>hp : p ≠ 0<GOAL>centralMoment 0 p μ = 0
<VAR>n : ℕ<GOAL>eulerMascheroniSeq n < eulerMascheroniSeq (n + 1)
<VAR>n : ℕ<GOAL>log (1 + (↑n + 1)⁻¹) < (↑n + 1)⁻¹
<VAR>n : ℕ<GOAL>0 < 1 + (↑n + 1)⁻¹
<VAR>n : ℕ<GOAL>0 < (↑n + 1)⁻¹
<VAR>n : ℕ<GOAL>1 + (↑n + 1)⁻¹ - 1 = (↑n + 1)⁻¹
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>x : M ⧸ S<GOAL>‖x‖ = infDist 0 {m | ↑m = x}
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>f g : ℕ → R<VAR>hf : ∀ (n : ℕ), 0 < n → f n ≠ 0<VAR>hg : ∀ (n : ℕ), 0 < n → g n ≠ 0<GOAL>(∀ n > 0, ∏ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, ∏ x ∈ n.divisorsAntidiagonal, g x.2 ^ μ x.1 = f n
<VAR>R : Type u_1<VAR>inst✝ : CommGroupWithZero R<VAR>f g : ℕ → R<VAR>hf : ∀ (n : ℕ), 0 < n → f n ≠ 0<VAR>hg : ∀ (n : ℕ), 0 < n → g n ≠ 0<VAR>n : ℕ<VAR>hn : n > 0<GOAL>∏ i ∈ n.divisors, f i = g n ↔ (∏ i ∈ n.divisors, if h : 0 < i then Units.mk0 (f i) ⋯ else 1) = if h : 0 < n then Units.mk0 (g n) ⋯ else 1