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>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hfi : HasFiniteIntegral f μ<GOAL>IsFiniteMeasure (μ.withDensity fun x => ENNReal.ofReal (f x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → ℝ<VAR>hfi : HasFiniteIntegral f μ<VAR>x : α<GOAL>ENNReal.ofReal (f x) ≤ ↑‖f x‖₊
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atBot.IsMeasurablyGenerated<VAR>inst✝ : atTop.IsMeasurablyGenerated<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<VAR>ho' : f =O[atTop] g'<VAR>hg' : IntegrableAtFilter g' atTop μ<GOAL>Integrable f μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atBot.IsMeasurablyGenerated<VAR>inst✝ : atTop.IsMeasurablyGenerated<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<VAR>ho' : f =O[atTop] g'<VAR>hg' : IntegrableAtFilter g' atTop μ<GOAL>StronglyMeasurableAtFilter f atBot μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>f : α → E<VAR>g : α → F<VAR>a b : α<VAR>μ : Measure α<VAR>l : Filter α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : SecondCountableTopology α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : CompactIccSpace α<VAR>g' : α → F<VAR>inst✝¹ : atBot.IsMeasurablyGenerated<VAR>inst✝ : atTop.IsMeasurablyGenerated<VAR>hf : LocallyIntegrable f μ<VAR>ho : f =O[atBot] g<VAR>hg : IntegrableAtFilter g atBot μ<VAR>ho' : f =O[atTop] g'<VAR>hg' : IntegrableAtFilter g' atTop μ<GOAL>StronglyMeasurableAtFilter f atTop μ
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : MulOneClass P<VAR>S : Submonoid M<VAR>A : Type u_4<VAR>inst✝ : SetLike A M<VAR>hA : SubmonoidClass A M<VAR>S' : A<GOAL>↑(⊥.prod ⊥) = ↑⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Set α<VAR>f : α → β<VAR>s : Set β<VAR>H : Function.Injective f<VAR>hs : s ⊆ range f<GOAL>(f ⁻¹' s).ncard = s.ncard
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} A B<VAR>inst✝ : IsDomain B<GOAL>NeZero ↑↑n
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra K L<VAR>inst✝¹ : IsCyclotomicExtension {n} A B<VAR>inst✝ : IsDomain B<VAR>this : NeZero ↑↑n<GOAL>NeZero ↑↑n
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, infEdist x t ≤ r<VAR>H2 : ∀ x ∈ t, infEdist x s ≤ r<GOAL>hausdorffEdist s t ≤ r
<VAR>ι : Sort u_1<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : PseudoEMetricSpace α<VAR>inst✝ : PseudoEMetricSpace β<VAR>x y : α<VAR>s t u : Set α<VAR>Φ : α → β<VAR>r : ℝ≥0∞<VAR>H1 : ∀ x ∈ s, infEdist x t ≤ r<VAR>H2 : ∀ x ∈ t, infEdist x s ≤ r<GOAL>(∀ i ∈ s, infEdist i t ≤ r) ∧ ∀ i ∈ t, infEdist i s ≤ r
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝¹ : SemilatticeSup α<VAR>inst✝ : OrderBot α<VAR>s s₁ s₂ : Finset β<VAR>f✝ g : β → α<VAR>a : α<VAR>P : α → Prop<VAR>Pbot : P ⊥<VAR>Psup : ∀ ⦃x y : α⦄, P x → P y → P (x ⊔ y)<VAR>t : Finset β<VAR>f : β → { x // P x }<VAR>this✝ : SemilatticeSup { x // P x } := Subtype.semilatticeSup Psup<VAR>this : OrderBot { x // P x } := Subtype.orderBot Pbot<GOAL>↑(t.sup f) = t.sup fun x => ↑(f x)
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>hi : i < i0<GOAL>toZ i0 i < 0
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>hi : i < i0<GOAL>toZ i0 i ≤ 0
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>hi : i < i0<GOAL>toZ i0 i ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : CommSemiring R<VAR>c : R<VAR>m : ℕ<GOAL>derivative ((X + C c) ^ m) = C ↑m * (X + C c) ^ (m - 1)
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : LieRing L<VAR>inst✝¹⁰ : LieAlgebra R L<VAR>inst✝⁹ : LieRing L'<VAR>inst✝⁸ : LieAlgebra R L'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : LieRingModule L M<VAR>inst✝⁴ : LieModule R L M<VAR>inst✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>x : L<GOAL>x ∈ ↑f.ker ↔ f x = 0
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : CommRing α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : TopologicalRing α<VAR>x y : α<GOAL>x - y ∈ closure 0 ↔ x - y ∈ ⊥.closure
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>f : α → ℤ<VAR>l : Filter α<GOAL>Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : Absorbent ℝ s<VAR>hr : 0 ≤ r<VAR>hsr : s ⊆ closedBall 0 r<GOAL>‖x‖ / r ≤ gauge s x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>s : Set E<VAR>r : ℝ<VAR>x : E<VAR>hs : Absorbent ℝ s<VAR>hr : 0 ≤ r<VAR>hsr : s ⊆ closedBall 0 r<GOAL>gauge (closedBall 0 r) x ≤ gauge s x
<VAR>C : Type u₁<VAR>inst✝¹² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹¹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹⁰ : AddMonoid M<VAR>inst✝⁹ : HasShift C M<VAR>inst✝⁸ : HasShift D M<VAR>inst✝⁷ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Z Z<VAR>a b c : M<VAR>f : SmallShiftedHom W X Y a<VAR>g : SmallShiftedHom W Y Z b<VAR>h : b + a = c<GOAL>((L.commShiftIso c).app Z).homToEquiv ((SmallHom.equiv W L) (SmallHom.comp f (g.shift a c h))) = ((L.commShiftIso a).app Y).homToEquiv ((SmallHom.equiv W L) f) ≫ (shiftFunctor D a).map (((L.commShiftIso b).app Z).homToEquiv ((SmallHom.equiv W L) g)) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)
<VAR>C : Type u₁<VAR>inst✝¹² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹¹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹⁰ : AddMonoid M<VAR>inst✝⁹ : HasShift C M<VAR>inst✝⁸ : HasShift D M<VAR>inst✝⁷ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Z Z<VAR>a b c : M<VAR>f : SmallShiftedHom W X Y a<VAR>g : SmallShiftedHom W Y Z b<VAR>h : b + a = c<GOAL>((SmallHom.equiv W L) f ≫ (SmallHom.equiv W L) (g.shift a c h)) ≫ ((L.commShiftIso c).app Z).hom = ((SmallHom.equiv W L) f ≫ ((L.commShiftIso a).app Y).hom) ≫ (shiftFunctor D a).map ((SmallHom.equiv W L) g ≫ ((L.commShiftIso b).app Z).hom) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)
<VAR>C : Type u₁<VAR>inst✝¹² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹¹ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝¹⁰ : AddMonoid M<VAR>inst✝⁹ : HasShift C M<VAR>inst✝⁸ : HasShift D M<VAR>inst✝⁷ : W.IsCompatibleWithShift M<VAR>L : C ⥤ D<VAR>inst✝⁶ : L.IsLocalization W<VAR>inst✝⁵ : HasShift D M<VAR>inst✝⁴ : L.CommShift M<VAR>X Y Z T : C<VAR>inst✝³ : HasSmallLocalizedShiftedHom W M X Y<VAR>inst✝² : HasSmallLocalizedShiftedHom W M Y Z<VAR>inst✝¹ : HasSmallLocalizedShiftedHom W M X Z<VAR>inst✝ : HasSmallLocalizedShiftedHom W M Z Z<VAR>a b c : M<VAR>f : SmallShiftedHom W X Y a<VAR>g : SmallShiftedHom W Y Z b<VAR>h : b + a = c<GOAL>(SmallHom.equiv W L) f ≫ (L.commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫ (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z) = (SmallHom.equiv W L) f ≫ (L.commShiftIso a).hom.app Y ≫ (shiftFunctor D a).map ((SmallHom.equiv W L) g) ≫ (shiftFunctor D a).map ((L.commShiftIso b).hom.app Z) ≫ (shiftFunctorAdd' D b a c h).inv.app (L.obj Z)
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>s = trivial G ↔ ∀ x ∈ s, x = 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝ : Group G<VAR>s : Set G<VAR>hs : IsSubgroup s<GOAL>(∀ (x : G), x ∈ s ↔ x = 1) ↔ ∀ x ∈ s, x = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝¹ : Group G<VAR>inst✝ : Group G'<VAR>H K✝ L : Subgroup G<VAR>f : G' →* G<VAR>K : Subgroup G'<GOAL>(comap f H).relindex K = H.relindex (map f K)
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>(fun y => c y / d y) = fun y => c y * (Inv.inv ∘ d) y
<VAR>𝕜 : Type u<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t : Set 𝕜<VAR>L : Filter 𝕜<VAR>𝕜' : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜'<VAR>inst✝ : NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>(c' * d x - c x * d') / d x ^ 2 = c' * (Inv.inv ∘ d) x + c x * (-(d x ^ 2)⁻¹ * d')
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s<GOAL>hitting u s n m₁ ω = hitting u s n m₂ ω
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>h' : ∃ j ∈ Set.Icc n m₁, u j ω ∈ s<GOAL>sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>j : ι<VAR>hj₁ : j ∈ Set.Icc n m₁<VAR>hj₂ : u j ω ∈ s<GOAL>sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = if ∃ j ∈ Set.Icc n m₂, u j ω ∈ s then sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s}) else m₂
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>j : ι<VAR>hj₁ : j ∈ Set.Icc n m₁<VAR>hj₂ : u j ω ∈ s<GOAL>sInf (Set.Icc n m₁ ∩ {i | u i ω ∈ s}) = sInf (Set.Icc n m₂ ∩ {i | u i ω ∈ s})
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : ConditionallyCompleteLinearOrder ι<VAR>u : ι → Ω → β<VAR>s : Set β<VAR>n i : ι<VAR>ω : Ω<VAR>m₁ m₂ : ι<VAR>h : m₁ ≤ m₂<VAR>j : ι<VAR>hj₁ : j ∈ Set.Icc n m₁<VAR>hj₂ : u j ω ∈ s<GOAL>∃ j ∈ Set.Icc n m₂, u j ω ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X✝ I✝ : Set α<VAR>M : Matroid α<VAR>Y : Set α<VAR>I X : Set ↑Y<GOAL>(M.restrictSubtype Y).Basis I X ↔ M.Basis' ↑I ↑X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X✝ I✝ : Set α<VAR>M : Matroid α<VAR>Y : Set α<VAR>I X : Set ↑Y<GOAL>M.Basis (↑I) (↑X ∩ M.E) ∧ ↑X ⊆ Y ↔ M.Basis (↑I) (↑X ∩ M.E)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → β<VAR>E✝ I✝¹ s : Set α<VAR>M✝ : Matroid α<VAR>N : Matroid β<VAR>E X✝ I✝ : Set α<VAR>M : Matroid α<VAR>Y : Set α<VAR>I X : Set ↑Y<GOAL>(M ↾ Y).Basis ↑I ↑X → I ⊆ X
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(image f s).sym2 = image (Sym2.map f) s.sym2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(image f s).sym2.val = (image (Sym2.map f) s.sym2).val
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t : Finset α<VAR>a b : α<VAR>inst✝ : DecidableEq β<VAR>f : α → β<VAR>s : Finset α<GOAL>(Multiset.map f s.val).dedup.sym2 = (Multiset.map (Sym2.map f) s.val.sym2).dedup
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>h : a < b * c<GOAL>a < b / c⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ✝ : Kernel α β<VAR>inst✝ : Fintype ι<VAR>κ : ι → Kernel α β<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((Kernel.sum κ) a) s = ((∑ i : ι, κ i) a) s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : TopologicalSpace Y<VAR>s : Set X<VAR>hs : s.Finite<VAR>f : X → Y<GOAL>ContinuousOn f s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T1Space X<VAR>inst✝ : TopologicalSpace Y<VAR>s : Set X<VAR>hs : s.Finite<VAR>f : X → Y<GOAL>Continuous (s.restrict f)
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>κ : ι → Type u_5<VAR>m₁ m₂ _mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>s t : Set Ω<VAR>S T : Set (Set Ω)<VAR>inst✝ : IsProbabilityMeasure μ<VAR>f : ι → Set Ω<VAR>hf : ∀ (i : ι), MeasurableSet (f i)<GOAL>iIndepSet f μ ↔ ∀ (s : Finset ι), μ (⋂ i ∈ s, f i) = ∏ i ∈ s, μ (f i)
<VAR>ι : Type u_1<VAR>ι₂ : Type u_2<VAR>ι₃ : Type u_3<VAR>R : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>R₁ : Type u_5<VAR>R₂ : Type u_6<VAR>s : ι → Type u_7<VAR>inst✝⁸ : (i : ι) → AddCommMonoid (s i)<VAR>inst✝⁷ : (i : ι) → Module R (s i)<VAR>M : Type u_8<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>E : Type u_9<VAR>inst✝⁴ : AddCommMonoid E<VAR>inst✝³ : Module R E<VAR>F : Type u_10<VAR>inst✝² : AddCommMonoid F<VAR>t : ι → Type u_11<VAR>inst✝¹ : (i : ι) → AddCommMonoid (t i)<VAR>inst✝ : (i : ι) → Module R (t i)<VAR>f : (i : ι) → s i →ₗ[R] t i<VAR>e : ι ≃ ι₂<VAR>m : (i : ι) → s i<GOAL>(((map fun i => f (e.symm i)) ∘ₗ ↑(reindex R s e)).compMultilinearMap (tprod R)) m = ((↑(reindex R t e) ∘ₗ map f).compMultilinearMap (tprod R)) m
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x✝ : FractionRing K[X]<VAR>x : K[X] × ↥K[X]⁰<GOAL>{ toFractionRing := Localization.mk x.1 x.2 } = (IsLocalization.algEquiv K[X]⁰ (FractionRing K[X]) (RatFunc K)) (Localization.mk x.1 x.2)
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>x✝ : FractionRing K[X]<VAR>x : K[X] × ↥K[X]⁰<GOAL>IsLocalization.mk' (RatFunc K) x.1 x.2 = IsLocalization.mk' (RatFunc K) ((RingHom.id K[X]) x.1) ⟨(RingHom.id K[X]) ↑x.2, ⋯⟩
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : NormedAddCommGroup E''<VAR>inst✝⁸ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x✝ x' : G<VAR>y y' : E<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 E'<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝² : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : AddGroup G<VAR>x : G<VAR>hfg : ConvolutionExistsAt f g x L μ<VAR>hfg' : ConvolutionExistsAt f g' x L μ<GOAL>(f ⋆[L, μ] (g + g')) x = (f ⋆[L, μ] g) x + (f ⋆[L, μ] g') x
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝³ : MulZeroClass β<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : PosMulMono β<VAR>inst✝ : MulPosMono β<VAR>l : Filter α<VAR>f₁ f₂ g₁ g₂ : α → β<VAR>hf : f₁ ≤ᶠ[l] f₂<VAR>hg : g₁ ≤ᶠ[l] g₂<VAR>hg₀ : 0 ≤ᶠ[l] g₁<VAR>hf₀ : 0 ≤ᶠ[l] f₂<GOAL>f₁ * g₁ ≤ᶠ[l] f₂ * g₂
<VAR>E : Type u<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>s : Set E<VAR>a x y : E<VAR>h : IsLocalMinOn f s a<VAR>hf : HasFDerivWithinAt f f' s a<VAR>hy : y ∈ posTangentConeAt s a<GOAL>0 ≤ f' y
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I✝ X R J I : Set α<GOAL>uniqueBaseOn ∅ I = loopyOn I
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.151867, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : S₂.Exact<VAR>inst✝³ : Epi S₁.g<VAR>inst✝² : Epi S₂.g<VAR>inst✝¹ : Epi φ.τ₁<VAR>inst✝ : Epi φ.τ₃<VAR>this✝² : Mono S₁.op.f<VAR>this✝¹ : Mono S₂.op.f<VAR>this✝ : Mono (opMap φ).τ₁<VAR>this : Mono (opMap φ).τ₃<GOAL>Epi φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.151867, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₂ : S₂.Exact<VAR>inst✝³ : Epi S₁.g<VAR>inst✝² : Epi S₂.g<VAR>inst✝¹ : Epi φ.τ₁<VAR>inst✝ : Epi φ.τ₃<VAR>this✝³ : Mono S₁.op.f<VAR>this✝² : Mono S₂.op.f<VAR>this✝¹ : Mono (opMap φ).τ₁<VAR>this✝ : Mono (opMap φ).τ₃<VAR>this : Mono (opMap φ).τ₂<GOAL>Epi φ.τ₂
<VAR>m n : ℤ<VAR>even : Even (n - m)<GOAL>m + 2 ≤ n ↔ m < n
<VAR>m n : ℤ<VAR>even : Even (n - m)<GOAL>2 + m ≤ n ↔ m < n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>f ≤ f ⊔ g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<GOAL>↑f ≤ᶠ[ae μ] ↑(f ⊔ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑f a✝ ≤ ↑(f ⊔ g) a✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝⁵ : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝⁴ : TopologicalSpace β<VAR>inst✝³ : TopologicalSpace γ<VAR>inst✝² : TopologicalSpace δ<VAR>inst✝¹ : SemilatticeSup β<VAR>inst✝ : ContinuousSup β<VAR>f g : α →ₘ[μ] β<VAR>a✝ : α<VAR>ha : ↑(f ⊔ g) a✝ = ↑f a✝ ⊔ ↑g a✝<GOAL>↑f a✝ ≤ ↑f a✝ ⊔ ↑g a✝
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra F K<VAR>hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>x : K<VAR>a : L<GOAL>(a ∈ Set.range fun ψ => ψ x) ↔ a ∈ (minpoly F x).rootSet L
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra F K<VAR>hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>x : K<VAR>a : L<GOAL>(a ∈ Set.range fun ψ => ψ x) ↔ (aeval a) (minpoly F x) = 0
<VAR>F : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Field L<VAR>inst✝² : Algebra F L<VAR>inst✝¹ : Algebra F K<VAR>hA : ∀ (x : K), Splits (algebraMap F L) (minpoly F x)<VAR>inst✝ : Algebra.IsAlgebraic F K<VAR>x : K<VAR>a : L<VAR>x✝ : a ∈ Set.range fun ψ => ψ x<VAR>ψ : K →ₐ[F] L<VAR>hψ : (fun ψ => ψ x) ψ = a<GOAL>(aeval a) (minpoly F x) = 0
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>a x y : G<VAR>h : SemiconjBy a x y<GOAL>x = 1 ↔ y = 1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>a b : α<VAR>s : Seq α<VAR>S : Seq (Seq1 α)<GOAL>(match (Seq.cons b s).destruct with | none => (a, S.join) | some s' => (a, (Seq.cons s' S).join)) = (a, (Seq.cons (b, s) S).join)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>f ''ᵁ f ⁻¹ᵁ U = f.opensRange ⊓ U
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X Y : Scheme<VAR>f : X.Hom Y<VAR>H : IsOpenImmersion f<VAR>U : Y.Opens<GOAL>↑(f ''ᵁ f ⁻¹ᵁ U) = ↑(f.opensRange ⊓ U)
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>n : ℕ<VAR>x✝ : 0 < n + 1<GOAL>↑(n + 1 - 1) = ↑(n + 1) - 1
<VAR>R : Type u<VAR>inst✝ : AddGroupWithOne R<VAR>n : ℕ<VAR>x✝ : 0 < n + 1<GOAL>↑(n + 1 - 1) = ↑n
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>s : Multiset ι<VAR>f : ι → ℝ<VAR>hs : ∀ i ∈ s, 0 ≤ f i<VAR>r : ℝ<GOAL>(Multiset.map (fun x => f x ^ r) s).prod = (Multiset.map f s).prod ^ r
<VAR>w x y z : ℝ<VAR>ι : Type u_1<VAR>f : ι → ℝ<VAR>r : ℝ<VAR>l : List ι<VAR>hs : ∀ i ∈ ⟦l⟧, 0 ≤ f i<GOAL>(Multiset.map (fun x => f x ^ r) ⟦l⟧).prod = (Multiset.map f ⟦l⟧).prod ^ r
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : Zero Γ<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : MulZeroOneClass R<GOAL>order 1 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : Zero Γ<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : MulZeroOneClass R<VAR>h✝ : Subsingleton R<GOAL>order 1 = 0
<VAR>Γ : Type u_1<VAR>Γ' : Type u_2<VAR>R : Type u_3<VAR>V : Type u_4<VAR>inst✝² : Zero Γ<VAR>inst✝¹ : PartialOrder Γ<VAR>inst✝ : MulZeroOneClass R<VAR>h✝ : Nontrivial R<GOAL>order 1 = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>c : Computation (WSeq α)<GOAL>(flatten c).destruct = c >>= destruct