ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<VAR>u_meas : ∀ (n : ℕ), MeasurableSet (u n)<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : FiniteDimensional ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → E<VAR>f' : E → E →L[ℝ] E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>hs : MeasurableSet s<VAR>hf' : ∀ x ∈ s, HasFDerivWithinAt f (f' x) s x<VAR>u : ℕ → Set E := fun n => disjointed (spanningSets μ) n<VAR>u_meas : ∀ (n : ℕ), MeasurableSet (u n)<VAR>A : s = ⋃ n, s ∩ u n<GOAL>μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>h : 0 < a<VAR>b : Ordinal.{u_4}<GOAL>a * b < a * succ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>a : Ordinal.{u_4}<VAR>h : 0 < a<VAR>b : Ordinal.{u_4}<GOAL>a * b < a * b + a
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>H : SimpleGraph V<VAR>hr : 0 < r<VAR>hn : r ≤ Fintype.card V<VAR>hG : G.IsTuranMaximal r<VAR>h : G.CliqueFree r<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>H : SimpleGraph V<VAR>K : Finset V<VAR>left✝ : K ⊆ univ<VAR>hr : 0 < K.card<VAR>hn : K.card ≤ Fintype.card V<VAR>hG : G.IsTuranMaximal K.card<VAR>h : G.CliqueFree K.card<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n : ℕ<VAR>H : SimpleGraph V<VAR>K : Finset V<VAR>left✝ : K ⊆ univ<VAR>hr : 0 < K.card<VAR>hn : K.card ≤ Fintype.card V<VAR>hG : G.IsTuranMaximal K.card<VAR>h : G.CliqueFree K.card<VAR>a b : V<VAR>hab : a ≠ b<VAR>hGab : ¬G.Adj a b<GOAL>False
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>0 ≤ normSq a
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedCommRing R<VAR>a : ℍ[R]<GOAL>0 ≤ a.re ^ 2 + a.imI ^ 2 + a.imJ ^ 2 + a.imK ^ 2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<GOAL>⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : a ≤ 0<GOAL>⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<GOAL>⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>ha : 0 ≤ a<GOAL>⌊a / ↑0⌋₊ = ⌊a⌋₊ / 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>⌊a / ↑n⌋₊ = ⌊a⌋₊ / n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>0 ≤ a / ↑n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>↑(⌊a⌋₊ / n) ≤ a / ↑n ∧ a / ↑n < ↑(⌊a⌋₊ / n) + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>a / ↑n < ↑(⌊a⌋₊ / n) + 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>⌊a⌋₊ < ⌊a⌋₊ / n * n + n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>inst✝ : FloorSemiring α<VAR>a : α<VAR>n : ℕ<VAR>ha : 0 ≤ a<VAR>hn : n > 0<GOAL>0 < ↑n
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : AnalyticAt 𝕜 f x<VAR>n : ℕ∞<GOAL>ContDiffAt 𝕜 n f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>F : Type v<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace 𝕜 F<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>r : ℝ≥0∞<VAR>f : E → F<VAR>x : E<VAR>s✝ : Set E<VAR>inst✝ : CompleteSpace F<VAR>h : AnalyticAt 𝕜 f x<VAR>n : ℕ∞<VAR>s : Set E<VAR>hs : s ∈ nhds x<VAR>hf : AnalyticOn 𝕜 f s<GOAL>ContDiffAt 𝕜 n f x
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike G N M<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : MonoidHomClass G N M<VAR>f : F<VAR>x : M<VAR>g : G<VAR>hfg : LeftInverse ⇑g ⇑f<VAR>h : IsUnit (f x)<GOAL>IsUnit x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>P : Type u_5<VAR>G : Type u_6<VAR>H : Type u_7<VAR>F : Type u_8<VAR>inst✝² : Mul M<VAR>inst✝¹ : CommSemigroup N<VAR>inst✝ : CommSemigroup P<VAR>g : N →ₙ* P<VAR>f₁ f₂ : M →ₙ* N<VAR>x✝ : M<GOAL>(g.comp (f₁ * f₂)) x✝ = (g.comp f₁ * g.comp f₂) x✝
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsBezout R<VAR>inst✝ : GCDMonoid R<VAR>x y : R<GOAL>Ideal.span {GCDMonoid.gcd x y} = Ideal.span {gcd x y}
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : IsBezout R<VAR>inst✝ : GCDMonoid R<VAR>x y : R<GOAL>Associated (GCDMonoid.gcd x y) (gcd x y)
<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>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ map ϕ.toMonoidHom H
<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>H K : Subgroup G<GOAL>H.Characteristic ↔ ∀ (ϕ : G ≃* G), H ≤ comap ϕ.symm.toMonoidHom H
<VAR>C : Type u<VAR>inst✝⁶ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝⁵ : Category.{u_4, u_1} A<VAR>inst✝⁴ : Category.{u_3, u_2} B<VAR>F : A ⥤ B<VAR>inst✝³ : HasWeakSheafify J A<VAR>inst✝² : HasWeakSheafify J B<VAR>inst✝¹ : J.HasSheafCompose F<VAR>inst✝ : J.PreservesSheafification F<VAR>P : Cᵒᵖ ⥤ A<GOAL>whiskerRight (toSheafify J P) F ≫ (sheafifyComposeIso J F P).inv = toSheafify J (P ⋙ F)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Mul α<VAR>inst✝¹ : IsLeftCancelMul α<VAR>inst✝ : DecidableEq α<VAR>s✝ t✝ : Finset α<VAR>a : α<VAR>s : Set α<VAR>t : Finset α<GOAL>(s.PairwiseDisjoint fun x => x • t) ↔ Set.InjOn (fun p => p.1 * p.2) (s ×ˢ ↑t)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>I ∈ (toPrincipalIdeal R K).range ↔ ∃ x, spanSingleton R⁰ x = ↑I
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : Field K<VAR>inst✝⁷ : Field L<VAR>inst✝⁶ : DecidableEq L<VAR>inst✝⁵ : Algebra R K<VAR>inst✝⁴ : IsFractionRing R K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : FiniteDimensional K L<VAR>inst✝¹ : Algebra R L<VAR>inst✝ : IsScalarTower R K L<VAR>I : (FractionalIdeal R⁰ K)ˣ<GOAL>(∃ x, spanSingleton R⁰ ↑x = ↑I) ↔ ∃ x, spanSingleton R⁰ x = ↑I
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>p₁ p₂ p₃ p₄ : P<GOAL>edist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ edist p₁ p₃ + edist p₂ p₄
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>p₁ p₂ p₃ p₄ : P<GOAL>↑(nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄)) ≤ ↑(nndist p₁ p₃) + ↑(nndist p₂ p₄)
<VAR>α : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>W : Type u_4<VAR>Q : Type u_5<VAR>inst✝⁵ : SeminormedAddCommGroup V<VAR>inst✝⁴ : PseudoMetricSpace P<VAR>inst✝³ : NormedAddTorsor V P<VAR>inst✝² : NormedAddCommGroup W<VAR>inst✝¹ : MetricSpace Q<VAR>inst✝ : NormedAddTorsor W Q<VAR>p₁ p₂ p₃ p₄ : P<GOAL>nndist (p₁ -ᵥ p₂) (p₃ -ᵥ p₄) ≤ nndist p₁ p₃ + nndist p₂ p₄
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : Preorder α<VAR>a✝ b c : α<VAR>inst✝ : NoMaxOrder α<VAR>a : α<GOAL>⋃ b, Ioo a b = Ioi a
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<GOAL>count K v I⁻¹ = -count K v I
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<GOAL>m.IsCaratheodory (s₁ ∩ s₂)
<VAR>α : Type u<VAR>m : OuterMeasure α<VAR>s s₁ s₂ : Set α<VAR>h₁ : m.IsCaratheodory s₁<VAR>h₂ : m.IsCaratheodory s₂<GOAL>m.IsCaratheodory (s₁ᶜ ∪ s₂ᶜ)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>s t : Cofork f g<VAR>i : s.pt ≅ t.pt<VAR>w : autoParam (s.π ≫ i.hom = t.π) _auto✝<GOAL>t.π ≫ i.inv = s.π
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.80688, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<GOAL>s.s ≫ s.r = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.80688, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>this : Epi S.g<GOAL>s.s ≫ s.r = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x : List α<VAR>f : α → β<VAR>l : Language α<GOAL>(map f) l∗ = ((map f) l)∗
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x : List α<VAR>f : α → β<VAR>l : Language α<GOAL>(map f) (⨆ i, l ^ i) = ⨆ i, (map f) l ^ i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>l✝ m : Language α<VAR>a b x : List α<VAR>f : α → β<VAR>l : Language α<GOAL>(map f) (⨆ i, l ^ i) = ⨆ i, (map f) (l ^ i)
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : NormalizationMonoid α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>M : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero M<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : Unique Mˣ<VAR>x : M<GOAL>factors x = Multiset.map (⇑normalize) (factors x)
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : NormalizationMonoid α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>M : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero M<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : Unique Mˣ<VAR>x x✝ : M<VAR>a✝ : x✝ ∈ factors x<GOAL>⇑normalize = id
<VAR>α : Type u_1<VAR>inst✝⁵ : CancelCommMonoidWithZero α<VAR>inst✝⁴ : NormalizationMonoid α<VAR>inst✝³ : UniqueFactorizationMonoid α<VAR>M : Type u_2<VAR>inst✝² : CancelCommMonoidWithZero M<VAR>inst✝¹ : UniqueFactorizationMonoid M<VAR>inst✝ : Unique Mˣ<VAR>x x✝ : M<VAR>a✝ : x✝ ∈ factors x<VAR>p : M<GOAL>normalize p = id p
<VAR>k G✝ : Type u<VAR>inst✝² : CommRing k<VAR>inst✝¹ : Monoid G✝<VAR>G : Type u<VAR>inst✝ : Group G<VAR>A : Rep k G<VAR>g : G<VAR>x : CoeSort.coe A<GOAL>(A.ρ g * A.ρ g⁻¹) x = x
<VAR>X : Type u_1<VAR>Y✝ : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y✝<VAR>inst✝³ : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝² : TopologicalSpace X'<VAR>inst✝¹ : TopologicalSpace Y'<VAR>ι : Type u_6<VAR>ι' : Type u_7<VAR>Y : ι' → Type u_8<VAR>inst✝ : (j : ι') → TopologicalSpace (Y j)<VAR>e : ι ≃ ι'<VAR>i : ι<GOAL>Continuous fun a => (Equiv.piCongrLeft Y e).toFun a (e i)
<VAR>a b c : ℕ<VAR>hac : a ≤ c<VAR>x : ℕ<GOAL>x ∈ image (fun x => c - x) (Ico a b) ↔ x ∈ Ico (c + 1 - b) (c + 1 - a)
<VAR>a b c : ℕ<VAR>hac : a ≤ c<VAR>x : ℕ<GOAL>(∃ a_1, (a ≤ a_1 ∧ a_1 < b) ∧ c - a_1 = x) ↔ c + 1 - b ≤ x ∧ x < c + 1 - a
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : ℵ₀ ≤ b<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : b < ℵ₀<GOAL>a * b = max a b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : b < ℵ₀<GOAL>max a b ≤ a * b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : b < ℵ₀<VAR>this : b ≤ a<GOAL>max a b ≤ a * b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : b < ℵ₀<VAR>this : b ≤ a<GOAL>a ≤ a * b
<VAR>a b : Cardinal.{u_1}<VAR>h : ℵ₀ ≤ a<VAR>h' : b ≠ 0<VAR>hb : b < ℵ₀<VAR>this : b ≤ a<GOAL>a = a * 1
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>lv : All (fun x => cmpLT cmp x v) l<VAR>vr : All (fun x => cmpLT cmp v x) r<VAR>hl : Ordered cmp l<VAR>hr : Ordered cmp r<GOAL>Ordered cmp (l.balance2 v r)
<VAR>α : Type u_1<VAR>cmp : α → α → Ordering<VAR>l : RBNode α<VAR>v : α<VAR>r : RBNode α<VAR>lv : All (fun x => cmpLT cmp x v) l<VAR>vr : All (fun x => cmpLT cmp v x) r<VAR>hl : Ordered cmp l<VAR>hr : Ordered cmp r<GOAL>Ordered cmp (r.reverse.balance1 v l.reverse).reverse
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ (x : E), (p x 0).uncurry0 = f x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x✝ x : α<GOAL>x ∈ [[a, c]] → x ∈ [[a, b]] ∪ [[b, c]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>s : Set α<VAR>a a₁ a₂ b b₁ b₂ c d x✝ x : α<GOAL>a ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ a → (a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a) ∨ b ≤ x ∧ x ≤ c ∨ c ≤ x ∧ x ≤ b
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hi : I.IsLocal<VAR>x : R<VAR>h : I ⊔ span {x} = ⊤<VAR>p : R<VAR>hpi : p ∈ I<VAR>q : R<VAR>hq : q ∈ span {x}<VAR>hpq : p + q = 1<VAR>r : R<VAR>hr : q = x * r<GOAL>r * x - 1 ∈ I
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝ : CommRing R<VAR>I : Ideal R<VAR>hi : I.IsLocal<VAR>x : R<VAR>h : I ⊔ span {x} = ⊤<VAR>p : R<VAR>hpi : p ∈ I<VAR>q : R<VAR>hq : q ∈ span {x}<VAR>hpq : p + q = 1<VAR>r : R<VAR>hr : q = x * r<GOAL>-p ∈ I
<VAR>x✝ y✝ x y : ℝ<VAR>hy : 0 ≤ y<GOAL>√(x * y) = √x * √y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>hy : y ⊆ f '' x<GOAL>x ∩ f ⁻¹' maximals s y = maximals r (x ∩ f ⁻¹' y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>y : Set β<VAR>x : Set α<VAR>hf : ∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))<VAR>hy : y ⊆ f '' x<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a' a ↔ s (f a') (f a))
<VAR>x : USize<GOAL>x.toNat < 2 ^ System.Platform.numBits
<VAR>α : Type u<GOAL>induced pure Ultrafilter.topologicalSpace = ⊥
<VAR>α : Type u<GOAL>∀ (x : α), IsOpen {x}
<VAR>α : Type u<VAR>x : α<GOAL>IsOpen {x}
<VAR>α : Type u<VAR>x : α<GOAL>pure ⁻¹' {u | {x} ∈ u} = {x}
<VAR>a x z✝ z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Tendsto arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)
<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (coconeMorphism F j) x
<VAR>J : Type u<VAR>inst✝ : Category.{v, u} J<VAR>F : J ⥤ AddCommGrp<VAR>j j' : J<VAR>f : j ⟶ j'<VAR>x : ↑(F.obj j)<GOAL>(coconeMorphism F j') ((F.map f) x) = (F.map f ≫ coconeMorphism F j') x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x y : F<VAR>h : ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖<GOAL>‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖
<VAR>a b : ℕ<VAR>ha : Odd a<VAR>hb : Odd b<GOAL>J(↑a | b) = (-1) ^ (a / 2 * (b / 2)) * J(↑b | a)
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = spanSingleton R⁰ k<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(choose ⋯)})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = spanSingleton R⁰ k<VAR>n : R := choose ⋯<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑(choose ⋯)})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = spanSingleton R⁰ k<VAR>n : R := choose ⋯<VAR>d : ↥R⁰ := choose ⋯<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = spanSingleton R⁰ k<VAR>n : R := choose ⋯<VAR>d : ↥R⁰ := choose ⋯<VAR>hnd : mk' K n d = k<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = I
<VAR>R : Type u_1<VAR>inst✝⁴ : CommRing R<VAR>K : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra R K<VAR>inst✝¹ : IsFractionRing R K<VAR>inst✝ : IsDedekindDomain R<VAR>v : HeightOneSpectrum R<VAR>I : FractionalIdeal R⁰ K<VAR>hI : I ≠ 0<VAR>k : K<VAR>hk : I = spanSingleton R⁰ k<VAR>n : R := choose ⋯<VAR>d : ↥R⁰ := choose ⋯<VAR>hnd : mk' K n d = k<VAR>hn0 : n ≠ 0<GOAL>∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ (↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {choose ⋯})).factors) - ↑((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {↑d})).factors)) = I
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<GOAL>a ∈ grade R m ↔ a.support ⊆ {m}
<VAR>M : Type u_1<VAR>ι : Type u_2<VAR>R : Type u_3<VAR>inst✝ : CommSemiring R<VAR>m : M<VAR>a : R[M]<GOAL>a ∈ grade R m ↔ ↑a.support ⊆ {m}
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>m n : ℕ<GOAL>(coeff R m) (X ^ n) = if m = n then 1 else 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k m : ℕ<VAR>hm : k ≤ m<VAR>hk : (f.genEigenspace μ) k ≠ ⊥<GOAL>(f.genEigenspace μ) m ≠ ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k m : ℕ<VAR>hm : k ≤ m<VAR>hk : (f.genEigenspace μ) m = ⊥<GOAL>(f.genEigenspace μ) k = ⊥
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>k m : ℕ<VAR>hm : k ≤ m<VAR>hk : (f.genEigenspace μ) m = ⊥<GOAL>(f.genEigenspace μ) k ≤ (f.genEigenspace μ) m
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>y : β<VAR>h : ∀ x ∈ s, Commute y (f x)<GOAL>Commute y (s.noncommProd f comm)
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>y : β<VAR>h : ∀ x ∈ s, Commute y (f x)<GOAL>∀ x ∈ Multiset.map f s.val, Commute y x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>y✝ : β<VAR>h : ∀ x ∈ s, Commute y✝ (f x)<VAR>y : β<GOAL>y ∈ Multiset.map f s.val → Commute y✝ y
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>f✝ : α → β → β<VAR>op : α → α → α<VAR>inst✝² : Monoid β<VAR>inst✝¹ : Monoid γ<VAR>inst✝ : FunLike F β γ<VAR>s : Finset α<VAR>f : α → β<VAR>comm : (↑s).Pairwise fun a b => Commute (f a) (f b)<VAR>y✝ : β<VAR>h : ∀ x ∈ s, Commute y✝ (f x)<VAR>y : β<GOAL>(∃ a ∈ s.val, f a = y) → Commute y✝ y
<VAR>a✝ b✝ : Prop<VAR>α : Sort u_1<VAR>a b : α<VAR>p : Prop<GOAL>a = b ∧ p ↔ b = a ∧ p