ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>u : Set τ<VAR>hu : u ∈ f<GOAL>⋂ u, closure (image2 ϕ (↑u) s) ⊆ closure (image2 ϕ u s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>a✝ : β<VAR>hx : a✝ ∈ ⋂ u, closure (image2 ϕ (↑u) s)<GOAL>a✝ ∈ closure (image2 ϕ u s)
<VAR>τ : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_4<VAR>inst✝ : TopologicalSpace β<VAR>f : Filter τ<VAR>ϕ : τ → α → β<VAR>s s₁ s₂ : Set α<VAR>u : Set τ<VAR>hu : u ∈ f<VAR>a✝ : β<VAR>hx : ∀ (i : ↑f.sets), a✝ ∈ closure (image2 ϕ (↑i) s)<GOAL>a✝ ∈ closure (image2 ϕ u s)
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>f : AdjoinRoot g<GOAL>(mk g) ((modByMonicHom hg) f) = f
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>p✝ : R[X]<GOAL>(mk g) ((modByMonicHom hg) ((mk g) p✝)) = (mk g) p✝
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>g : R[X]<VAR>hg : g.Monic<VAR>p✝ : R[X]<GOAL>g ∣ g * (p✝ /ₘ g)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>(f * ↑ζ) x = ∑ i ∈ x.divisors, f i
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : ArithmeticFunction R<VAR>x : ℕ<GOAL>∑ x ∈ x.divisorsAntidiagonal, f x.1 * ↑ζ x.2 = ∑ i ∈ x.divisors, f i
<VAR>a b m n✝ p n : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hn : n ≠ 0<VAR>hf : ∀ p ∈ f.support, Prime p<VAR>h : f = n.factorization<GOAL>(f.prod fun x x_1 => x ^ x_1) = n
<VAR>a b m n✝ p n : ℕ<VAR>f : ℕ →₀ ℕ<VAR>hn : n ≠ 0<VAR>hf : ∀ p ∈ f.support, Prime p<VAR>h : (f.prod fun x x_1 => x ^ x_1) = n<GOAL>f = n.factorization
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<GOAL>μ.withDensityᵥ f = (μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<GOAL>μ.withDensityᵥ f = (μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<GOAL>μ.withDensityᵥ f = (μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>E : Type u_3<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f✝ g : α → E<VAR>f : α → ℝ<VAR>hfi : Integrable f μ<VAR>this✝ : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))<VAR>this : IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal ((-f) x))<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(μ.withDensityᵥ f) i = ↑((μ.withDensity fun x => ENNReal.ofReal (f x)).toSignedMeasure - (μ.withDensity fun x => ENNReal.ofReal (-f x)).toSignedMeasure) i
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>uas : Set (UniformSpace α)<VAR>ubs : Set (UniformSpace β)<VAR>ua : UniformSpace α<VAR>ub : UniformSpace β<VAR>uc : UniformSpace γ<VAR>ha : ua ∈ uas<VAR>hb : ub ∈ ubs<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>x✝ : UniformSpace (α × β) := instUniformSpaceProd<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>uas : Set (UniformSpace α)<VAR>ubs : Set (UniformSpace β)<VAR>ua : UniformSpace α<VAR>ub : UniformSpace β<VAR>uc : UniformSpace γ<VAR>ha✝ : ua ∈ uas<VAR>hb : ub ∈ ubs<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>x✝ : UniformSpace (α × β) := instUniformSpaceProd<VAR>ha : UniformContinuous id<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>uas : Set (UniformSpace α)<VAR>ubs : Set (UniformSpace β)<VAR>ua : UniformSpace α<VAR>ub : UniformSpace β<VAR>uc : UniformSpace γ<VAR>ha✝ : ua ∈ uas<VAR>hb✝ : ub ∈ ubs<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>x✝ : UniformSpace (α × β) := instUniformSpaceProd<VAR>ha : UniformContinuous id<VAR>hb : UniformContinuous id<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>α✝ : Type ua<VAR>β✝ : Type ub<VAR>γ✝ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝² : UniformSpace α✝<VAR>inst✝¹ : UniformSpace β✝<VAR>inst✝ : UniformSpace γ✝<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>f : α → β → γ<VAR>uas : Set (UniformSpace α)<VAR>ubs : Set (UniformSpace β)<VAR>ua : UniformSpace α<VAR>ub : UniformSpace β<VAR>uc : UniformSpace γ<VAR>ha✝ : ua ∈ uas<VAR>hb✝ : ub ∈ ubs<VAR>hf : UniformContinuous fun p => f p.1 p.2<VAR>x✝ : UniformSpace (α × β) := instUniformSpaceProd<VAR>ha : UniformContinuous id<VAR>hb : UniformContinuous id<VAR>h_unif_cont_id : UniformContinuous (Prod.map id id)<GOAL>UniformContinuous fun p => f p.1 p.2
<VAR>K : Type ?u.611342<VAR>L : Type ?u.611345<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p q : K[X]<VAR>hp : p ≠ 0<VAR>hpq : Associated p q<GOAL>(aeval (root q)) p = 0
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>b ≤ max |a| |c|
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>a b c d : α<VAR>hab : a ≤ b<VAR>hbc : b ≤ c<GOAL>-b ≤ max |a| |c|
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Field K<VAR>inst✝ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>X : { p // p ∣ J }<GOAL>(idealFactorsFunOfQuotHom ⋯) X = OrderHom.id X
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a : α<GOAL>⌊1⌋ = 1
<VAR>R : Type u<VAR>inst✝² : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝¹ : Field F<VAR>W : Jacobian F<VAR>S : Type u_1<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>P Q : Fin 3 → R<GOAL>dblXYZ (map W' f) (⇑f ∘ P) = ⇑f ∘ W'.dblXYZ P
<VAR>A : Type u_1<VAR>inst✝³ : AddCommGroup A<VAR>inst✝² : Module ℂ A<VAR>inst✝¹ : StarAddMonoid A<VAR>inst✝ : StarModule ℂ A<VAR>a : A<GOAL>↑((skewAdjoint.negISMul ∘ₗ skewAdjointPart ℝ) a) = -I • 2⁻¹ • (a - star a)
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>S : Ideal R<VAR>inst✝ : IsPrincipal S<VAR>is_prime : S.IsPrime<VAR>ne_bot : S ≠ ⊥<VAR>x✝¹ x✝ : R<GOAL>generator S ∣ x✝¹ * x✝ → generator S ∣ x✝¹ ∨ generator S ∣ x✝
<VAR>C : Type u_1<VAR>inst✝ : Category.{?u.42576, u_1} C<VAR>n m : ℕ<VAR>F✝ G✝ F G : ComposableArrows C n<VAR>app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i<VAR>w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi<VAR>i : ℕ<VAR>hi : i < n<GOAL>G.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).inv = (app ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi
<VAR>C : Type u_1<VAR>inst✝² : Category.{?u.206122, u_1} C<VAR>inst✝¹ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>k : A ⟶ S.X₂<VAR>hk : k ≫ S.g = 0<VAR>inst✝ : S.HasLeftHomology<VAR>x : A ⟶ S.X₁<VAR>hx : k = x ≫ S.f<GOAL>k ≫ S.g = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : ↑(MonCat.of G)<GOAL>((ofMulAction k G G).ρ g ≫ (Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) = ((Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) ≫ A.ρ g
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : ↑(MonCat.of G)<VAR>y : G<GOAL>(((ofMulAction k G G).ρ g ≫ (Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) ∘ₗ Finsupp.lsingle y) 1 = ((((Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) ≫ A.ρ g) ∘ₗ Finsupp.lsingle y) 1
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : ↑(MonCat.of G)<VAR>y : G<GOAL>((Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) (((ofMulAction k G G).ρ g) (Finsupp.single y 1)) = (A.ρ g) (((Finsupp.lift (↑A.V) k G) fun g => (A.ρ g) x) (Finsupp.single y 1))
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : ↑(MonCat.of G)<VAR>y : G<GOAL>((Finsupp.single (g • y) 1).sum fun x_1 r => r • (A.ρ x_1) x) = (A.ρ g) ((Finsupp.single y 1).sum fun x_1 r => r • (A.ρ x_1) x)
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : ↑(MonCat.of G)<VAR>y : G<GOAL>(A.ρ g * A.ρ y) x = (A.ρ g) ((A.ρ y) x)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>l : List ℤ<VAR>n : ℤ<GOAL>l.prod % n = (map (fun x => x % n) l).prod % n
<VAR>K : Type u_1<VAR>V : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : IsAlgClosed K<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<GOAL>⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤
<VAR>K : Type u_1<VAR>inst✝⁷ : Field K<VAR>R : Type u_3<VAR>M : Type u_4<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : IsAlgClosed K<VAR>n : ℕ<VAR>ih : ∀ m < n, ∀ {V : Type u_2} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V), finrank K V = m → ⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤<VAR>V : Type u_2<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>f : End K V<VAR>h_dim : finrank K V = n<GOAL>⨆ μ, ⨆ k, (f.genEigenspace μ) k = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f✝ : β × γ → E<VAR>hE : CompleteSpace E<GOAL>Integrable f✝ ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f✝ z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f✝ (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f✝ : β × γ → E<VAR>hE : CompleteSpace E<GOAL>∀ (c : E) ⦃s : Set (β × γ)⦄, MeasurableSet s → ((κ ⊗ₖ η) a) s < ⊤ → ∫ (z : β × γ), s.indicator (fun x => c) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f✝ : β × γ → E<VAR>hE : CompleteSpace E<GOAL>∀ ⦃f g : β × γ → E⦄, Disjoint (support f) (support g) → Integrable f ((κ ⊗ₖ η) a) → Integrable g ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a → ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a → ∫ (z : β × γ), (f + g) z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), (f + g) (x, y) ∂η (a, x) ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f✝ : β × γ → E<VAR>hE : CompleteSpace E<GOAL>IsClosed {f | ∫ (z : β × γ), ↑↑f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>E : Type u_4<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>κ : Kernel α β<VAR>inst✝⁵ : IsSFiniteKernel κ<VAR>η : Kernel (α × β) γ<VAR>inst✝⁴ : IsSFiniteKernel η<VAR>a : α<VAR>inst✝³ : NormedSpace ℝ E<VAR>E' : Type u_5<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : CompleteSpace E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>f✝ : β × γ → E<VAR>hE : CompleteSpace E<GOAL>∀ ⦃f g : β × γ → E⦄, f =ᶠ[ae ((κ ⊗ₖ η) a)] g → Integrable f ((κ ⊗ₖ η) a) → ∫ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a → ∫ (z : β × γ), g z ∂(κ ⊗ₖ η) a = ∫ (x : β), ∫ (y : γ), g (x, y) ∂η (a, x) ∂κ a
<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₁ x₂ y₁ L : R<GOAL>(map W f).toAffine.addY (f x₁) (f x₂) (f y₁) (f L) = f ((toAffine W).addY x₁ x₂ y₁ L)
<VAR>n : ℕ<GOAL>range' n (n + 1 - n) = [n]
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.leadingCoeff * a ≠ 0<GOAL>(p * C a).natDegree = p.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.leadingCoeff * a ≠ 0<GOAL>p.natDegree ∈ (p * C a).support
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>h : p.leadingCoeff * a ≠ 0<GOAL>(p * C a).coeff p.natDegree ≠ 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (β × β)<VAR>hs : s ∈ 𝓤 β<VAR>x : β × β<VAR>h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)<GOAL>x ∈ s
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k : T.LocalizationMap Q<VAR>z : N<GOAL>k.toMap (g ↑(f.sec z).2) * (f.map hy k) z = k.toMap (g (f.sec z).1)
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<VAR>eif : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a<VAR>uif : ∀ (f g : Multiset α), (∀ x ∈ f, Irreducible x) → (∀ x ∈ g, Irreducible x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g<VAR>a✝³ : α<VAR>a✝² : a✝³ ≠ 0<VAR>x✝ : Multiset α<VAR>a✝¹ : α<VAR>a✝ : a✝¹ ∈ x✝<GOAL>Prime a✝¹ ↔ Irreducible a✝¹
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N✝ N₁ N₂ P P₁ P₂ N : Submodule R M<VAR>x : M<VAR>r : R<GOAL>r ∈ N.colon (span R {x}) ↔ ∀ (a : R), r • a • x ∈ N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N✝ N₁ N₂ P P₁ P₂ N : Submodule R M<VAR>x : M<VAR>r : R<GOAL>(∀ (a : R), r • a • x ∈ N) ↔ r • x ∈ N
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>N✝ N₁ N₂ P P₁ P₂ N : Submodule R M<VAR>x : M<VAR>r : R<GOAL>(∀ (a : R), a • r • x ∈ N) ↔ r • x ∈ N
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r : R[X]<VAR>hp : p ≠ 0<VAR>hq : Monic 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r : R[X]<VAR>hp : p ≠ 0<VAR>hq : 0 = 1<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p r : R[X]<VAR>hp : 0 ≠ 0<VAR>hq : 0 = 1<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℤ<GOAL>(C a * T n).support ⊆ {n}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>a : R<VAR>n : ℤ<GOAL>(Finsupp.single n a).support ⊆ {n}
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Algebra R S<VAR>σ : Type u_1<VAR>i : σ<GOAL>(mvPolynomialBasis R σ).repr ((D R (MvPolynomial σ R)) (MvPolynomial.X i)) = Finsupp.single i 1
<VAR>n : ℕ<GOAL>(2 * (n + 1))‼ = 2 ^ (n + 1) * (n + 1)!
<VAR>n : ℕ<GOAL>(2 * n + 2) * (2 ^ n * n !) = 2 ^ n * 2 * ((n + 1) * n !)
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤<GOAL>∀ᵐ (x : α) ∂μ, Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))<VAR>h'x : f x = AEMeasurable.mk f hf x<GOAL>Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (𝓝 (f x))
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))<VAR>h'x : f x = AEMeasurable.mk f hf x<VAR>a : Set α<GOAL>∫⁻ (y : α) in a, f y ∂μ = ∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>f : α → ℝ≥0∞<VAR>hf : AEMeasurable f μ<VAR>h'f : ∫⁻ (y : α), f y ∂μ ≠ ⊤<VAR>A : ∫⁻ (y : α), AEMeasurable.mk f hf y ∂μ ≠ ⊤<VAR>x : α<VAR>hx : Tendsto (fun a => (∫⁻ (y : α) in a, AEMeasurable.mk f hf y ∂μ) / μ a) (v.filterAt x) (𝓝 (AEMeasurable.mk f hf x))<VAR>h'x : f x = AEMeasurable.mk f hf x<VAR>a : Set α<GOAL>f =ᶠ[ae (μ.restrict a)] AEMeasurable.mk f hf
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>a : Over P<GOAL>Quot.mk (PseudoEqual P) a = 0 ↔ a.hom = 0
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Abelian C<VAR>P : C<VAR>a : Over P<GOAL>Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0
<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>a b c✝ d x✝ y z : P<VAR>r R : ℝ<VAR>c x : P<GOAL>inversion c (dist c x) x = x
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.595057<VAR>S' : Type ?u.595060<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.597491<VAR>S'' : Type ?u.597494<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>p : P.Ring<VAR>hp : p ∈ P.ker<VAR>m : P.ker.Cotangent<GOAL>p • m = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝²⁵ : CommRing R<VAR>inst✝²⁴ : CommRing S<VAR>inst✝²³ : Algebra R S<VAR>P : Generators R S<VAR>R' : Type ?u.595057<VAR>S' : Type ?u.595060<VAR>inst✝²² : CommRing R'<VAR>inst✝²¹ : CommRing S'<VAR>inst✝²⁰ : Algebra R' S'<VAR>P' : Generators R' S'<VAR>inst✝¹⁹ : Algebra R R'<VAR>inst✝¹⁸ : Algebra S S'<VAR>inst✝¹⁷ : Algebra R S'<VAR>inst✝¹⁶ : IsScalarTower R R' S'<VAR>inst✝¹⁵ : IsScalarTower R S S'<VAR>R'' : Type ?u.597491<VAR>S'' : Type ?u.597494<VAR>inst✝¹⁴ : CommRing R''<VAR>inst✝¹³ : CommRing S''<VAR>inst✝¹² : Algebra R'' S''<VAR>P'' : Generators R'' S''<VAR>inst✝¹¹ : Algebra R R''<VAR>inst✝¹⁰ : Algebra S S''<VAR>inst✝⁹ : Algebra R S''<VAR>inst✝⁸ : IsScalarTower R R'' S''<VAR>inst✝⁷ : IsScalarTower R S S''<VAR>inst✝⁶ : Algebra R' R''<VAR>inst✝⁵ : Algebra S' S''<VAR>inst✝⁴ : Algebra R' S''<VAR>inst✝³ : IsScalarTower R' R'' S''<VAR>inst✝² : IsScalarTower R' S' S''<VAR>inst✝¹ : IsScalarTower R R' R''<VAR>inst✝ : IsScalarTower S S' S''<VAR>p : P.Ring<VAR>hp : p ∈ P.ker<VAR>x : ↥P.ker<GOAL>p • P.ker.toCotangent x = 0