ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<VAR>a : ↥S<VAR>ha : a • x' = a • S.subtype y • x<GOAL>(a * y) • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<VAR>a : ↥S<VAR>ha : a • x' = a • S.subtype y • x<GOAL>(a * y) • x = ↑a • x'
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<VAR>a : ↥S<VAR>ha : a • x' = a • S.subtype y • x<GOAL>(a * y) • x = a • S.subtype y • x
<VAR>R : Type u_1<VAR>inst✝⁶ : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommMonoid M<VAR>inst✝⁴ : Module R M<VAR>M' : Type u_3<VAR>inst✝³ : AddCommMonoid M'<VAR>inst✝² : Module R M'<VAR>f : M →ₗ[R] M'<VAR>inst✝¹ : IsLocalizedModule S f<VAR>inst✝ : DecidableEq M<VAR>x : M<VAR>s : Finset M'<VAR>y : ↥S := commonDenomOfFinset S f s<VAR>hx₁ : ↑y • Submodule.span R ↑s = Submodule.span R (⇑f '' ↑(finsetIntegerMultiple S f s))<VAR>x' : M<VAR>hx' : x' ∈ ↑(Submodule.span R ↑(finsetIntegerMultiple S f s))<VAR>hx'' : f x' = f (S.subtype y • x)<VAR>a : ↥S<VAR>ha : a • x' = a • S.subtype y • x<GOAL>↑(a * y) • x = ↑a • ↑y • x
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>z : M<GOAL>z ∈ center M ↔ ∀ (g : M), g * z = z * g
<VAR>M : Type u_1<VAR>inst✝ : Semigroup M<VAR>z : M<GOAL>z ∈ center M ↔ z ∈ Set.center M
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(derivative p).coeff n = p.coeff (n + 1) * (↑n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p.sum fun n a => C (a * ↑n) * X ^ (n - 1)).coeff n = p.coeff (n + 1) * (↑n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p.sum fun a b => b * ↑a * if n = a - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>(p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = p.coeff (n + 1) * (↑n + 1)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>∀ b ∈ p.support, b ≠ n + 1 → (p.coeff b * ↑b * if n = b - 1 then 1 else 0) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p : R[X]<VAR>n : ℕ<GOAL>n + 1 ∉ p.support → (p.coeff (n + 1) * ↑(n + 1) * if n = n + 1 - 1 then 1 else 0) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>this : IsSFiniteKernel ρCond<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ρ ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>this : IsSFiniteKernel ρCond<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * (ρ.fst ⊗ₘ ρCond) ({x} ×ˢ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>Ω : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mΩ : MeasurableSpace Ω<VAR>ρ : Measure (α × Ω)<VAR>inst✝² : IsFiniteMeasure ρ<VAR>ρCond : Kernel α Ω<VAR>inst✝¹ : ρ.IsCondKernel ρCond<VAR>inst✝ : MeasurableSingletonClass α<VAR>x : α<VAR>hx : ρ.fst {x} ≠ 0<VAR>s : Set Ω<VAR>hs : MeasurableSet s<VAR>this : IsSFiniteKernel ρCond<GOAL>(ρCond x) s = (ρ.fst {x})⁻¹ * ∫⁻ (a : α), (ρCond a) (Prod.mk a ⁻¹' {x} ×ˢ s) ∂ρ.fst
<VAR>α : Type u_1<VAR>inst✝ : AddCommMonoid α<VAR>n₁ : ℕ<VAR>x a₁ : α<VAR>n₂ : ℕ<VAR>a₂ : α<VAR>n' : ℕ<VAR>a' : α<VAR>h₁ : n₁ + n₂ = n'<VAR>h₂ : a₁ + a₂ = a'<GOAL>term n₁ x a₁ + term n₂ x a₂ = term n' x a'
<VAR>n✝ n : ℕ<GOAL>n.divisors.sup id = n
<VAR>n✝ n : ℕ<GOAL>n ≤ n.divisors.sup id
<VAR>n : ℕ<GOAL>0 ≤ (divisors 0).sup id
<VAR>n✝ n : ℕ<VAR>hn : n ≠ 0<GOAL>n ≤ n.divisors.sup id
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : LE α<VAR>S : Set (UpperSet α)<VAR>s t : UpperSet α<VAR>a : α<GOAL>(∃ i, ∃ (_ : i ∈ S), a ∈ ↑i) ↔ ∃ s ∈ S, a ∈ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hμ : μ ≠ 0<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h : ∀ᵐ (x : α) ∂μ, f x < g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hμ : ¬μ univ = 0<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h : ∀ᵐ (x : α) ∂μ, f x < g x<GOAL>∫⁻ (x : α), f x ∂μ < ∫⁻ (x : α), g x ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f g : α → ℝ≥0∞<VAR>hμ : ¬μ univ = 0<VAR>hg : AEMeasurable g μ<VAR>hfi : ∫⁻ (x : α), f x ∂μ ≠ ⊤<VAR>h : ∀ᵐ (x : α) ∂μ, f x < g x<GOAL>∀ᵐ (x : α) ∂μ, x ∈ univ → f x < g x
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hω : ¬IsSuccLimit (⨆ i, f i)<GOAL>∃ i, f i = ⨆ i, f i
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hω : ¬IsSuccLimit (⨆ i, f i)<GOAL>BddAbove (range f)
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hf : ¬BddAbove (range f)<GOAL>IsSuccLimit (⨆ i, f i)
<VAR>α β ι : Type u<VAR>f : ι → Cardinal.{v}<VAR>hf : ¬BddAbove (range f)<GOAL>IsSuccLimit ⊥
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set X<VAR>h : X ≃ₜ Y<VAR>x : X<VAR>hx : x ∈ s<GOAL>⇑h '' connectedComponentIn s x = connectedComponentIn (⇑h '' s) (h x)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set X<VAR>h : X ≃ₜ Y<VAR>x : X<VAR>hx : x ∈ s<GOAL>connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>X' : Type u_4<VAR>Y' : Type u_5<VAR>inst✝¹ : TopologicalSpace X'<VAR>inst✝ : TopologicalSpace Y'<VAR>s : Set X<VAR>h : X ≃ₜ Y<VAR>x : X<VAR>hx : x ∈ s<VAR>this : ⇑h.symm '' connectedComponentIn (⇑h '' s) (h x) ⊆ connectedComponentIn (⇑h.symm '' (⇑h '' s)) (h.symm (h x))<GOAL>connectedComponentIn (⇑h '' s) (h x) ⊆ ⇑h '' connectedComponentIn s x
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>c : R<VAR>f : RingSeminorm R<VAR>hf1 : f 1 ≤ 1<VAR>hc : f c ≠ 0<VAR>hpm : IsPowMul ⇑f<VAR>x : R<VAR>hx : ∀ (y : R), f (x * y) = f x * f y<VAR>hseq : seminormFromConst_seq c f x = fun _n => f x<GOAL>Tendsto (fun _n => f x) atTop (𝓝 (f x))
<VAR>n : ℕ<GOAL>2 ∣ (n + 1).centralBinom
<VAR>n : ℕ<GOAL>(n + 1).centralBinom = 2 * (n + 1 + n).choose n
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<VAR>hz : 0 ∈ p.coeffs<GOAL>False
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q p : MvPolynomial σ R<VAR>hz : 0 ∈ p.coeffs<VAR>n : σ →₀ ℕ<VAR>hnsupp : n ∈ p.support<VAR>hn : 0 = coeff n p<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hf_meas : StronglyMeasurable f<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hft_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ this : SigmaFinite (μ.restrict t)<VAR>S : ℕ → Set α := spanningSets (μ.restrict t)<GOAL>FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hf_meas : StronglyMeasurable f<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hft_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ this : SigmaFinite (μ.restrict t)<VAR>S : ℕ → Set α := spanningSets (μ.restrict t)<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<GOAL>FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hf_meas : StronglyMeasurable f<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hft_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ this : SigmaFinite (μ.restrict t)<VAR>S : ℕ → Set α := spanningSets (μ.restrict t)<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<VAR>f_approx : ℕ → α →ₛ β := hf_meas.approx<VAR>fs : ℕ → α →ₛ β := fun n => (f_approx n).restrict (S n ∩ t)<GOAL>FinStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f g : α → β<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : Zero β<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hf_meas : StronglyMeasurable f<VAR>t : Set α<VAR>ht : MeasurableSet t<VAR>hft_zero : ∀ x ∈ tᶜ, f x = 0<VAR>htμ this : SigmaFinite (μ.restrict t)<VAR>S : ℕ → Set α := spanningSets (μ.restrict t)<VAR>hS_meas : ∀ (n : ℕ), MeasurableSet (S n)<VAR>f_approx : ℕ → α →ₛ β := hf_meas.approx<VAR>fs : ℕ → α →ₛ β := fun n => (f_approx n).restrict (S n ∩ t)<VAR>h_fs_t_compl : ∀ (n : ℕ), ∀ x ∉ t, ↑(fs n) x = 0<GOAL>FinStronglyMeasurable f μ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁸ : OrderedCommRing R<VAR>inst✝¹⁷ : Nontrivial R<VAR>inst✝¹⁶ : StarRing R<VAR>inst✝¹⁵ : StarOrderedRing R<VAR>inst✝¹⁴ : MetricSpace R<VAR>inst✝¹³ : TopologicalRing R<VAR>inst✝¹² : ContinuousStar R<VAR>inst✝¹¹ : ∀ (α : Type ?u.1260451) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀<VAR>inst✝¹⁰ : TopologicalSpace A<VAR>inst✝⁹ : NonUnitalRing A<VAR>inst✝⁸ : StarRing A<VAR>inst✝⁷ : PartialOrder A<VAR>inst✝⁶ : StarOrderedRing A<VAR>inst✝⁵ : Module R A<VAR>inst✝⁴ : IsScalarTower R A A<VAR>inst✝³ : SMulCommClass R A A<VAR>inst✝² : StarModule R A<VAR>inst✝¹ : NonUnitalContinuousFunctionalCalculus R p<VAR>inst✝ : NonnegSpectrumClass R A<VAR>a : A<VAR>ha : p a<VAR>f g : C(↑(σₙ R a), R)₀<GOAL>(cfcₙHom ha) f ≤ (cfcₙHom ha) g ↔ f ≤ g
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<GOAL>x - x ^ 3 / 4 < sin x
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<GOAL>x - x ^ 3 / 4 < sin x
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : -(|x| ^ 4 * (5 / 96)) ≤ sin x - (x - x ^ 3 / 6)<GOAL>x - x ^ 3 / 4 < sin x
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<GOAL>x - x ^ 3 / 4 < sin x
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<GOAL>x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<VAR>this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹<GOAL>x - x ^ 3 / 4 < -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6)
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<VAR>this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹<GOAL>x ^ 4 * (5 / 96) < x ^ 3 * 12⁻¹
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<VAR>this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹<GOAL>x ^ 4 ≤ x ^ 3
<VAR>x✝ x : ℝ<VAR>h : 0 < x<VAR>h' : x ≤ 1<VAR>hx : |x| = x<VAR>this✝ : -(x ^ 4 * (5 / 96)) + (x - x ^ 3 / 6) ≤ sin x<VAR>this : x ^ 3 / 4 - x ^ 3 / 6 = x ^ 3 * 12⁻¹<GOAL>3 ≤ 4
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : Z.Fiber b<GOAL>(Trivialization.continuousLinearMapAt R (Z.localTriv i) b) v = (Z.coordChange (Z.indexAt b) i b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : Z.Fiber b<GOAL>(fun y => (↑(Z.localTriv i) { proj := b, snd := y }).2) v = (Z.coordChange (Z.indexAt b) i b) v
<VAR>R : Type u_1<VAR>B : Type u_2<VAR>F : Type u_3<VAR>E : B → Type u_4<VAR>inst✝⁸ : NontriviallyNormedField R<VAR>inst✝⁷ : (x : B) → AddCommMonoid (E x)<VAR>inst✝⁶ : (x : B) → Module R (E x)<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace R F<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹ : (x : B) → TopologicalSpace (E x)<VAR>inst✝ : FiberBundle F E<VAR>ι : Type u_5<VAR>Z : VectorBundleCore R B F ι<VAR>b✝ : B<VAR>a : F<VAR>i j : ι<VAR>b : B<VAR>hb : b ∈ Z.baseSet i<VAR>v : Z.Fiber b<GOAL>b ∈ (Z.localTriv i).baseSet
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<GOAL>A ∈ unitaryGroup n α ↔ star A * A = 1
<VAR>n : Type u<VAR>inst✝³ : DecidableEq n<VAR>inst✝² : Fintype n<VAR>α : Type v<VAR>inst✝¹ : CommRing α<VAR>inst✝ : StarRing α<VAR>A : Matrix n n α<VAR>hA : star A * A = 1<GOAL>A * star A = 1
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>inst✝ : IsIrrefl α r<VAR>s : Multiset α<GOAL>¬CutExpand r s 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ≠ x<GOAL>x ∈ l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : DecidableEq α<VAR>l✝ : List α<VAR>x✝ : α<VAR>l : List α<VAR>x : α<VAR>h : l.formPerm x ≠ x<GOAL>x ∈ {y | l.formPerm y ≠ y}
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<VAR>H₁ H₂ H₃ K₁ K₂ : Subgroup G<GOAL>⁅H₁, H₂⁆ = ⊥ ↔ H₁ ≤ centralizer ↑H₂
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<VAR>H₁ H₂ H₃ K₁ K₂ : Subgroup G<GOAL>(∀ g₁ ∈ H₁, ∀ g₂ ∈ H₂, ⁅g₁, g₂⁆ ∈ ⊥) ↔ H₁ ≤ centralizer ↑H₂
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : FunLike F G G'<VAR>inst✝ : MonoidHomClass F G G'<VAR>f : F<VAR>g₁ g₂ g₃ g : G<VAR>H₁ H₂ H₃ K₁ K₂ : Subgroup G<VAR>p : G<VAR>_hp : p ∈ H₁<VAR>q : G<VAR>hq : q ∈ H₂<GOAL>⁅p, q⁆ ∈ ⊥ ↔ q * p = p * q
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q f : R[X]<VAR>hf : f ≠ 0<VAR>hfR : ↑f.natDegree < #R<GOAL>∃ r, eval r f ≠ 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q f : R[X]<VAR>hfR : ↑f.natDegree < #R<VAR>hf : ∀ (r : R), eval r f = 0<GOAL>f = 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>ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>f : α → E<VAR>hf : Integrable f μ<GOAL>∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a
<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>ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>f : α → E<VAR>hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)<GOAL>∫ (a : α), f a ∂μ = ∑' (a : α), (μ {a}).toReal • f a
<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>ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>f : α → E<VAR>hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)<GOAL>∑' (i : α), ∫ (a : α), f a ∂μ {i} • Measure.dirac i = ∑' (a : α), ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a
<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>ν : Measure α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<VAR>f : α → E<VAR>hf : Integrable f (Measure.sum fun a => μ {a} • Measure.dirac a)<VAR>a : α<GOAL>∫ (a : α), f a ∂μ {a} • Measure.dirac a = ((Measure.sum fun a => μ {a} • Measure.dirac a) {a}).toReal • f a
<VAR>m n : ℕ<GOAL>(m + n).gcd n = m.gcd 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∞<VAR>r : ℝ≥0∞<GOAL>HasSum f r ↔ Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)
<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∞<VAR>r : ℝ≥0∞<VAR>h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)<GOAL>HasSum f r
<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∞<VAR>r : ℝ≥0∞<VAR>h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)<GOAL>HasSum f (∑' (i : ℕ), f i)
<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∞<VAR>r : ℝ≥0∞<VAR>h : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop (𝓝 r)<GOAL>Monotone fun n => ∑ i ∈ Finset.range n, f i
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x / ↑m)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>Irrational (x / ↑↑m)
<VAR>q : ℚ<VAR>x y : ℝ<VAR>h : Irrational x<VAR>m : ℤ<VAR>hm : m ≠ 0<GOAL>↑m ≠ 0
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x x' y : M<GOAL>polar (⇑Q) (x - x') y = polar (⇑Q) x y - polar (⇑Q) x' y
<GOAL>-π < -π / 2 ∧ -π / 2 ≤ π
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : MulOneClass G<VAR>f : MonoidAlgebra k G<VAR>r : k<VAR>x a : G<GOAL>a * 1 = x ↔ a = x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<GOAL>DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f : 𝕜 → E<VAR>a b : 𝕜<VAR>s : Set 𝕜<VAR>h : b ≠ a<VAR>hd : DifferentiableWithinAt 𝕜 f s b<GOAL>DifferentiableWithinAt 𝕜 (dslope f a) s b