ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>R : Type u_5<VAR>inst✝⁶ : MeasurableSpace X<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : MeasurableSpace Y<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>f✝ g : X → E<VAR>μ : Measure X<VAR>s : Set X<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>f : X → E<VAR>p : ℝ≥0∞<VAR>hf : Memℒp f p μ<VAR>hp : 1 ≤ p<VAR>x : X<VAR>U : Set X<VAR>hU : U ∈ 𝓝 x<VAR>h'U : μ U < ⊤<VAR>this : Fact (μ U < ⊤)<GOAL>Memℒp f 1 (μ.restrict U)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t✝ s : Set A<VAR>t : Set B<GOAL>adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) = (adjoin R s).prod (adjoin R t)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t✝ s : Set A<VAR>t : Set B<GOAL>adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1})) ≤ (adjoin R s).prod (adjoin R t)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t✝ s : Set A<VAR>t : Set B<GOAL>(adjoin R s).prod (adjoin R t) ≤ adjoin R (⇑(LinearMap.inl R A B) '' (s ∪ {1}) ∪ ⇑(LinearMap.inr R A B) '' (t ∪ {1}))
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<GOAL>IsQuasiregular x ↔ IsUnit (1 + x)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<GOAL>IsQuasiregular x
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<GOAL>∃ y, y + x + x * y = 0 ∧ x + y + y * x = 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<GOAL>↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0 ∧ x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<GOAL>↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<GOAL>x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<VAR>this : (1 + x) * ↑hx.unit⁻¹ - 1 = 1 - 1<GOAL>↑hx.unit⁻¹ - 1 + x + x * (↑hx.unit⁻¹ - 1) = 0
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>x : R<VAR>hx : IsUnit (1 + x)<VAR>this : ↑hx.unit⁻¹ * (1 + x) - 1 = 1 - 1<GOAL>x + (↑hx.unit⁻¹ - 1) + (↑hx.unit⁻¹ - 1) * x = 0
<VAR>a b m n : ℕ+<VAR>cop : m.Coprime n<VAR>am : a ∣ m<VAR>bn : b ∣ n<GOAL>a = (a * b).gcd m
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Monoid G<VAR>a : G<VAR>n : ℕ<VAR>inst✝ : MulAction G H<VAR>b : H<GOAL>(fun x => a • x)^[Nat.zero] b = a ^ Nat.zero • b
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>G : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Monoid G<VAR>a : G<VAR>n✝ : ℕ<VAR>inst✝ : MulAction G H<VAR>b : H<VAR>n : ℕ<VAR>ih : (fun x => a • x)^[n] b = a ^ n • b<GOAL>(fun x => a • x)^[n.succ] b = a ^ n.succ • b
<VAR>m n✝ a n : ℕ<GOAL>pred^[n + 1] a = a - (n + 1)
<VAR>m n✝ a n : ℕ<GOAL>(pred ∘ pred^[n]) a = (a - n).pred
<VAR>l : Type u_1<VAR>m : Type u<VAR>n : Type u'<VAR>α : Type v<VAR>inst✝² : Fintype n<VAR>inst✝¹ : DecidableEq n<VAR>inst✝ : CommRing α<VAR>A B : Matrix n n α<VAR>v : n → α<GOAL>IsUnit (diagonal v) ↔ IsUnit v
<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 K : Subgroup G<GOAL>Codisjoint (H.subgroupOf (H ⊔ K)) (K.subgroupOf (H ⊔ K))
<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 K : Subgroup G<GOAL>H ≤ H ⊔ K
<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 K : Subgroup G<GOAL>K ≤ H ⊔ K
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConcaveOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : MonovaryOn f g s<GOAL>ConvexOn 𝕜 s (-f • -g)
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : LieRing L<VAR>inst✝ : LieAlgebra R L<VAR>h : LieAlgebra.center R L = ⊥<GOAL>Function.Injective ⇑(ad R L)
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : SMul M α<VAR>inst✝¹ : MeasurableSMul M α<VAR>c : M<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure M α μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>(Measure.map (fun x => c • x) μ) s = μ s
<VAR>G : Type u<VAR>M : Type v<VAR>α : Type w<VAR>s✝ : Set α<VAR>m : MeasurableSpace α<VAR>inst✝³ : MeasurableSpace M<VAR>inst✝² : SMul M α<VAR>inst✝¹ : MeasurableSMul M α<VAR>c : M<VAR>μ : Measure α<VAR>inst✝ : SMulInvariantMeasure M α μ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>μ ((fun x => c • x) ⁻¹' s) = μ s
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝ : Category.{u_2, u_1} D<VAR>P : MorphismProperty D<VAR>F : C ⥤ D<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>P.inverseImage F f ↔ P (F.map f)
<VAR>ι : Type u_1<VAR>Ω : Type u_2<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : PseudoEMetricSpace Ω<VAR>μ : Measure Ω<GOAL>levyProkhorovDist μ μ = 0
<VAR>a b c d m n : ℤ<VAR>h : 1 < a.natAbs<GOAL>Function.Injective (natAbs ∘ fun x => a ^ x)
<VAR>a b c d m n : ℤ<VAR>h : 1 < a.natAbs<VAR>x✝ : ℕ<GOAL>(natAbs ∘ fun x => a ^ x) x✝ = a.natAbs ^ x✝
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<GOAL>∀ (a_1 : R), star a * a_1 = a_1 * star a
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star a * (b * c) = star a * (star (star b) * star (star c))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star a * (star (star b) * star (star c)) = star a * star (star c * star b)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star a * star (star c * star b) = star (star c * star b * a)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star c * star b * a) = star (star c * (star b * a))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star c * (star b * a)) = star (star b * a) * c
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star b * a) * c = star a * b * c
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>b * star a * c = star (star c * star (b * star a))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star c * star (b * star a)) = star (star c * (a * star b))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star c * (a * star b)) = star (star c * a * star b)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (star c * a * star b) = b * (star a * c)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>b * c * star a = star (a * star (b * c))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (a * star (b * c)) = star (a * (star c * star b))
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (a * (star c * star b)) = star (a * star c * star b)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>star (a * star c * star b) = b * star (a * star c)
<VAR>R : Type u_1<VAR>inst✝¹ : Mul R<VAR>inst✝ : StarMul R<VAR>a : R<VAR>s : Set R<VAR>ha : a ∈ center R<VAR>b c : R<GOAL>b * star (a * star c) = b * (c * star a)
<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 l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>(R.boundedFormula₂ t₁ t₂).Realize v xs ↔ RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
<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 l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>(RelMap R fun i => realize (Sum.elim v xs) (![t₁, t₂] i)) = RelMap R ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂]
<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 l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>realize (Sum.elim v xs) (![t₁, t₂] 0) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] 0
<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 l : ℕ<VAR>φ ψ : L.BoundedFormula α l<VAR>θ : L.BoundedFormula α l.succ<VAR>v : α → M<VAR>xs : Fin l → M<VAR>R : L.Relations 2<VAR>t₁ t₂ : L.Term (α ⊕ Fin l)<GOAL>∀ (i : Fin 1), realize (Sum.elim v xs) (![t₁, t₂] i.succ) = ![realize (Sum.elim v xs) t₁, realize (Sum.elim v xs) t₂] i.succ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<VAR>C : ℝ≥0<VAR>hC : ∀ (x : α), ↑φ x ≤ C<GOAL>∃ δ > 0, ∀ (s : Set α), μ s < δ → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<VAR>C : ℝ≥0<VAR>hC : ∀ (x : α), ↑φ x ≤ C<GOAL>∀ (s : Set α), μ s < (ε₂ - ε₁) / ↑C → ∫⁻ (x : α) in s, f x ∂μ < ε
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<VAR>C : ℝ≥0<VAR>hC : ∀ (x : α), ↑φ x ≤ C<VAR>s : Set α<VAR>hs : μ s < (ε₂ - ε₁) / ↑C<GOAL>∫⁻ (x : α) in s, f x ∂μ ≤ ε₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<VAR>C : ℝ≥0<VAR>hC : ∀ (x : α), ↑φ x ≤ C<VAR>s : Set α<VAR>hs : μ s < (ε₂ - ε₁) / ↑C<GOAL>∀ (i : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑i x) ≤ f x) → (SimpleFunc.map ofNNReal i).lintegral (μ.restrict s) ≤ ε₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>h : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>ε₂ : ℝ≥0∞<VAR>hε₂0 : 0 < ε₂<VAR>hε₂ε : ε₂ < ε<VAR>ε₁ : ℝ≥0∞<VAR>hε₁0 : 0 < ε₁<VAR>hε₁₂ : ε₁ < ε₂<VAR>φ : α →ₛ ℝ≥0<VAR>left✝ : ∀ (x : α), ↑(↑φ x) ≤ f x<VAR>hφ : ∀ (ψ : α →ₛ ℝ≥0), (∀ (x : α), ↑(↑ψ x) ≤ f x) → (SimpleFunc.map ofNNReal (ψ - φ)).lintegral μ < ε₁<VAR>C : ℝ≥0<VAR>hC : ∀ (x : α), ↑φ x ≤ C<VAR>s : Set α<VAR>hs : μ s < (ε₂ - ε₁) / ↑C<VAR>ψ : α →ₛ ℝ≥0<VAR>hψ : ∀ (x : α), ↑(↑ψ x) ≤ f x<GOAL>(SimpleFunc.map ofNNReal ψ).lintegral (μ.restrict s) ≤ ε₂
<VAR>M : Type u_1<VAR>inst✝² : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝¹ : CommMonoid N<VAR>P : Type u_3<VAR>inst✝ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>x : M<VAR>y : ↥S<GOAL>f.toMap ((f.sec (f.mk' x y)).1 * ↑y) = f.toMap (x * ↑(f.sec (f.mk' x y)).2)
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<GOAL>(condCount s) (t ∩ u) = (condCount (s ∩ u)) t * (condCount s) u
<VAR>Ω : Type u_1<VAR>inst✝¹ : MeasurableSpace Ω<VAR>inst✝ : MeasurableSingletonClass Ω<VAR>s t u : Set Ω<VAR>hs : s.Finite<GOAL>(condCount s) (u ∩ t) = (condCount (s ∩ u)) t * (condCount s) u
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<GOAL>(multiplicity a (-b)).Dom ↔ (multiplicity a b).Dom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h₁ : (multiplicity a (-b)).Dom<VAR>h₂ : (multiplicity a b).Dom<GOAL>↑((multiplicity a (-b)).get h₁) = ↑((multiplicity a b).get h₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Ring α<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>a b : α<VAR>h₁ : (multiplicity a (-b)).Dom<VAR>h₂ : (multiplicity a b).Dom<GOAL>multiplicity a (-b) = ↑((multiplicity a b).get h₂)
<VAR>X✝ : Type u_1<VAR>Y✝ : Type u_2<VAR>inst✝³ : TopologicalSpace X✝<VAR>X : Type u_3<VAR>Y : Type u_4<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : T1Space Y<VAR>y : Y<VAR>s : Set X<VAR>x✝ : IsClosed s<VAR>h2s : s.Nonempty<GOAL>IsClosed (const X y '' s)
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>n d : ℕ<VAR>f : K⟦X⟧<VAR>H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))<VAR>hnd : n < d<GOAL>(PowerSeries.coeff K n) f = 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>n d : ℕ<VAR>f : K⟦X⟧<VAR>H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))<VAR>hnd : n < d<GOAL>PowerSeries.X ^ d ∣ f
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝ : Field K<VAR>n d : ℕ<VAR>f : K⟦X⟧<VAR>H : Valued.v ((ofPowerSeries ℤ K) f) ≤ ↑(Multiplicative.ofAdd (-↑d))<VAR>hnd : n < d<GOAL>(PowerSeries.idealX K).valuation ((algebraMap K⟦X⟧ (LaurentSeries K)) f) ≤ ↑(Multiplicative.ofAdd (-↑d))
<VAR>n : ℕ<VAR>hn : n ≠ 0<VAR>x : ℝ≥0∞<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>x y : ℝ<GOAL>Real.toEReal '' Icc x y = Icc ↑x ↑y
<VAR>x y : ℝ<GOAL>WithBot.some '' (WithTop.some '' Icc x y) = Icc ↑x ↑y
<VAR>x y : ℝ<GOAL>Icc ↑↑x ↑↑y = Icc ↑x ↑y
<VAR>X : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : Semiring R<VAR>inst✝¹ : TopologicalSpace R<VAR>inst✝ : TopologicalSemiring R<VAR>x : X<VAR>f : C(X, R)<GOAL>f ∈ idealOfSet R {x}ᶜ ↔ f x = 0
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>ui : (i : ι) → ↑(S i) → ↑(S i)<VAR>uβ : β → β<VAR>h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)<VAR>u : ↑(iUnion S) → ↑(iUnion S)<VAR>hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)<VAR>x : ↑(iUnion S)<GOAL>iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>ui : (i : ι) → ↑(S i) → ↑(S i)<VAR>uβ : β → β<VAR>h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)<VAR>u : ↑(iUnion S) → ↑(iUnion S)<VAR>hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)<VAR>x : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<GOAL>iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>ui : (i : ι) → ↑(S i) → ↑(S i)<VAR>uβ : β → β<VAR>h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)<VAR>u : ↑(iUnion S) → ↑(iUnion S)<VAR>hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)<VAR>x : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<GOAL>iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)
<VAR>α : Type u_1<VAR>ι : Sort u_2<VAR>β : Sort u_3<VAR>S : ι → Set α<VAR>f : (i : ι) → ↑(S i) → β<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>ui : (i : ι) → ↑(S i) → ↑(S i)<VAR>uβ : β → β<VAR>h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)<VAR>u : ↑(iUnion S) → ↑(iUnion S)<VAR>hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)<VAR>x : ↑(iUnion S)<VAR>i : ι<VAR>hi : ↑x ∈ S i<VAR>this : x = inclusion ⋯ ⟨↑x, hi⟩<GOAL>iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>1 n = ↑((fun x => ζ x) n)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian f φ<VAR>R' : 𝒮<VAR>a' : 𝒳<VAR>g : R' ⟶ R<VAR>f' : R' ⟶ S<VAR>hf' : f' = g ≫ f<VAR>φ' : a' ⟶ b<VAR>inst✝ : p.IsHomLift f' φ'<GOAL>∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R✝ : 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>a' : 𝒳<VAR>φ' : a' ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>g : p.obj a' ⟶ R✝<VAR>f : R✝ ⟶ p.obj b✝<VAR>inst✝¹ : p.IsStronglyCartesian f φ<VAR>hf' : p.map φ' = g ≫ f<VAR>inst✝ : p.IsHomLift (p.map φ') φ'<GOAL>∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R : 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>a' : 𝒳<VAR>φ' : a' ⟶ b<VAR>g : p.obj a' ⟶ R<VAR>f : R ⟶ p.obj b<VAR>inst✝¹ : p.IsStronglyCartesian f φ<VAR>hf' : p.map φ' = g ≫ f<VAR>inst✝ : p.IsHomLift (p.map φ') φ'<VAR>this : p.IsHomLift (g ≫ f) φ'<GOAL>∃! χ, p.IsHomLift g χ ∧ χ ≫ φ = φ'
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>inst✝ : Fintype α<GOAL>𝒜.shatterer.card ≤ ∑ k ∈ Iic 𝒜.vcDim, (Fintype.card α).choose k
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>inst✝ : Fintype α<GOAL>𝒜.shatterer.card ≤ ∑ x ∈ Iic 𝒜.vcDim, (powersetCard x univ).card
<VAR>α : Type u_1<VAR>inst✝¹ : DecidableEq α<VAR>𝒜 ℬ : Finset (Finset α)<VAR>s✝ t : Finset α<VAR>a : α<VAR>n : ℕ<VAR>inst✝ : Fintype α<VAR>s : Finset α<VAR>hs : s ∈ 𝒜.shatterer<GOAL>s.card ∈ Iic 𝒜.vcDim ∧ s ∈ powersetCard s.card univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<GOAL>Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 (∑' (n : ℕ), f n))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>f✝ g : α → ℝ≥0∞<VAR>f : ℕ → ℝ≥0∞<GOAL>HasSum f (∑' (n : ℕ), f n)
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>-(a - b) = -a + b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>0 - (a - b) = 0 - a + b
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y : C<VAR>a b : X ⟶ Y<GOAL>0 - 0 - (a - b) = 0 - a + b
<VAR>x : ℝ<VAR>h1 : 0 ≤ x<VAR>h2 : x ≤ 1<VAR>n : ℕ<VAR>hn : 0 < n<VAR>h3 : |x| = x<VAR>h4 : |x| ≤ 1<GOAL>rexp x ≤ ∑ m ∈ range n, x ^ m / ↑m.factorial + x ^ n * (↑n + 1) / (↑n.factorial * ↑n)