ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<VAR>d : ℝ<VAR>left✝ : d > 0<VAR>hd' : ∃ ε, 0 < ε ∧ ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<VAR>d : ℝ<VAR>left✝ : d > 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖<GOAL>∃ c, 0 < c ∧ IntegrableOn (fun t => t ^ (s - 1) * f t) (Ioc 0 c) volume
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<VAR>d : ℝ<VAR>left✝ : d > 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖<GOAL>AEStronglyMeasurable (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioo 0 ε))
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>b : ℝ<VAR>f : ℝ → ℝ<VAR>hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))<VAR>hf : f =O[𝓝[>] 0] fun x => x ^ (-b)<VAR>s : ℝ<VAR>hs : b < s<VAR>d : ℝ<VAR>left✝ : d > 0<VAR>ε : ℝ<VAR>hε : 0 < ε<VAR>hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖<GOAL>HasFiniteIntegral (fun t => t ^ (s - 1) * f t) (volume.restrict (Ioo 0 ε))
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>K : Type u_4<VAR>K₂ : Type u_5<VAR>M : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>V : Type u_9<VAR>V₂ : Type u_10<VAR>inst✝¹³ : Semiring R<VAR>inst✝¹² : Semiring R₂<VAR>inst✝¹¹ : Semiring R₃<VAR>inst✝¹⁰ : AddCommMonoid M<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>inst✝⁸ : AddCommMonoid M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>inst✝⁷ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : Module R₂ M₂<VAR>inst✝⁴ : Module R₃ M₃<VAR>σ₂₁ : R₂ →+* R<VAR>τ₁₂ : R →+* R₂<VAR>τ₂₃ : R₂ →+* R₃<VAR>τ₁₃ : R →+* R₃<VAR>inst✝³ : RingHomCompTriple τ₁₂ τ₂₃ τ₁₃<VAR>F : Type u_11<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F τ₁₂ M M₂<VAR>inst✝ : RingHomSurjective τ₁₂<VAR>f : M →ₛₗ[τ₁₂] M₂<VAR>g : M₂ →ₛₗ[τ₂₃] M₃<VAR>h : g.comp f = 0<VAR>x : M₂<VAR>hx : x ∈ range f<VAR>y : M<VAR>hy : f y = x<GOAL>g x = 0
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c u : αˣ<VAR>a : α<VAR>h : ↑u = a<GOAL>↑u⁻¹ * a = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P : Cubic F<VAR>inst✝¹ : Field F<VAR>inst✝ : Field K<VAR>φ : F →+* K<VAR>x y z : K<VAR>ha : P.a ≠ 0<VAR>h3 : (map φ P).roots = {x, y, z}<GOAL>φ P.b = φ P.a * -(x + y + z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>s : α → Set β<GOAL>⋃ i, s i = range fun a => ↑a.snd
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s✝ s₁ s₂ t t₁ t₂ u s : Set α<GOAL>¬s.Nonempty ↔ s = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a b : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<GOAL>StrictMono f ∨ StrictAnti f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝¹⁰ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁹ : TopologicalSpace α<VAR>inst✝⁸ : OrderTopology α<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder β<VAR>inst✝⁶ : TopologicalSpace β<VAR>inst✝⁵ : OrderTopology β<VAR>inst✝⁴ : Nonempty γ<VAR>inst✝³ : DenselyOrdered α<VAR>a b : α<VAR>δ : Type u_1<VAR>inst✝² : LinearOrder δ<VAR>inst✝¹ : TopologicalSpace δ<VAR>inst✝ : OrderClosedTopology δ<VAR>f : α → δ<VAR>hf_c : Continuous f<VAR>hf_i : Injective f<VAR>H : ∀ {c d : α}, c < d → StrictMono f ∨ StrictAnti f<GOAL>StrictMono f ∨ StrictAnti f
<VAR>m✝ n : ℕ<VAR>i : Fin (n + 1)<VAR>m : Fin n<VAR>h : i ≤ m.castSucc<GOAL>(finSuccEquiv' i) m.succ = some m
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Ring R<VAR>p✝ q✝ p q : R[X]<GOAL>(p - q).natDegree ≤ max p.natDegree q.natDegree
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hcong : ∃ n, λ ^ 2 ∣ ↑u - ↑n<GOAL>u = 1 ∨ u = -1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hcong : ∃ n, 3 ∣ ↑u - ↑n<GOAL>u = 1 ∨ u = -1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ✝ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hcong : ∃ n, 3 ∣ ↑u - ↑n<VAR>hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3<GOAL>u = 1 ∨ u = -1
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ✝ : IsPrimitiveRoot ζ ↑3<VAR>u : (𝓞 K)ˣ<VAR>hcong : ∃ n, 3 ∣ ↑u - ↑n<VAR>hζ : IsPrimitiveRoot (zeta 3 ℚ K) ↑3<VAR>this : u ∈ [1, -1, ⋯.unit, -⋯.unit, ⋯.unit ^ 2, -⋯.unit ^ 2]<GOAL>u = 1 ∨ u = -1
<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>α : Type u_4<VAR>inst✝ : Infinite α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<GOAL>∑' (x : α), c = ⊤
<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>α : Type u_4<VAR>inst✝ : Infinite α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))<GOAL>∑' (x : α), c = ⊤
<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>α : Type u_4<VAR>inst✝ : Infinite α<VAR>c : ℝ≥0∞<VAR>hc : c ≠ 0<VAR>A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))<VAR>B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c<GOAL>∑' (x : α), c = ⊤
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>(o.kahler x) ((o.rotation θ) y) = ↑θ.expMapCircle * (o.kahler x) y
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>θ : Real.Angle<GOAL>↑θ.cos * (o.kahler x) y + ↑θ.sin * (I * (o.kahler x) y) = (↑θ.cos + ↑θ.sin * I) * (o.kahler x) y
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : MonoidalCategory C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>inst✝ : MonoidalCategory D<VAR>F : OplaxMonoidalFunctor C D<VAR>X : C<GOAL>F.δ X (𝟙_ C) ≫ F.obj X ◁ F.η ≫ (ρ_ (F.obj X)).hom = F.map (ρ_ X).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>a • b ≤ 0 ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a✝ a₁ a₂ : α<VAR>b✝ b₁ b₂ : β<VAR>inst✝³ : LinearOrderedRing α<VAR>inst✝² : LinearOrderedAddCommGroup β<VAR>inst✝¹ : Module α β<VAR>inst✝ : PosSMulStrictMono α β<VAR>a : α<VAR>b : β<GOAL>(0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<GOAL>a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : b < 0<GOAL>a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a c d : α<VAR>n : ℤ<GOAL>a / 0 < 1 ↔ 0 < 0 ∧ a < 0 ∨ 0 = 0 ∨ 0 < 0 ∧ 0 < a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hb : 0 < b<GOAL>a / b < 1 ↔ 0 < b ∧ a < b ∨ b = 0 ∨ b < 0 ∧ b < a
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace α<GOAL>AnalyticSet ∅
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : TopologicalSpace α<GOAL>∅ = ∅ ∨ ∃ f, Continuous f ∧ range f = ∅
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis (range fun i => ↑i)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>hb' : b = range fun i => ↑i<GOAL>∃ s, U = ⋃₀ (Subtype.val '' ↑s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis (range fun i => ↑i)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>hb' : b = range fun i => ↑i<VAR>s : Set ↑b<VAR>hs : s.Finite<VAR>hU : U = ⋃ i ∈ s, ↑i<GOAL>∃ s, U = ⋃₀ (Subtype.val '' ↑s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis (range fun i => ↑i)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>hb' : b = range fun i => ↑i<VAR>s : Set ↑b<VAR>hs : s.Finite<VAR>hU : U = ⋃ i ∈ s, ↑i<VAR>this : Finite ↑s<VAR>x✝ : Fintype ↑s := Fintype.ofFinite ↑s<GOAL>∃ s, U = ⋃₀ (Subtype.val '' ↑s)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>b : Set (Set X)<VAR>hb : IsTopologicalBasis (range fun i => ↑i)<VAR>U : Set X<VAR>hUc : IsCompact U<VAR>hUo : IsOpen U<VAR>hb' : b = range fun i => ↑i<VAR>s : Set ↑b<VAR>hs : s.Finite<VAR>hU : U = ⋃ i ∈ s, ↑i<VAR>this : Finite ↑s<VAR>x✝ : Fintype ↑s := Fintype.ofFinite ↑s<GOAL>U = ⋃₀ (Subtype.val '' ↑s.toFinset)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<VAR>a : ℝ<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>hxa : x < a<VAR>hay : a < y<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : DifferentiableOn ℝ f (interior D)<VAR>hf'_mono : MonotoneOn (deriv f) (interior D)<VAR>x y z : ℝ<VAR>hx : x ∈ D<VAR>hz : z ∈ D<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hxzD : Icc x z ⊆ D<VAR>hxyD : Icc x y ⊆ D<VAR>hxyD' : Ioo x y ⊆ interior D<VAR>hyzD : Icc y z ⊆ D<VAR>hyzD' : Ioo y z ⊆ interior D<VAR>a : ℝ<VAR>ha : deriv f a = (f y - f x) / (y - x)<VAR>hxa : x < a<VAR>hay : a < y<VAR>b : ℝ<VAR>hb : deriv f b = (f z - f y) / (z - y)<VAR>hyb : y < b<VAR>hbz : b < z<GOAL>(f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
<VAR>α : Type u_1<VAR>f : Filter α<VAR>inst✝ : CountableInterFilter f<VAR>u v : α → ℝ≥0∞<GOAL>limsup (u * v) f ≤ limsup (fun x => limsup u f * v x) f
<VAR>α : Type u_1<VAR>f : Filter α<VAR>inst✝ : CountableInterFilter f<VAR>u v : α → ℝ≥0∞<GOAL>u * v ≤ᶠ[f] fun x => limsup u f * v x
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>W : MorphismProperty C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>D' : Type u₃<VAR>inst✝² : Category.{v₃, u₃} D'<VAR>X Y Z T : C<VAR>inst✝¹ : HasSmallLocalizedHom W X Y<VAR>inst✝ : HasSmallLocalizedHom W X X<VAR>α : SmallHom W X Y<GOAL>(equiv W W.Q) ((mk W (𝟙 X)).comp α) = (equiv W W.Q) α
<VAR>a b : Cardinal.{u_1}<VAR>hb : ℵ₀ ≤ b<VAR>ha : a ≤ b<VAR>ha' : a ≠ 0<GOAL>a * b = b
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>Odd (a + (a + 1))
<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>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x✝ : M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<GOAL>UniqueMDiffOn 𝓘(𝕜, E) ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' s)
<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>inst✝⁶ : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝⁵ : NormedAddCommGroup E'<VAR>inst✝⁴ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝³ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : SmoothManifoldWithCorners I' M'<VAR>s : Set M<VAR>x✝ : M<VAR>hs : UniqueMDiffOn I s<VAR>x : M<GOAL>UniqueMDiffOn 𝓘(𝕜, E) (↑(extChartAt I x) '' (s ∩ (chartAt H x).source))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>U V : Opens α<VAR>i : U ≤ V<GOAL>IsOpen (range (inclusion ⋯))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>U V : Opens α<VAR>i : U ≤ V<GOAL>IsOpen {x | ↑x ∈ ↑U}
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : DecidableEq α<VAR>σ : Perm α<VAR>h : σ.IsThreeCycle<GOAL>σ.IsCycle
<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 : α<GOAL>(∀ (a b c : α), c ∈ [[a, b]] → f c ∈ [[f a, f b]]) → Monotone f ∨ Antitone f
<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 : α<GOAL>¬Monotone f ∧ ¬Antitone f → ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
<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 : α<GOAL>(∃ a b c, a ≤ b ∧ b ≤ c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) → ∃ a b, ∃ c ∈ [[a, b]], f c ∉ [[f a, f b]]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<GOAL>s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>c : β → α<VAR>h : range c ∈ f<VAR>W : Set β<VAR>W_in : W ∈ comap c f<GOAL>c '' W ∈ f
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f✝ f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>c : β → α<VAR>h : range c ∈ f<VAR>W : Set β<VAR>W_in : W ∈ comap c f<GOAL>c '' W ∈ map c (comap c f)
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<GOAL>∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ<GOAL>∫ (x : α) in s, |(μ[f|m]) x| ∂μ ≤ ∫ (x : α) in s, |f x| ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ<GOAL>∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ ≤ ∫ (x : α), s.indicator (fun x => |f x|) x ∂μ
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>f : α → ℝ<VAR>hnm : m ≤ m0<VAR>hfint : Integrable f μ<VAR>this : ∫ (x : α) in s, |(μ[f|m]) x| ∂μ = ∫ (x : α), |(μ[s.indicator f|m]) x| ∂μ<VAR>x : α<GOAL>(fun x => |s.indicator f x|) x = s.indicator (fun x => |f x|) x
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊔ b - c ⊔ d‖ ≤ ‖a - c‖ + ‖b - d‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>‖a ⊔ b - c ⊔ d‖ ≤ ‖|a - c|‖ + ‖|b - d|‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>|a ⊔ b - c ⊔ d| ≤ ||a - c| + |b - d||
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>a b c d : α<GOAL>|a ⊔ b - c ⊔ d| ≤ |a - c| + |b - d|
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>H : Subgroup G<VAR>A : Type u_2<VAR>inst✝¹ : CommGroup A<VAR>ϕ : ↥H →* A<VAR>R S T : ↑(leftTransversals ↑H)<VAR>inst✝ : H.FiniteIndex<VAR>g : G<VAR>x✝¹ : Fintype (G ⧸ H) := H.fintypeQuotientOfFiniteIndex<VAR>x✝ : G ⧸ H<GOAL>ϕ ⟨(↑((MemLeftTransversals.toEquiv ⋯) x✝))⁻¹ * ↑((MemLeftTransversals.toEquiv ⋯) x✝), ⋯⟩ = ϕ ⟨(↑((MemLeftTransversals.toEquiv ⋯) ((Equiv.symm (toPerm g)) x✝)))⁻¹ * ↑((MemLeftTransversals.toEquiv ⋯) ((Equiv.symm (toPerm g)) x✝)), ⋯⟩
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>(p.smash q h).toFun (Fin.natAdd p.length i).castSucc = q.toFun i.castSucc
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>q.toFun ⟨↑(Fin.natAdd p.length i).castSucc - p.length, ⋯⟩ = q.toFun i.castSucc
<VAR>α : Type u_1<VAR>r : Rel α α<VAR>β : Type u_2<VAR>s : Rel β β<VAR>p q : RelSeries r<VAR>h : p.last = q.head<VAR>i : Fin q.length<GOAL>↑(Fin.natAdd p.length i).castSucc - p.length = ↑i
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>inst✝ : DecidableEq α<VAR>s t : Multiset α<VAR>a : α<VAR>n : ℕ<VAR>i : α<GOAL>count i (replicate n a) = (DFinsupp.single a n) i
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : AddGroup A<VAR>inst✝² : Ring R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : MulAction α β<VAR>b : β<VAR>k : ℤ<GOAL>(orbitZPowersEquiv a b).symm ↑k = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
<VAR>n : ℕ<VAR>A : Type u_1<VAR>R : Type u_2<VAR>inst✝³ : AddGroup A<VAR>inst✝² : Ring R<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : Group α<VAR>a : α<VAR>inst✝ : MulAction α β<VAR>b : β<VAR>k : ℤ<GOAL>⟨a, ⋯⟩ ^ (k % ↑(minimalPeriod (fun x => a • x) b)) • ⟨b, ⋯⟩ = ⟨a, ⋯⟩ ^ k • ⟨b, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>hF : IsOpen F<GOAL>IsOpen (connectedComponentIn F x)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>hF : IsOpen F<GOAL>∀ x_1 ∈ connectedComponentIn F x, connectedComponentIn F x ∈ 𝓝 x_1
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>hF : IsOpen F<VAR>y : α<VAR>hy : y ∈ connectedComponentIn F x<GOAL>connectedComponentIn F x ∈ 𝓝 y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝¹ : TopologicalSpace α<VAR>s t u v : Set α<VAR>inst✝ : LocallyConnectedSpace α<VAR>F : Set α<VAR>x : α<VAR>hF : IsOpen F<VAR>y : α<VAR>hy : y ∈ connectedComponentIn F x<GOAL>connectedComponentIn F y ∈ 𝓝 y
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>L : Filter F<VAR>c : 𝕜<GOAL>∇ (fun x => c) x = 0
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>n : ℕ<VAR>ha : a ≠ 0<GOAL>(C a * X ^ n).trailingDegree = ↑n
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b ≠ 0<GOAL>P.toPoly.leadingCoeff = P.b
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>(adjoinRootXPowSubCEquiv hζ H hα).symm α = root (X ^ n - C a)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<GOAL>(adjoinRootXPowSubCEquiv hζ H hα) ((adjoinRootXPowSubCEquiv hζ H hα).symm α) = (adjoinRootXPowSubCEquiv hζ H hα) (root (X ^ n - C a))