ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π✝ : TaggedPrepartition I<VAR>c : ℝ<VAR>f : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>π : TaggedPrepartition I<GOAL>integralSum (c • f) vol π = c • integralSum f vol π
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrderedField α<VAR>a b : CauSeq α abs<VAR>h : a ≤ b<GOAL>a ⊓ b ≈ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>p✝ : α → Prop<VAR>f✝ : (a : α) → p✝ a → β<VAR>x✝ : Option α<VAR>p : α → Prop<VAR>f : α → β<VAR>x : Option α<VAR>H : ∀ (a : α), a ∈ x → p a<GOAL>pmap (fun a x => f a) x H = Option.map f x
<VAR>k : ℕ<VAR>hk : k ≠ 1<GOAL>bernoulliFun k 1 = bernoulliFun k 0
<VAR>X : Type w<VAR>inst✝ : TopologicalSpace X<VAR>Y : Type u_1<VAR>t : TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)<GOAL>Continuous f
<VAR>X : Type w<VAR>inst✝ : TopologicalSpace X<VAR>Y : Type u_1<VAR>t : TopologicalSpace Y<VAR>f : X → Y<VAR>h : ∀ (S : CompHaus) (g : C(↑S.toTop, X)), Continuous (f ∘ ⇑g)<GOAL>Continuous (f ∘ fun x => match x with | ⟨⟨fst, i⟩, s⟩ => i s)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>map (LinearMap.snd R M M₂) (snd R M M₂) = ⊤
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<GOAL>⊤ ≤ map (LinearMap.snd R M M₂) (snd R M M₂)
<VAR>R : Type u<VAR>K : Type u'<VAR>M : Type v<VAR>V : Type v'<VAR>M₂ : Type w<VAR>V₂ : Type w'<VAR>M₃ : Type y<VAR>V₃ : Type y'<VAR>M₄ : Type z<VAR>ι : Type x<VAR>M₅ : Type u_1<VAR>M₆ : Type u_2<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : AddCommMonoid M₂<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R M₂<VAR>p : Submodule R M<VAR>q : Submodule R M₂<VAR>x : M₂<GOAL>x ∈ map (LinearMap.snd R M M₂) (snd R M M₂)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l : List M<VAR>ha : a ∈ l<GOAL>a ∣ l.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l : List M<VAR>ha : a ∈ l<VAR>s t : List M<VAR>h : l = s ++ a :: t<GOAL>a ∣ l.prod
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝ : CommMonoid M<VAR>a : M<VAR>l : List M<VAR>ha : a ∈ l<VAR>s t : List M<VAR>h : l = s ++ a :: t<GOAL>a ∣ a * (s.prod * t.prod)
<VAR>b x : Ordinal.{u_1}<VAR>hx : x = 0<GOAL>log b x ≤ x
<VAR>b x : Ordinal.{u_1}<VAR>hx : ¬x = 0<VAR>hb : ¬1 < b<GOAL>log b x ≤ x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : QuasiSober α<VAR>inst✝ : IrreducibleSpace α<GOAL>IsGenericPoint (genericPoint α) ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1<GOAL>∃ x ∈ s, f x ≠ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>M : Type u_5<VAR>N : Type u_6<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommMonoid N<VAR>f g : α → M<VAR>a b : α<VAR>s t : Set α<VAR>h : ∏ᶠ (i : α) (_ : i ∈ s), f i ≠ 1<VAR>h' : ∀ x ∈ s, f x = 1<GOAL>False
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>w : List T<GOAL>w ∈ g.language ↔ g.Derives [Symbol.nonterminal g.initial] (List.map Symbol.terminal w)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(descPochhammer ℤ n).smeval r = n.factorial • choose r n
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<GOAL>(ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
<VAR>R : Type u_1<VAR>inst✝³ : NonAssocRing R<VAR>inst✝² : Pow R ℕ<VAR>inst✝¹ : BinomialRing R<VAR>inst✝ : NatPowAssoc R<VAR>r : R<VAR>n : ℕ<VAR>h : (1 - ↑n).smeval r = 1 - ↑n<GOAL>(ascPochhammer ℤ n).smeval (r + (1 - ↑n).smeval r) = (ascPochhammer ℕ n).smeval (r - ↑n + 1)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>R : ℝ<VAR>hF : CompleteSpace F<GOAL>∫ (x : E), f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>hF : CompleteSpace F<GOAL>∫ (x : E), f (0 • x) ∂μ = |(0 ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : MeasurableSpace E<VAR>inst✝⁴ : BorelSpace E<VAR>inst✝³ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝² : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>s : Set E<VAR>f : E → F<VAR>R : ℝ<VAR>hF : CompleteSpace F<VAR>hR : R ≠ 0<GOAL>∫ (x : E), f (R • x) ∂μ = |(R ^ finrank ℝ E)⁻¹| • ∫ (x : E), f x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>s.encard ≤ 1 ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>(s.Nonempty → ∃ x, s = {x}) ↔ ∀ (a b : α), a ∈ s → b ∈ s → a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>h : s.Nonempty → ∃ x, s = {x}<VAR>a b : α<VAR>has : a ∈ s<VAR>hbs : b ∈ s<GOAL>a = b
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>c : ℝ<GOAL>(normAtPlace w) (c • x) = |c| * (normAtPlace w) x
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>w : InfinitePlace K<VAR>x : ({ w // w.IsReal } → ℝ) × ({ w // w.IsComplex } → ℂ)<VAR>c : ℝ<GOAL>(if hw : w.IsReal then ‖(c • x).1 ⟨w, hw⟩‖ else ‖(c • x).2 ⟨w, ⋯⟩‖) = |c| * if hw : w.IsReal then ‖x.1 ⟨w, hw⟩‖ else ‖x.2 ⟨w, ⋯⟩‖
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
<VAR>n : ZMod 0<GOAL>IsUnit n ↔ Int.natAbs n = 1
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<GOAL>legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>h : p = q<GOAL>legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
<VAR>p q : ℕ<VAR>inst✝¹ : Fact (Nat.Prime p)<VAR>inst✝ : Fact (Nat.Prime q)<VAR>hp : p ≠ 2<VAR>hq : q ≠ 2<VAR>h : p ≠ q<GOAL>legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasEqualizer f g<VAR>inst✝ : HasEqualizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = h ≫ g<GOAL>G.map h ≫ G.map f = G.map h ≫ G.map g
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasEqualizer f g<VAR>inst✝ : HasEqualizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = h ≫ g<GOAL>G.map (equalizer.lift h w) ≫ equalizerComparison f g G = equalizer.lift (G.map h) ⋯
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>inst✝¹ : HasEqualizer f g<VAR>inst✝ : HasEqualizer (G.map f) (G.map g)<VAR>Z : C<VAR>h : Z ⟶ X<VAR>w : h ≫ f = h ≫ g<GOAL>(G.map (equalizer.lift h w) ≫ equalizerComparison f g G) ≫ equalizer.ι (G.map f) (G.map g) = equalizer.lift (G.map h) ⋯ ≫ equalizer.ι (G.map f) (G.map g)
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝² inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>φ ψ : MvPolynomial σ R<VAR>m n : ℕ<VAR>hφ : φ.IsHomogeneous m<VAR>r : R<GOAL>(C r * φ).IsHomogeneous m
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x✝ y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<VAR>x : P<GOAL>x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>x✝ y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>x : P<VAR>hy : y ≠ x<GOAL>x ∈ inversion x R ⁻¹' sphere y (dist y x) ↔ x ∈ insert x ↑(perpBisector x (inversion x R y))
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c x✝ y : P<VAR>R : ℝ<VAR>hR : R ≠ 0<VAR>hy : y ≠ c<VAR>x : P<VAR>hx : x ≠ c<GOAL>x ∈ inversion c R ⁻¹' sphere y (dist y c) ↔ x ∈ insert c ↑(perpBisector c (inversion c R y))
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>ι : Type w<VAR>h : Basis ι R M<GOAL>↑(finrank R M) = #ι
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝⁴ : Ring R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>ι✝ : Type w<VAR>ι' : Type w'<VAR>inst✝¹ : StrongRankCondition R<VAR>inst✝ : Module.Finite R M<VAR>ι : Type w<VAR>h : Basis ι R M<VAR>val✝ : Fintype ι<GOAL>↑(finrank R M) = #ι
<VAR>R : Type u_1<VAR>M₁ : Type u_2<VAR>M₂ : Type u_3<VAR>ι₁ : Type u_4<VAR>ι₂ : Type u_5<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : AddCommGroup M₂<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : Module R M₂<VAR>inst✝² : Fintype ι₁<VAR>inst✝¹ : Finite ι₂<VAR>inst✝ : DecidableEq ι₁<VAR>b₁ : Basis ι₁ R M₁<VAR>b₂ : Basis ι₂ R M₂<GOAL>(fun i => ((toMatrix b₁ b₁) id).toMvPolynomial i) = X
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝⁵ : CommSemiring R<VAR>inst✝⁴ : StarRing R<VAR>inst✝³ : Semiring A<VAR>inst✝² : StarMul A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : StarModule R A<VAR>r : R<VAR>hr : IsSelfAdjoint r<GOAL>IsSelfAdjoint ((algebraMap R A) r)
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M ≃ₗ[R] M'<GOAL>lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M ≃ₗ[R] M'<GOAL>lift.{v', v} (Module.rank R M) ≤ lift.{v, v'} (Module.rank R M')
<VAR>R : Type u<VAR>R' : Type u'<VAR>M M₁ : Type v<VAR>M' : Type v'<VAR>inst✝⁹ : Ring R<VAR>inst✝⁸ : Ring R'<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M'<VAR>inst✝⁵ : AddCommGroup M₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M₁<VAR>inst✝¹ : Module R' M'<VAR>inst✝ : Module R' M₁<VAR>f : M ≃ₗ[R] M'<GOAL>lift.{v, v'} (Module.rank R M') ≤ lift.{v', v} (Module.rank R M)
<VAR>x : PGame<VAR>h : 0 < x<GOAL>x⁻¹ = x.inv'
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι✝ : Sort x<VAR>f✝ g : Filter α<VAR>s t : Set α<VAR>ι : Sort w<VAR>f : ι → Filter (Filter α)<VAR>x : Set α<GOAL>x ∈ ⨆ x, (f x).join ↔ x ∈ (⨆ x, f x).join
<VAR>x✝ x : ℝ<VAR>hx : |x| ≤ π<VAR>hx₀ : 0 ≤ x<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (-(2 / π ^ 2 * (↑2 * x ^ (2 - 1))) - -sin x) x<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<VAR>hmono : MonotoneOn (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<VAR>hmono : MonotoneOn (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))<VAR>hconc : ConcaveOn ℝ (Icc (π / 2) π) fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x<GOAL>cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<VAR>hmono : MonotoneOn (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))<VAR>hconc : ConcaveOn ℝ (Icc (π / 2) π) fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x<GOAL>0 ≤ 1 - 2 / π ^ 2 * x ^ 2 - cos x
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<VAR>hmono : MonotoneOn (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))<VAR>hconc : ConcaveOn ℝ (Icc (π / 2) π) fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x<VAR>hx' : x ≤ π / 2<GOAL>0 ≤ 1 - 2 / π ^ 2 * x ^ 2 - cos x
<VAR>x✝ x : ℝ<VAR>hx : x ≤ π<VAR>hx₀ : 0 ≤ x<VAR>hderiv : ∀ (x : ℝ), HasDerivAt (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (sin x - 2 / π ^ 2 * 2 * x) x<VAR>hmono : MonotoneOn (fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x) (Icc 0 (π / 2))<VAR>hconc : ConcaveOn ℝ (Icc (π / 2) π) fun x => 1 - 2 / π ^ 2 * x ^ 2 - cos x<VAR>hx' : π / 2 ≤ x<GOAL>0 ≤ 1 - 2 / π ^ 2 * x ^ 2 - cos x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : BooleanAlgebra α<VAR>a b c d : α<GOAL>b ⇔ a ⇔ a = b
<VAR>J : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>F✝ : J ⥤ C<VAR>inst✝¹ : HasColimitsOfShape J C<VAR>G : J ⥤ C<VAR>α✝ : F✝ ⟶ G<VAR>inst✝ : HasColimitsOfShape K C<VAR>F : J ⥤ C<VAR>E₁ E₂ : K ⥤ J<VAR>α : E₁ ⟶ E₂<VAR>j✝ : K<GOAL>ι (E₁ ⋙ F) j✝ ≫ pre F E₁ = ι (E₁ ⋙ F) j✝ ≫ colim.map (whiskerRight α F) ≫ pre F E₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : LinearOrderedField α<VAR>inst✝² : Ring β<VAR>abv : β → α<VAR>inst✝¹ : IsAbsoluteValue abv<VAR>f g : ℕ → β<VAR>a✝ : ℕ → α<VAR>inst✝ : Archimedean α<VAR>a x : α<VAR>hx1 : |x| < 1<GOAL>IsCauSeq abs fun m => ∑ n ∈ range m, a * x ^ n
<VAR>x y : ℂ<VAR>hre : |x.re| ≤ |y.re|<VAR>him : |x.im| ≤ |y.im|<GOAL>normSq x ≤ normSq y
<VAR>x y : ℂ<VAR>hre : |x.re| ≤ |y.re|<VAR>him : |x.im| ≤ |y.im|<GOAL>|x.re| * |x.re| + |x.im| * |x.im| ≤ |y.re| * |y.re| + |y.im| * |y.im|
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>l₁ l₂ : List α<VAR>k : ℕ<VAR>hk : k ≤ l₂.length<GOAL>(l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>l₁ l₂ : List α<VAR>k : ℕ<VAR>hk : k ≤ l₂.reverse.length<GOAL>(l₁ ++ l₂).rdrop k = l₁ ++ l₂.rdrop k
<VAR>p : Char → Bool<VAR>l m r : List Char<VAR>acc : List String<GOAL>(if h : { data := l ++ m ++ r }.atEnd { byteIdx := utf8Len l + utf8Len m } = true then let r := { data := l ++ m ++ r }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc; r.reverse else let_fun this := ⋯; if p ({ data := l ++ m ++ r }.get { byteIdx := utf8Len l + utf8Len m }) = true then let i' := { data := l ++ m ++ r }.next { byteIdx := utf8Len l + utf8Len m }; { data := l ++ m ++ r }.splitAux p i' i' ({ data := l ++ m ++ r }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc) else { data := l ++ m ++ r }.splitAux p { byteIdx := utf8Len l } ({ data := l ++ m ++ r }.next { byteIdx := utf8Len l + utf8Len m }) acc) = acc.reverse ++ List.map mk (List.splitOnP.go p r m.reverse)
<VAR>p : Char → Bool<VAR>l m r : List Char<VAR>acc : List String<GOAL>(if r = [] then acc.reverse ++ [{ data := l ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m }] else if p ({ data := l ++ (m ++ r) }.get { byteIdx := utf8Len l + utf8Len m }) = true then { data := l ++ (m ++ r) }.splitAux p ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m }) ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m }) ({ data := l ++ (m ++ r) }.extract { byteIdx := utf8Len l } { byteIdx := utf8Len l + utf8Len m } :: acc) else { data := l ++ (m ++ r) }.splitAux p { byteIdx := utf8Len l } ({ data := l ++ (m ++ r) }.next { byteIdx := utf8Len l + utf8Len m }) acc) = acc.reverse ++ List.map mk (List.splitOnP.go p r m.reverse)
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>↑((associatesEquivIsPrincipal R) 1) = 1
<VAR>R : Type u_1<VAR>inst✝¹ : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝ : Fintype n<VAR>M : Matrix m n R<GOAL>LinearMap.range M.mulVecLin = span R (Set.range Mᵀ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>a b c d : α<VAR>hac : a ≤ c<VAR>hbd : b ≤ d<VAR>this✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>this : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<GOAL>a * b = c * d ↔ a = c ∧ b = d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<GOAL>0 < s.encard ↔ s.Nonempty
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>s : Multiset α<VAR>a : α<GOAL>0 ⊂ s ↔ s ≠ 0
<VAR>R : Type u<VAR>ι : Type w<VAR>s✝ : Finset ι<VAR>inst✝ : CommRing R<VAR>s : Finset ι<VAR>f : ι → R<VAR>hs : 0 < s.card<GOAL>(∏ i ∈ s, (X - C (f i))).coeff (s.card - 1) = -∑ i ∈ s, f i
<VAR>R : Type u1<VAR>inst✝⁵ : CommRing R<VAR>M : Type u2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>A : Type u_1<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>(ι R) x ≠ 1
<VAR>R : Type u1<VAR>inst✝⁵ : CommRing R<VAR>M : Type u2<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>A : Type u_1<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra R A<VAR>inst✝ : Nontrivial R<VAR>x : M<GOAL>¬(x = 0 ∧ 1 = 0)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : PseudoMetricSpace α<VAR>inst✝ : PseudoMetricSpace β<VAR>K : ℝ≥0<VAR>f : α → β<GOAL>(∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>s ∈ 𝓝 x ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
<VAR>α : Type ua<VAR>β : Type ub<VAR>γ : Type uc<VAR>δ : Type ud<VAR>ι : Sort u_1<VAR>inst✝ : UniformSpace α<VAR>x : α<VAR>s : Set α<GOAL>(∃ t ∈ 𝓤 α, Prod.mk x ⁻¹' t ⊆ s) ↔ ∃ V ∈ 𝓤 α, ball x V ⊆ s
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>φ ψ : ℝ → ℝ<VAR>s✝ : Set E<VAR>a b m✝ : ℝ<VAR>x y : E<VAR>f✝ g : E → ℝ<VAR>s : Set E<VAR>f : E → ℝ<VAR>m n : ℝ<GOAL>StrongConvexOn s 0 f ↔ ConvexOn ℝ s f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>g' : ↑(X.presheaf.stalk ↑x)<VAR>heq : (X.presheaf.germ x) f * g' = 1<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>heq : (X.presheaf.germ x) f * (X.presheaf.germ ⟨↑x, hxV⟩) g = 1<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>heq : (X.presheaf.germ x) f * (X.presheaf.germ ⟨↑x, hxV⟩) g = 1<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>heq : (X.presheaf.germ x) f * (X.presheaf.germ ⟨↑x, hxV⟩) g = 1<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<VAR>heq : (X.presheaf.germ ⟨↑x, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ ⟨↑x, hxW⟩) 1<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>x : ↥U<VAR>h : IsUnit ((X.presheaf.germ x) f)<VAR>V : Opens ↑↑X.toPresheafedSpace<VAR>hxV : ↑x ∈ V<VAR>g : (CategoryTheory.forget CommRingCat).obj (X.presheaf.obj (op V))<VAR>W : Opens ↑↑X.toPresheafedSpace := U ⊓ V<VAR>hxW : ↑x ∈ W<VAR>heq : (X.presheaf.germ ⟨↑x, hxW⟩) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.germ ⟨↑x, hxW⟩) 1<VAR>W' : Opens ↑↑X.toPresheafedSpace<VAR>hxW' : ↑x ∈ W'<VAR>i₁ i₂ : W' ⟶ W<VAR>heq' : (X.presheaf.map i₁.op) ((X.presheaf.map (U.infLELeft V).op) f * (X.presheaf.map (U.infLERight V).op) g) = (X.presheaf.map i₂.op) 1<GOAL>∃ V i, ∃ (_ : ↑x ∈ V), IsUnit ((X.presheaf.map i.op) f)