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>ι✝ : 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✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝¹ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this✝ : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<VAR>F1 : δ → α := fun x => F0 (reparam x j) x<VAR>hF1 : F1 = fun x => F0 (reparam x j) x<VAR>g : ℕ → Subtype p := Classical.choose ⋯<VAR>Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k<VAR>this : F1 = fun x => if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x<GOAL>Measurable fun x => F0 (g (Nat.find ⋯)) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<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✝³ : MeasurableSpace δ<VAR>inst✝² : ConditionallyCompleteLinearOrder α<VAR>inst✝¹ : OrderTopology α<VAR>inst✝ : SecondCountableTopology α<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>f : ι → δ → α<VAR>v : Filter ι<VAR>hf : ∀ (i : ι), Measurable (f i)<VAR>p : ι' → Prop<VAR>s : ι' → Set ι<VAR>hv : v.HasCountableBasis p s<VAR>hs : ∀ (j : ι'), (s j).Countable<VAR>this✝¹ : Countable (Subtype p)<VAR>hp : Nonempty (Subtype p)<VAR>H : ¬∃ j, s ↑j = ∅<VAR>this✝ : ∀ (i : ι'), Countable ↑(s i)<VAR>m : Subtype p → Set δ := fun j => {x | BddBelow (range fun i => f (↑i) x)}<VAR>m_meas : ∀ (j : Subtype p), MeasurableSet (m j)<VAR>mc_meas : MeasurableSet {x | ∀ (j : Subtype p), x ∉ m j}<VAR>j : Subtype p<VAR>reparam : δ → Subtype p → Subtype p := fun x => liminf_reparam (fun i => f i x) s p<VAR>F0 : Subtype p → δ → α := fun j x => ⨅ i, f (↑i) x<VAR>F0_meas : ∀ (j : Subtype p), Measurable (F0 j)<VAR>F1 : δ → α := fun x => F0 (reparam x j) x<VAR>hF1 : F1 = fun x => F0 (reparam x j) x<VAR>g : ℕ → Subtype p := Classical.choose ⋯<VAR>Z : ∀ (x : δ), ∃ n, x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k<VAR>this : F1 = fun x => if x ∈ m j then F0 j x else F0 (g (Nat.find ⋯)) x<VAR>n : ℕ<GOAL>MeasurableSet {x | x ∈ m (g n) ∨ ∀ (k : Subtype p), x ∉ m k}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<GOAL>balancedCoreAux 𝕜 ∅ = ∅
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : NormedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t : Set E<GOAL>∀ (a : E), ∃ i, ∃ (_ : 1 ≤ ‖i‖), a ∉ ∅
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>m0 : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>inst✝ : ConditionallyCompleteLinearOrderBot ι<VAR>a b : ℝ<VAR>f : ι → Ω → ℝ<VAR>N : ι<VAR>n m : ℕ<VAR>ω : Ω<GOAL>lowerCrossingTime a b f N n ω ≤ N
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>relabel Sum.inl φ = castLE ⋯ φ
<VAR>L : Language<VAR>L' : Language<VAR>M : Type w<VAR>N : Type u_1<VAR>P : Type u_2<VAR>inst✝² : L.Structure M<VAR>inst✝¹ : L.Structure N<VAR>inst✝ : L.Structure P<VAR>α : Type u'<VAR>β : Type v'<VAR>γ : Type u_3<VAR>n : ℕ<VAR>φ : L.BoundedFormula α n<GOAL>mapTermRel (fun x t => Term.relabel (Sum.map id (natAdd 0)) t) (fun x => id) (fun x => castLE ⋯) φ = castLE ⋯ φ
<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>hμ : f.HasEigenvalue μ<GOAL>μ ∈ spectrum R f
<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>hμ : f.HasEigenvalue μ<VAR>h_unit : IsUnit ((algebraMap R (End R M)) μ - f)<GOAL>False
<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>hμ : f.HasEigenvalue μ<VAR>h_unit : IsUnit ((algebraMap R (End R M)) μ - f)<VAR>f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit<GOAL>False
<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>hμ : f.HasEigenvalue μ<VAR>h_unit : IsUnit ((algebraMap R (End R M)) μ - f)<VAR>f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit<VAR>v : M<VAR>hv : f.HasEigenvector μ v<GOAL>False
<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>hμ : f.HasEigenvalue μ<VAR>h_unit : IsUnit ((algebraMap R (End R M)) μ - f)<VAR>f' : M ≃ₗ[R] M := LinearMap.GeneralLinearGroup.toLinearEquiv h_unit.unit<VAR>v : M<VAR>hv : f.HasEigenvector μ v<GOAL>μ • v - f v = 0
<VAR>α : Type u_1<VAR>m : Set (OuterMeasure α)<VAR>s : Set α<VAR>h : m.Nonempty<GOAL>(sInf m) s = ⨅ t, ⨅ (_ : s ⊆ iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, μ (t n)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>f : γ → β<VAR>this : UniformSpace γ := UniformSpace.comap f inst✝<GOAL>uniformSpace α γ = UniformSpace.comap (fun x => f ∘ x) (uniformSpace α β)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : Finite α<VAR>inst✝ : Finite β<VAR>this✝ : Fintype α<VAR>this : Fintype β<GOAL>Nat.card (α ⊕ β) = Nat.card α + Nat.card β
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.52509, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : PreservesFiniteLimits s<VAR>hF : IsSheaf (coherentTopology C) F<GOAL>IsSheaf (coherentTopology C) (F ⋙ s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.52509, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : PreservesFiniteLimits s<VAR>hF : Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F<GOAL>Nonempty (PreservesFiniteProducts (F ⋙ s)) ∧ EqualizerCondition (F ⋙ s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.52509, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : PreservesFiniteLimits s<VAR>hF : Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F<VAR>this : PreservesFiniteProducts F<GOAL>Nonempty (PreservesFiniteProducts (F ⋙ s)) ∧ EqualizerCondition (F ⋙ s)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁶ : Category.{u_3, u_1} C<VAR>inst✝⁵ : Category.{?u.52509, u_2} D<VAR>F✝ : C ⥤ D<VAR>A : Type u₃<VAR>inst✝⁴ : Category.{v₃, u₃} A<VAR>F : Cᵒᵖ ⥤ A<VAR>B : Type u₄<VAR>inst✝³ : Category.{v₄, u₄} B<VAR>s : A ⥤ B<VAR>inst✝² : Preregular C<VAR>inst✝¹ : FinitaryExtensive C<VAR>h : ∀ {Y X : C} (f : Y ⟶ X) [inst : EffectiveEpi f], HasPullback f f<VAR>inst✝ : PreservesFiniteLimits s<VAR>hF : Nonempty (PreservesFiniteProducts F) ∧ EqualizerCondition F<VAR>this : PreservesFiniteProducts F<VAR>x✝² x✝¹ : C<VAR>π : x✝² ⟶ x✝¹<VAR>x✝ : EffectiveEpi π<VAR>c : PullbackCone π π<VAR>hc : IsLimit c<GOAL>IsLimit (Fork.ofι ((F ⋙ s).map π.op) ⋯)
<VAR>R : Type u<VAR>S : Type v<VAR>ι : Type w<VAR>a b : R<VAR>m n : ℕ<VAR>K : Type u_1<VAR>inst✝ : DivisionRing K<VAR>p : K[X]<VAR>h : p ≠ 0<GOAL>(p * C p.leadingCoeff⁻¹).Monic
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>r : ℝ≥0∞<VAR>h : r < dimH s<GOAL>∃ x ∈ s, ∀ t ∈ 𝓝[s] x, r < dimH t
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>r : ℝ≥0∞<VAR>h : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, dimH t ≤ r<GOAL>dimH s ≤ r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>r : ℝ≥0∞<VAR>t : X → Set X<VAR>htx : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>htr : ∀ x ∈ s, dimH (t x) ≤ r<GOAL>dimH s ≤ r
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝² : EMetricSpace X<VAR>inst✝¹ : EMetricSpace Y<VAR>inst✝ : SecondCountableTopology X<VAR>s : Set X<VAR>r : ℝ≥0∞<VAR>t : X → Set X<VAR>htx : ∀ x ∈ s, t x ∈ 𝓝[s] x<VAR>htr : ∀ x ∈ s, dimH (t x) ≤ r<VAR>S : Set X<VAR>hSs : S ⊆ s<VAR>hSc : S.Countable<VAR>hSU : s ⊆ ⋃ x ∈ S, t x<GOAL>dimH s ≤ r
<VAR>t t' : Type u → Type u<VAR>eqv : (α : Type u) → t α ≃ t' α<VAR>inst✝¹ : Functor t<VAR>inst✝ : LawfulFunctor t<VAR>h₀ : ∀ {α β : Type u} (f : α → β), map f = Equiv.map eqv f<VAR>h₁ : ∀ {α β : Type u} (f : β), mapConst f = (Equiv.map eqv ∘ Function.const α) f<GOAL>LawfulFunctor t'
<VAR>R : Type ?u.5<VAR>inst✝ : Field R<VAR>a b : R<VAR>hab : a ^ 2 + b ^ 2 ≠ 0<GOAL>!![a, -b; b, a].det ≠ 0
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>p✝ m : ℕ<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>p ∈ restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n
<VAR>σ : Type u<VAR>R : Type v<VAR>inst✝ : CommSemiring R<VAR>p✝ m : ℕ<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>↑p.support ⊆ {n_1 | ∀ (i : σ), n_1 i ≤ n} ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NonUnitalNormedRing A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : SMulCommClass 𝕜 A A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : 𝓜(𝕜, A)<VAR>h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C<GOAL>‖a.toProd.1‖ = ‖a.toProd.2‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NonUnitalNormedRing A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : SMulCommClass 𝕜 A A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : 𝓜(𝕜, A)<VAR>h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C<VAR>h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊<GOAL>‖a.toProd.1‖ = ‖a.toProd.2‖
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NonUnitalNormedRing A<VAR>inst✝⁴ : NormedSpace 𝕜 A<VAR>inst✝³ : SMulCommClass 𝕜 A A<VAR>inst✝² : IsScalarTower 𝕜 A A<VAR>inst✝¹ : StarRing A<VAR>inst✝ : CstarRing A<VAR>a : 𝓜(𝕜, A)<VAR>h0 : ∀ (f : A →L[𝕜] A) (C : ℝ≥0), (∀ (b : A), ‖f b‖₊ ^ 2 ≤ C * ‖f b‖₊ * ‖b‖₊) → ‖f‖₊ ≤ C<VAR>h1 : ∀ (b : A), ‖a.toProd.1 b‖₊ ^ 2 ≤ ‖a.toProd.2‖₊ * ‖a.toProd.1 b‖₊ * ‖b‖₊<VAR>h2 : ∀ (b : A), ‖a.toProd.2 b‖₊ ^ 2 ≤ ‖a.toProd.1‖₊ * ‖a.toProd.2 b‖₊ * ‖b‖₊<GOAL>‖a.toProd.1‖ = ‖a.toProd.2‖
<VAR>X : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>s : Set (OnePoint X)<VAR>t : Set X<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : DiscreteTopology X<VAR>f : OnePoint X → Y<GOAL>Continuous f ↔ Tendsto (fun x => f ↑x) cofinite (𝓝 (f ∞))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : Submodule R M<VAR>S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}}<GOAL>p = sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : Submodule R M<VAR>S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}}<GOAL>p ≤ sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}}
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : Submodule R M<VAR>S : Set (Submodule R M) := {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}}<GOAL>sSup {T | ∃ m ∈ p, m ≠ 0 ∧ T = span R {m}} ≤ p
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>φ' : S' ⟶ R<VAR>d : M.Derivation φ<VAR>f : M ⟶ N<VAR>X✝ Y✝ : Dᵒᵖ<VAR>x✝¹ : X✝ ⟶ Y✝<VAR>x✝ : ↑(R.obj X✝)<GOAL>(fun {X} => (Hom.app f X).toAddMonoidHom.comp d.d) ((R.map x✝¹) x✝) = (N.map x✝¹) ((fun {X} => (Hom.app f X).toAddMonoidHom.comp d.d) x✝)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : Cᵒᵖ ⥤ CommRingCat<VAR>F : C ⥤ D<VAR>S' R : Dᵒᵖ ⥤ CommRingCat<VAR>M N : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)<VAR>φ : S ⟶ F.op ⋙ R<VAR>φ' : S' ⟶ R<VAR>d : M.Derivation φ<VAR>f : M ⟶ N<VAR>X : Cᵒᵖ<VAR>a : ↑(S.obj X)<GOAL>(Hom.app f (Opposite.op (F.obj (Opposite.unop X)))) (d.d ((φ.app X) a)) = 0
<VAR>a b : ℝ<VAR>n : ℕ<VAR>f : ℝ → ℝ<VAR>μ ν : Measure ℝ<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>c d : ℝ<GOAL>IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<VAR>s : Set α<GOAL>r.inv.preimage s = r.image s
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s✝ s t : Multiset α<VAR>h : s.Disjoint t<GOAL>s.ndunion t = s.dedup + t
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a✝ b✝ : List α<VAR>h : Disjoint (Quot.mk Setoid.r a✝) (Quot.mk Setoid.r b✝)<GOAL>ndunion (Quot.mk Setoid.r a✝) (Quot.mk Setoid.r b✝) = dedup (Quot.mk Setoid.r a✝) + Quot.mk Setoid.r b✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h : (filter p s).card = s.card<VAR>x : α<VAR>hx : x ∈ s<GOAL>p x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>s t u : Finset α<VAR>f : α → β<VAR>n : ℕ<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>h : (filter p s).card = s.card<VAR>x : α<VAR>hx : x ∈ s ∧ p x<GOAL>p x
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<GOAL>I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
<VAR>𝕜 : Type u_1<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝² : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹ : TopologicalSpace M<VAR>inst✝ : ChartedSpace H M<VAR>x : M<GOAL>↑(extChartAt I x) x ∉ interior (range ↑I) → ↑(extChartAt I x) x ∈ range ↑I ∧ ↑(extChartAt I x) x ∉ interior (range ↑I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : Finite α<VAR>f : α → α<GOAL>Injective f ↔ Bijective f
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z X Y : C<GOAL>(ρ_ X).inv ▷ Y ≫ (α_ X (𝟙_ C) Y).hom = X ◁ (λ_ Y).inv
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : PartialOrder R<VAR>inst✝¹ : StarRing R<VAR>inst✝ : StarOrderedRing R<VAR>x : R<GOAL>star x ≤ 1 ↔ x ≤ 1
<VAR>α : Type u_1<VAR>M₀ : Type u_2<VAR>G₀ : Type u_3<VAR>M₀' : Type u_4<VAR>G₀' : Type u_5<VAR>F : Type u_6<VAR>F' : Type u_7<VAR>inst✝¹ : MonoidWithZero M₀<VAR>inst✝ : GroupWithZero G₀<VAR>a b : G₀<VAR>p : (g : G₀) → g ≠ 0 → Prop<GOAL>(∃ g hg, p g hg) ↔ ∃ g hg, p ↑(mk0 g hg) ⋯
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>f : G →g G'<VAR>f' : G' →g G''<VAR>u v u' v' : V<VAR>p : G.Walk u v<VAR>hinj : Injective ⇑f<VAR>hp : p.IsPath<GOAL>(Walk.map f p).IsPath
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : PolishSpace α<VAR>s : Set α<VAR>hs : IsOpen s<GOAL>IsClopenable s
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₂ ≤ 0<GOAL>Wbtw R (r₁ • v +ᵥ x) x (r₂ • v +ᵥ x)
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝³ : LinearOrderedField R<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module R V<VAR>inst✝ : AddTorsor V P<VAR>x : P<VAR>v : V<VAR>r₁ r₂ : R<VAR>hr₁ : 0 ≤ r₁<VAR>hr₂ : r₂ ≤ 0<GOAL>Wbtw R (r₂ • v +ᵥ x) x (r₁ • v +ᵥ x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hfi : Integrable f μ<GOAL>∫ (x : α), f x ∂μ = 0 ↔ f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hfi : Integrable f μ<GOAL>∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hfi : Integrable f μ<GOAL>(fun a => ENNReal.ofReal (f a)) =ᶠ[ae μ] 0 ↔ f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NormedSpace 𝕜 E<VAR>inst✝⁷ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : FirstCountableTopology X<VAR>f : α → ℝ<VAR>hf : 0 ≤ᶠ[ae μ] f<VAR>hfi : Integrable f μ<GOAL>AEMeasurable (fun a => ENNReal.ofReal (f a)) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>𝔖 : Set (Set α)<VAR>F : ι → α →ᵤ[𝔖] β<VAR>f : α →ᵤ[𝔖] β<GOAL>Tendsto F p (𝓝 f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(toFun 𝔖) ∘ F) ((toFun 𝔖) f) p s
<VAR>R M : Type u<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>I : Ideal R<VAR>F F' : I.Filtration M<VAR>h : F.Stable<VAR>x✝ : PolynomialModule R M<GOAL>x✝ ∈ (F ⊓ F').submodule ↔ x✝ ∈ F.submodule ⊓ F'.submodule
<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>inst✝ : Semiring S<VAR>p : R[X]<VAR>n : ℕ<VAR>h : ¬p = 0<GOAL>↑n < p.degree ↔ n < p.natDegree
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t✝ : Set α<VAR>s : ι → Set α<VAR>t : Set ι<VAR>ht : t.Countable<VAR>p : α → Prop<GOAL>(∀ᵐ (x : α) ∂μ.restrict (⋃ i ∈ t, s i), p x) ↔ ∀ i ∈ t, ∀ᵐ (x : α) ∂μ.restrict (s i), p x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace 𝕜 E<VAR>inst✝¹³ : LocallyCompactSpace E<VAR>F : Type u_3<VAR>inst✝¹² : NormedAddCommGroup F<VAR>inst✝¹¹ : NormedSpace 𝕜 F<VAR>α : Type u_4<VAR>inst✝¹⁰ : TopologicalSpace α<VAR>inst✝⁹ : MeasurableSpace α<VAR>inst✝⁸ : MeasurableSpace E<VAR>inst✝⁷ : OpensMeasurableSpace α<VAR>inst✝⁶ : OpensMeasurableSpace E<VAR>f✝ : α → E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝⁵ : CompleteSpace F<VAR>inst✝⁴ : LocallyCompactSpace 𝕜<VAR>inst✝³ : MeasurableSpace 𝕜<VAR>inst✝² : OpensMeasurableSpace 𝕜<VAR>inst✝¹ : MeasurableSpace F<VAR>inst✝ : BorelSpace F<VAR>f : α → 𝕜 → F<VAR>hf : Continuous (Function.uncurry f)<GOAL>Measurable fun p => deriv (f p.1) p.2
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : TopologicalSpace γ<VAR>inst✝ : TopologicalSpace δ<VAR>g : SpectralMap β γ<VAR>f₁ f₂ : SpectralMap α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>m : Type u<VAR>n : Type v<VAR>α : Type w<VAR>inst✝⁴ : DecidableEq n<VAR>inst✝³ : Fintype n<VAR>inst✝² : DecidableEq m<VAR>inst✝¹ : Fintype m<VAR>inst✝ : CommRing α<VAR>A : Matrix n n α<VAR>j : n<GOAL>A.det = ∑ i : n, A i j * A.adjugate j i