ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<VAR>y1 : ℝ<VAR>hy1 : y1 ∈ Ico 0 (2 * π)<VAR>hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1<VAR>hy2 : y1 ∈ [[0, 2 * π]]<VAR>HX2 : ∀ (x : ℂ), abs (x - z) = R → abs (f x) ≤ abs (f X)<GOAL>‖circleTransformDeriv R z v f y‖ ≤ abs (V b a) * abs (f X)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<VAR>y1 : ℝ<VAR>hy1 : y1 ∈ Ico 0 (2 * π)<VAR>hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1<VAR>hy2 : y1 ∈ [[0, 2 * π]]<VAR>HX2 : ∀ (x : ℂ), abs (x - z) = R → abs (f x) ≤ abs (f X)<VAR>this : abs (circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩) * abs (f (circleMap z R y1)) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩) * abs (f X)<GOAL>‖circleTransformDeriv R z v f y‖ ≤ abs (V b a) * abs (f X)
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>R✝ : ℝ<VAR>z✝ w : ℂ<VAR>R : ℝ<VAR>hR : 0 < R<VAR>z x : ℂ<VAR>f : ℂ → ℂ<VAR>hx : x ∈ ball z R<VAR>hf : ContinuousOn f (sphere z R)<VAR>r : ℝ<VAR>hr : r < R<VAR>hrx : x ∈ ball z r<VAR>ε' : ℝ<VAR>hε' : ε' > 0<VAR>H : ball x ε' ⊆ ball z r<VAR>a : ℂ<VAR>b : ℝ<VAR>ha : (a, b).1 ∈ closedBall z r<VAR>hb : (a, b).2 ∈ [[0, 2 * π]]<VAR>hab : ∀ (y : ↑(closedBall z r ×ˢ [[0, 2 * π]])), abs (circleTransformBoundingFunction R z ↑y) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩)<VAR>V : ℝ → ℂ → ℂ := fun θ w => circleTransformDeriv R z w (fun x => 1) θ<VAR>X : ℂ<VAR>y : ℝ<VAR>v : ℂ<VAR>hv : v ∈ ball x ε'<VAR>y1 : ℝ<VAR>hy1 : y1 ∈ Ico 0 (2 * π)<VAR>hfun : circleTransformDeriv R z v f y = circleTransformDeriv R z v f y1<VAR>hy2 : y1 ∈ [[0, 2 * π]]<VAR>HX2 : ∀ (x : ℂ), abs (x - z) = R → abs (f x) ≤ abs (f X)<VAR>this : abs (circleTransformBoundingFunction R z ↑⟨(v, y1), ⋯⟩) * abs (f (circleMap z R y1)) ≤ abs (circleTransformBoundingFunction R z ↑⟨(a, b), ⋯⟩) * abs (f X)<GOAL>‖circleTransformDeriv R z v f y1‖ ≤ abs (V b a) * abs (f X)
<VAR>z : ℂ<VAR>x✝ : ∃ r, z = ↑r<VAR>h : ℝ<VAR>e : z = ↑h<GOAL>(starRingEnd ℂ) z = z
<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>hl : l.HasBasis p s<VAR>s' t : Set α<GOAL>t ∈ l ⊓ 𝓟 s' ↔ ∃ i, p i ∧ s i ∩ s' ⊆ t
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i✝ i : ι<VAR>hi : i ∈ ↑(indicator s f).support<GOAL>i ∈ ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i✝ i : ι<VAR>hi : (indicator s f) i ≠ 0<GOAL>i ∈ ↑s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝ : Zero α<VAR>s : Finset ι<VAR>f : (i : ι) → i ∈ s → α<VAR>i✝ i : ι<VAR>hi : (indicator s f) i ≠ 0<VAR>h : i ∉ ↑s<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>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>f : R →+* S<GOAL>(Polynomial.map f P).natDegree = P.natDegree
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>f : R →+* S<GOAL>(Polynomial.map f P).coeff P.natDegree ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝² : Semiring R<VAR>inst✝¹ : Semiring S<VAR>inst✝ : Nontrivial S<VAR>P : R[X]<VAR>hmo : P.Monic<VAR>f : R →+* S<GOAL>1 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s✝ s' : Finset α<VAR>t✝ t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝ : DecidableEq (α × β)<VAR>s : Finset α<VAR>t : Finset β<VAR>x✝ : α × β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ t ↔ (x, y) ∈ s.biUnion fun a => image (fun b => (a, b)) t
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X) = 𝟭 ((i : I) → ↑(π.obj (X i)))
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>∀ (X_1 : (i : I) → ↑(π.obj (X i))), (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).obj X_1 = (𝟭 ((i : I) → ↑(π.obj (X i)))).obj X_1
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>∀ (X_1 Y : (i : I) → ↑(π.obj (X i))) (f : X_1 ⟶ Y), (piToPiTop X ⋙ CategoryTheory.Functor.pi' (proj X)).map f = CategoryTheory.eqToHom ⋯ ≫ (𝟭 ((i : I) → ↑(π.obj (X i)))).map f ≫ CategoryTheory.eqToHom ⋯
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>autoParam (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y), (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f = CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯) _auto✝
<VAR>I : Type u<VAR>X : I → TopCat<GOAL>∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))), (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<GOAL>(p * X).comp r = p.comp r * r
<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>hp : p ≠ 0<GOAL>p.degree < (p * X).degree
<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>hp : p ≠ 0<VAR>this : Nontrivial R<GOAL>p.degree < (p * X).degree
<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>hp : p ≠ 0<VAR>this✝ : Nontrivial R<VAR>this : p.leadingCoeff * X.leadingCoeff ≠ 0<GOAL>p.degree < (p * X).degree
<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>hp : p ≠ 0<VAR>this✝ : Nontrivial R<VAR>this : p.leadingCoeff * X.leadingCoeff ≠ 0<GOAL>↑p.natDegree < ↑p.natDegree + 1
<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>hf : AEMeasurable f μ<VAR>g : X → E<VAR>f' : X → ℝ≥0 := AEMeasurable.mk f hf<GOAL>(∫ (x : X), g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X), f x • g x ∂μ
<VAR>α : Type u_1<VAR>inst✝ : Semiring α<VAR>m n : Num<GOAL>↑(m + n) = ↑m + ↑n
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³² : CommRing A<VAR>inst✝³¹ : CommRing B<VAR>inst✝³⁰ : Algebra A B<VAR>inst✝²⁹ : Field K<VAR>inst✝²⁸ : Field L<VAR>inst✝²⁷ : Algebra A K<VAR>inst✝²⁶ : IsFractionRing A K<VAR>inst✝²⁵ : Algebra B L<VAR>inst✝²⁴ : Algebra K L<VAR>inst✝²³ : Algebra A L<VAR>inst✝²² : IsScalarTower A B L<VAR>inst✝²¹ : IsScalarTower A K L<VAR>inst✝²⁰ : IsIntegralClosure B A L<VAR>inst✝¹⁹ : FiniteDimensional K L<VAR>Aₘ : Type ?u.571927<VAR>Bₘ : Type ?u.571930<VAR>inst✝¹⁸ : CommRing Aₘ<VAR>inst✝¹⁷ : CommRing Bₘ<VAR>inst✝¹⁶ : Algebra Aₘ Bₘ<VAR>inst✝¹⁵ : Algebra A Aₘ<VAR>inst✝¹⁴ : Algebra B Bₘ<VAR>inst✝¹³ : Algebra A Bₘ<VAR>inst✝¹² : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹¹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁰ : IsLocalization M Aₘ<VAR>inst✝⁹ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁸ : IsIntegrallyClosed A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsIntegrallyClosed A<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : IsIntegrallyClosed B<VAR>inst✝³ : Module.Finite A B<VAR>inst✝² : NoZeroSMulDivisors A B<VAR>inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this : IsIntegralClosure B A (FractionRing B)<GOAL>(intNorm A B) x = (norm A) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³² : CommRing A<VAR>inst✝³¹ : CommRing B<VAR>inst✝³⁰ : Algebra A B<VAR>inst✝²⁹ : Field K<VAR>inst✝²⁸ : Field L<VAR>inst✝²⁷ : Algebra A K<VAR>inst✝²⁶ : IsFractionRing A K<VAR>inst✝²⁵ : Algebra B L<VAR>inst✝²⁴ : Algebra K L<VAR>inst✝²³ : Algebra A L<VAR>inst✝²² : IsScalarTower A B L<VAR>inst✝²¹ : IsScalarTower A K L<VAR>inst✝²⁰ : IsIntegralClosure B A L<VAR>inst✝¹⁹ : FiniteDimensional K L<VAR>Aₘ : Type ?u.571927<VAR>Bₘ : Type ?u.571930<VAR>inst✝¹⁸ : CommRing Aₘ<VAR>inst✝¹⁷ : CommRing Bₘ<VAR>inst✝¹⁶ : Algebra Aₘ Bₘ<VAR>inst✝¹⁵ : Algebra A Aₘ<VAR>inst✝¹⁴ : Algebra B Bₘ<VAR>inst✝¹³ : Algebra A Bₘ<VAR>inst✝¹² : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹¹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁰ : IsLocalization M Aₘ<VAR>inst✝⁹ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁸ : IsIntegrallyClosed A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsIntegrallyClosed A<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : IsIntegrallyClosed B<VAR>inst✝³ : Module.Finite A B<VAR>inst✝² : NoZeroSMulDivisors A B<VAR>inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(intNorm A B) x = (norm A) x
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>B : Type u_4<VAR>inst✝³² : CommRing A<VAR>inst✝³¹ : CommRing B<VAR>inst✝³⁰ : Algebra A B<VAR>inst✝²⁹ : Field K<VAR>inst✝²⁸ : Field L<VAR>inst✝²⁷ : Algebra A K<VAR>inst✝²⁶ : IsFractionRing A K<VAR>inst✝²⁵ : Algebra B L<VAR>inst✝²⁴ : Algebra K L<VAR>inst✝²³ : Algebra A L<VAR>inst✝²² : IsScalarTower A B L<VAR>inst✝²¹ : IsScalarTower A K L<VAR>inst✝²⁰ : IsIntegralClosure B A L<VAR>inst✝¹⁹ : FiniteDimensional K L<VAR>Aₘ : Type ?u.571927<VAR>Bₘ : Type ?u.571930<VAR>inst✝¹⁸ : CommRing Aₘ<VAR>inst✝¹⁷ : CommRing Bₘ<VAR>inst✝¹⁶ : Algebra Aₘ Bₘ<VAR>inst✝¹⁵ : Algebra A Aₘ<VAR>inst✝¹⁴ : Algebra B Bₘ<VAR>inst✝¹³ : Algebra A Bₘ<VAR>inst✝¹² : IsScalarTower A Aₘ Bₘ<VAR>inst✝¹¹ : IsScalarTower A B Bₘ<VAR>M : Submonoid A<VAR>inst✝¹⁰ : IsLocalization M Aₘ<VAR>inst✝⁹ : IsLocalization (algebraMapSubmonoid B M) Bₘ<VAR>inst✝⁸ : IsIntegrallyClosed A<VAR>inst✝⁷ : IsDomain A<VAR>inst✝⁶ : IsIntegrallyClosed A<VAR>inst✝⁵ : IsDomain B<VAR>inst✝⁴ : IsIntegrallyClosed B<VAR>inst✝³ : Module.Finite A B<VAR>inst✝² : NoZeroSMulDivisors A B<VAR>inst✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)<VAR>inst✝ : Module.Free A B<VAR>x : B<VAR>this✝ : IsIntegralClosure B A (FractionRing B)<VAR>this : IsLocalization (algebraMapSubmonoid B A⁰) (FractionRing B)<GOAL>(algebraMap A (FractionRing A)) ((intNorm A B) x) = (algebraMap A (FractionRing A)) ((norm A) x)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : Submodule.comap f U ⟂ Submodule.comap f V<GOAL>U ⟂ V
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace 𝕜 F<VAR>f : E ≃ₗᵢ[𝕜] F<VAR>U V : Submodule 𝕜 F<VAR>h : Submodule.comap f U ⟂ Submodule.comap f V<VAR>hf : ∀ (p : Submodule 𝕜 F), Submodule.map f.toLinearIsometry (Submodule.comap f p) = p<GOAL>U ⟂ V
<VAR>a b c x : ℕ<GOAL>x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α✝<VAR>α : Type u_4<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y<GOAL>x ≤ y
<VAR>ι : Sort u_1<VAR>α✝ : Type u_2<VAR>β : Type u_3<VAR>inst✝² : PartialOrder α✝<VAR>α : Type u_4<VAR>inst✝¹ : BooleanAlgebra α<VAR>inst✝ : IsAtomic α<VAR>x y : α<VAR>h : ∀ (a : α), IsAtom a → a ≤ x → a ≤ y<VAR>this : x ⊓ yᶜ = ⊥<GOAL>x ≤ y
<VAR>n : ℕ<VAR>α : Type u_1<VAR>a : α<VAR>v : Vector α n<GOAL>(a ::ᵥ v).get 0 = a
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) const<GOAL>toLoop i (fromLoop i p) = p
<VAR>N : Type u_1<VAR>X : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>x : X<VAR>inst✝ : DecidableEq N<VAR>i : N<VAR>p : Ω (↑(Ω^ { j // j ≠ i } X x)) const<GOAL>{ toFun := fun t => ⟨({ toFun := Subtype.val, continuous_toFun := ⋯ }.comp p.toContinuousMap).uncurry.curry t, ⋯⟩, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ } = p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝¹ : SupSet α<VAR>inst✝ : SupSet β<VAR>f : ι → α × β<GOAL>(iSup f).swap = ⨆ i, (f i).swap
<VAR>F : Type u_1<VAR>inst✝¹ : Field F<VAR>ι : Type u_2<VAR>inst✝ : DecidableEq ι<VAR>s t : Finset ι<VAR>i j : ι<VAR>v r r' : ι → F<VAR>hvs : Set.InjOn v ↑s<VAR>hrr' : (interpolate s v) r = (interpolate s v) r'<VAR>x✝ : ι<VAR>hi : x✝ ∈ s<GOAL>r x✝ = r' x✝
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<GOAL>Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet s
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<GOAL>Disjoint G (fromEdgeSet s) ↔ Disjoint G.edgeSet (s \ {e | e.IsDiag} ∪ s ∩ {e | e.IsDiag})
<VAR>ι : Sort u_1<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>a b c u v w : V<VAR>e : Sym2 V<VAR>s : Set (Sym2 V)<GOAL>Disjoint G.edgeSet (s ∩ {e | e.IsDiag})
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>l : Filter α<VAR>f g : α → 𝕜<VAR>C : 𝕜<VAR>hC : 0 < C<VAR>hf : Tendsto f l (𝓝 C)<VAR>hg : Tendsto g l atBot<GOAL>Tendsto (fun x => f x * g x) l atBot
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>comap f (map f H) = H ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<GOAL>comap f (map f H) ≤ H ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<VAR>x : G<VAR>hx : x ∈ comap f (map f H)<GOAL>x ∈ H ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<VAR>x : G<VAR>hx : ∃ x_1 ∈ H, f x_1 = f x<GOAL>x ∈ H ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<VAR>x y : G<VAR>hy : y ∈ H<VAR>hy' : f y = f x<GOAL>x ∈ H ⊔ f.ker
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f : G →* N<VAR>H : Subgroup G<VAR>x y : G<VAR>hy : y ∈ H<VAR>hy' : f y = f x<GOAL>y * (y⁻¹ * x) ∈ H ⊔ f.ker
<VAR>R : Type u<VAR>S : Type v<VAR>K : Type w<VAR>inst✝ : CommRing R<VAR>f g : R[X]<GOAL>f ∣ g - 0 ↔ f ∣ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x a b : α<VAR>l : List α<GOAL>(a :: b :: l).reverse.formPerm = (a :: b :: l).formPerm⁻¹
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>↑(nndist ((starRingEnd ℂ) z) z) = ↑(2 * Real.nnabs z.im)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(s ⊻ t).truncatedInf a = s.truncatedInf a ⊔ t.truncatedInf a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>((filter (fun x => x ≤ a) s ⊻ filter (fun x => x ≤ a) t).inf' ⋯ fun x => id x) = (filter (fun x => x ≤ a) s ×ˢ filter (fun x => x ≤ a) t).inf' ⋯ fun i => id i.1 ⊔ id i.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>((image (Function.uncurry fun x x_1 => x ⊔ x_1) (filter (fun x => x ≤ a) s ×ˢ filter (fun x => x ≤ a) t)).inf' ⋯ fun x => id x) = (filter (fun x => x ≤ a) s ×ˢ filter (fun x => x ≤ a) t).inf' ⋯ fun i => id i.1 ⊔ id i.2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : DistribLattice α<VAR>inst✝² : BoundedOrder α<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableRel fun x x_1 => x ≤ x_1<VAR>s t : Finset α<VAR>a : α<VAR>hs : a ∈ upperClosure ↑s<VAR>ht : a ∈ upperClosure ↑t<GOAL>(filter (fun x => x ≤ a) s ×ˢ filter (fun x => x ≤ a) t).inf' ⋯ ((fun x => id x) ∘ Function.uncurry fun x x_1 => x ⊔ x_1) = (filter (fun x => x ≤ a) s ×ˢ filter (fun x => x ≤ a) t).inf' ⋯ fun i => id i.1 ⊔ id i.2
<VAR>p : ℕ<GOAL>(Summable fun n => (↑n ^ p)⁻¹) ↔ 1 < p
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<GOAL>a ∈ Icc a b ↔ a ≤ b
<VAR>a b m n✝ p✝ n p : ℕ<VAR>pp : Prime p<VAR>hn : n ≠ 0<GOAL>multiplicity p n = ↑(n.factorization p)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<GOAL>⊥.smallSets = pure ∅
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Sort u_3<VAR>l l' la : Filter α<VAR>lb : Filter β<GOAL>Monotone powerset
<VAR>R : Type u_1<VAR>inst✝³ : Semiring R<VAR>r : R<VAR>p : R[X]<VAR>S : Type u_2<VAR>inst✝² : AddCommMonoid S<VAR>inst✝¹ : Pow S ℕ<VAR>inst✝ : MulActionWithZero R S<VAR>x : S<GOAL>(C r).smeval x = r • x ^ 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹³ : TopologicalSpace α✝<VAR>inst✝¹² : MeasurableSpace α✝<VAR>inst✝¹¹ : BorelSpace α✝<VAR>inst✝¹⁰ : TopologicalSpace β✝<VAR>inst✝⁹ : MeasurableSpace β✝<VAR>inst✝⁸ : BorelSpace β✝<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : TopologicalSpace β<VAR>hβ : BorelSpace β<VAR>e : α → β<VAR>h'e : MeasurableEmbedding e<VAR>h''e : Inducing e<GOAL>inst✝³ = borel α
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>γ₂ : Type u_4<VAR>δ : Type u_5<VAR>ι : Sort y<VAR>s t u : Set α✝<VAR>inst✝¹³ : TopologicalSpace α✝<VAR>inst✝¹² : MeasurableSpace α✝<VAR>inst✝¹¹ : BorelSpace α✝<VAR>inst✝¹⁰ : TopologicalSpace β✝<VAR>inst✝⁹ : MeasurableSpace β✝<VAR>inst✝⁸ : BorelSpace β✝<VAR>inst✝⁷ : TopologicalSpace γ<VAR>inst✝⁶ : MeasurableSpace γ<VAR>inst✝⁵ : BorelSpace γ<VAR>inst✝⁴ : MeasurableSpace δ<VAR>α : Type u_6<VAR>β : Type u_7<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : TopologicalSpace β<VAR>hβ : BorelSpace β<VAR>e : α → β<VAR>h'e : MeasurableEmbedding e<VAR>h''e : Inducing e<VAR>this : MeasurableSpace.comap e (borel β) = inst✝³<GOAL>inst✝³ = borel α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>this✝ : Fintype α<VAR>this : Fintype β<GOAL>Nat.card (α ⊕ β) = Nat.card α + Nat.card β
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.length < c.boundaries.card
<VAR>n : ℕ<VAR>c : CompositionAsSet n<GOAL>c.length < c.length + 1
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>f : R<VAR>s : ↥x.asIdeal.primeCompl<GOAL>(toStalk R x) f = (toStalk R x) ↑s * ((structureSheaf R).presheaf.germ ⟨x, ⋯⟩) (const R f (↑s) (PrimeSpectrum.basicOpen ↑s) ⋯)
<VAR>G : Type u<VAR>inst✝ : Group G<GOAL>commutator G = Subgroup.normalClosure (commutatorSet G)
<VAR>q : ℚ<GOAL>q * ↑q.den = ↑q.num
<VAR>q : ℚ<GOAL>q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
<VAR>q : ℚ<VAR>this : ↑q.den ≠ 0<GOAL>q.num /. ↑q.den * (↑q.den /. 1) = q.num /. 1
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<GOAL>(adjoin R s).toSubmodule = span R ↑(Subsemigroup.closure s)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<GOAL>(adjoin R s).toSubmodule ≤ span R ↑(Subsemigroup.closure s)
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>s : Set A<GOAL>span R ↑(Subsemigroup.closure s) ≤ (adjoin R s).toSubmodule
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<GOAL>G.minDegree ≤ G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).min = ↑t<GOAL>G.minDegree ≤ G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>inst✝¹ : Fintype V<VAR>inst✝ : DecidableRel G.Adj<VAR>v : V<VAR>t : ℕ<VAR>ht : (image (fun v => G.degree v) univ).min = ↑t<VAR>this : t ≤ G.degree v<GOAL>G.minDegree ≤ G.degree v
<VAR>a✝ b✝ m n p✝ a b p : ℕ<VAR>ha : a ≠ 0<VAR>hb : b ≠ 0<GOAL>p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>s : SignedMeasure α<VAR>i✝ j : Set α<VAR>hs : VectorMeasure.restrict 0 univ ≤ VectorMeasure.restrict s univ<VAR>i : Set α<VAR>hi : MeasurableSet i<GOAL>↑(s.toMeasureOfZeroLE univ ⋯ hs).toSignedMeasure i = ↑s i