ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<GOAL>∀ x ∈ filter (fun x => x ≠ 0) f.range, T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ filter (fun x => x ≠ 0) f.range<GOAL>T' (↑f ⁻¹' {x}) = c • T (↑f ⁻¹' {x})
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ filter (fun x => x ≠ 0) f.range<GOAL>x ≠ 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>G : Type u_5<VAR>𝕜 : Type u_6<VAR>p : ℝ≥0∞<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace ℝ F<VAR>inst✝² : NormedAddCommGroup F'<VAR>inst✝¹ : NormedSpace ℝ F'<VAR>inst✝ : NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>T T' : Set α → E →L[ℝ] F'<VAR>c : ℝ<VAR>h_smul : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T' s = c • T s<VAR>f : α →ₛ E<VAR>hf : Integrable (↑f) μ<VAR>x : E<VAR>hx : x ∈ f.range ∧ x ≠ 0<GOAL>x ≠ 0
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>h₁ : Tendsto F l (𝓝 f)<VAR>h₂ : UniformEquicontinuous F<GOAL>UniformContinuous f
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>l : Filter ι<VAR>inst✝ : l.NeBot<VAR>F : ι → β → α<VAR>f : β → α<VAR>h₁ : ∀ (x : β), Tendsto (fun i => F i x) l (𝓝 (f x))<VAR>h₂ : UniformEquicontinuousOn F univ<GOAL>UniformContinuousOn f univ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map₂ m f (pure b) = map (fun x => m x b) f
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<GOAL>map ((fun p => m p.1 p.2) ∘ fun a => (a, b)) f = map (fun x => m x b) f
<VAR>m : ℕ<GOAL>0 < ack (m + 1) 0
<VAR>m : ℕ<GOAL>0 < ack m 1
<VAR>m n : ℕ<GOAL>0 < ack (m + 1) (n + 1)
<VAR>m n : ℕ<GOAL>0 < ack m (ack (m + 1) n)
<VAR>Δ Δ'' : SimplexCategory<VAR>φ : Δ ⟶ Δ''<VAR>e : Δ ⟶ image φ<VAR>inst✝¹ : Epi e<VAR>i : image φ ⟶ Δ''<VAR>inst✝ : Mono i<VAR>fac : e ≫ i = φ<GOAL>factorThruImage φ = e
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>hi : i0 ≤ i<GOAL>0 ≤ toZ i0 i
<VAR>ι : Type u_1<VAR>inst✝³ : LinearOrder ι<VAR>inst✝² : SuccOrder ι<VAR>inst✝¹ : IsSuccArchimedean ι<VAR>inst✝ : PredOrder ι<VAR>i0 i : ι<VAR>hi : i0 ≤ i<GOAL>0 ≤ ↑(Nat.find ⋯)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f ∈ s.finsuppAntidiag n ↔ (f.sum fun x x => x) = n ∧ f.support ⊆ s
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<GOAL>f.support ⊆ s → (s.sum ⇑f = n ↔ (f.sum fun x x => x) = n)
<VAR>ι : Type u_1<VAR>μ : Type u_2<VAR>μ' : Type u_3<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : AddCommMonoid μ<VAR>inst✝¹ : HasAntidiagonal μ<VAR>inst✝ : DecidableEq μ<VAR>s : Finset ι<VAR>n : μ<VAR>f : ι →₀ μ<VAR>hf : f.support ⊆ s<GOAL>s.sum ⇑f = n ↔ (f.sum fun x x => x) = n
<VAR>x y n m : ℕ<VAR>hx : x < 2 ^ n<VAR>hy : y < 2 ^ m<GOAL>y <<< n ||| x < 2 ^ (n + m)
<VAR>x y n m : ℕ<VAR>hx : x < 2 ^ n<VAR>hy : y < 2 ^ m<GOAL>y <<< n < 2 ^ (n + m)
<VAR>x y n m : ℕ<VAR>hx : x < 2 ^ n<VAR>hy : y < 2 ^ m<GOAL>x < 2 ^ (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>u₁ u₂ : UniformSpace γ<GOAL>uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>u₁ u₂ : UniformSpace γ<GOAL>⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>g : ι → α<VAR>inst✝ : UniformSpace β<VAR>u₁ u₂ : UniformSpace γ<VAR>i : Bool<GOAL>uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
<VAR>a x z✝ z : ℂ<VAR>θ : Real.Angle<GOAL>↑z.arg = θ ↔ z.arg = θ.toReal
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝² : CommMonoid α<VAR>inst✝¹ : CommMonoid β<VAR>s t : Multiset α<VAR>a✝ : α<VAR>m : Multiset ι<VAR>f g : ι → α<VAR>inst✝ : DecidableEq ι<VAR>a : ι<VAR>h : a ∈ m<GOAL>f a * (map f (m.erase a)).prod = (map f m).prod
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁵ : SeminormedAddCommGroup E<VAR>inst✝¹⁴ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹³ : SeminormedAddCommGroup F<VAR>inst✝¹² : SeminormedAddCommGroup Fₗ<VAR>inst✝¹¹ : SeminormedAddCommGroup G<VAR>inst✝¹⁰ : SeminormedAddCommGroup Gₗ<VAR>inst✝⁹ : NontriviallyNormedField 𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜₂<VAR>inst✝⁷ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>inst✝⁵ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁴ : NormedSpace 𝕜₂ F<VAR>inst✝³ : NormedSpace 𝕜 Fₗ<VAR>inst✝² : NormedSpace 𝕜₃ G<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝ : FunLike 𝓕 E F<VAR>f : E →SL[σ₁₂] F<GOAL>‖-f‖ = ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g f : α → ℝ≥0∞<VAR>h : μ s ≠ ⊤<GOAL>μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t : Set α<VAR>f✝ g f : α → ℝ≥0∞<VAR>h : μ s ≠ ⊤<VAR>this : Fact (μ s < ⊤)<GOAL>μ s * ⨍⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, f x ∂μ
<VAR>x✝ y z x : ℝ<VAR>hx : x ∈ interior (Ici 0)<GOAL>0 < deriv cosh x
<VAR>x✝ y z x : ℝ<VAR>hx : 0 < x<GOAL>0 < deriv cosh x
<VAR>α : Type u_1<VAR>inst✝⁸ : MetricSpace α<VAR>inst✝⁷ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁶ : IsUnifLocDoublingMeasure μ<VAR>inst✝⁵ : SecondCountableTopology α<VAR>inst✝⁴ : BorelSpace α<VAR>inst✝³ : IsLocallyFiniteMeasure μ<VAR>E : Type u_2<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>f : α → E<VAR>hf : LocallyIntegrable f μ<VAR>K : ℝ<GOAL>∀ᵐ (x : α) ∂μ, ∀ {ι : Type u_3} {l : Filter ι} (w : ι → α) (δ : ι → ℝ), Tendsto δ l (𝓝[>] 0) → (∀ᶠ (j : ι) in l, x ∈ closedBall (w j) (K * δ j)) → Tendsto (fun j => ⨍ (y : α) in closedBall (w j) (δ j), f y ∂μ) l (𝓝 (f x))
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>M.Base ∅ ↔ M = loopyOn M.E
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>E B I X R J : Set α<GOAL>(∀ (I : Set α), M.Indep I → I = ∅) ↔ ∀ I ⊆ M.E, M.Indep I ↔ I = ∅
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>p✝ : α → Prop<VAR>inst✝² : DecidablePred p✝<VAR>s s' : Multiset α<VAR>p p' : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred p'<GOAL>s = s' → (∀ x ∈ s, p x = p' x) → countP p s = countP p' s'
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>h✝ : IsEmpty ι<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>h✝ : Nonempty ι<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x y : ι → α<VAR>h : ∀ (i : ι), x i < y i<VAR>val✝ : Fintype ι<VAR>h✝ : Nonempty ι<VAR>ε : ι → α<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>hxε : ∀ (i : ι), x i + ε i = y i<GOAL>∃ ε, 0 < ε ∧ ∀ (i : ι), x i + ε < y i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x : ι → α<VAR>val✝ : Fintype ι<VAR>h✝ : Nonempty ι<VAR>ε : ι → α<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>h : ∀ (i : ι), x i < (x + ε) i<VAR>hxε : ∀ (i : ι), x i + ε i = (x + ε) i<GOAL>∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x : ι → α<VAR>val✝ : Fintype ι<VAR>h✝ : Nonempty ι<VAR>ε : ι → α<VAR>hε✝ : ∀ (i : ι), 0 < ε i<VAR>h : ∀ (i : ι), x i < (x + ε) i<VAR>hxε : ∀ (i : ι), x i + ε i = (x + ε) i<VAR>hε : 0 < Finset.univ.inf' ⋯ ε<GOAL>∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁴ : LinearOrderedCancelAddCommMonoid α<VAR>inst✝³ : Nontrivial α<VAR>inst✝² : DenselyOrdered α<VAR>inst✝¹ : ExistsAddOfLE α<VAR>inst✝ : Finite ι<VAR>x : ι → α<VAR>val✝ : Fintype ι<VAR>h✝ : Nonempty ι<VAR>ε : ι → α<VAR>hε✝ : ∀ (i : ι), 0 < ε i<VAR>h : ∀ (i : ι), x i < (x + ε) i<VAR>hxε : ∀ (i : ι), x i + ε i = (x + ε) i<VAR>hε : 0 < Finset.univ.inf' ⋯ ε<VAR>δ : α<VAR>hδ : 0 < δ<VAR>hδε : δ < Finset.univ.inf' ⋯ ε<GOAL>∃ ε_1, 0 < ε_1 ∧ ∀ (i : ι), x i + ε_1 < (x + ε) i
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<VAR>n : ℕ<GOAL>‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<GOAL>‖term f s 0‖ ≤ ‖↑C / ↑0 ^ (s + (1 - ↑x))‖
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<VAR>n : ℕ<VAR>hn : n > 0<GOAL>‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<VAR>n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n ^ s.re<GOAL>‖term f s n‖ ≤ ‖↑C / ↑n ^ (s + (1 - ↑x))‖
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<VAR>n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n ^ s.re<GOAL>‖f n‖ ≤ C * ↑n ^ (-(s + (1 - ↑x)).re + s.re)
<VAR>f : ℕ → ℂ<VAR>x : ℝ<VAR>s : ℂ<VAR>hs : x < s.re<VAR>C : ℝ<VAR>hC : ∀ (n : ℕ), n ≠ 0 → ‖f n‖ ≤ C * ↑n ^ (x - 1)<VAR>hC₀ : 0 ≤ C<VAR>hsum : Summable fun n => ‖↑C / ↑n ^ (s + (1 - ↑x))‖<VAR>n : ℕ<VAR>hn : n > 0<VAR>hn' : 0 < ↑n ^ s.re<GOAL>‖f n‖ ≤ C * ↑n ^ (x - 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>m : γ → β<GOAL>comap m (f.lift g) = f.lift (comap m ∘ g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Set α → Filter β<VAR>m : γ → β<GOAL>⨅ i ∈ f, comap m (g i) = ⨅ s ∈ f, (comap m ∘ g) s
<VAR>α : Type u_1<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : Fintype α<VAR>s t : Finset α<GOAL>Eₘ[s, univ] = Fintype.card α * s.card ^ 2
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<GOAL>DiscreteTopology ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>DiscreteTopology ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<GOAL>Subtype.val ⁻¹' Metric.ball 0 1 = {0}
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))<GOAL>x ∈ Subtype.val ⁻¹' Metric.ball 0 1 ↔ x ∈ {0}
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))<GOAL>(∀ (i : ι), ‖↑x i‖ < 1) ↔ x = 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))<GOAL>(∀ (i : ι), |↑x i| < 1) ↔ ∀ (a : ι), ↑x a = 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))<VAR>i : ι<GOAL>|↑x i| < 1 ↔ ↑x i = 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : Finite ι<VAR>val✝ : Fintype ι<VAR>x : ↥(span ℤ (Set.range ⇑(Pi.basisFun ℝ ι)))<VAR>i : ι<GOAL>∃ y, ↑y = ↑x i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>inst✝ : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s✝ s₁ s₂ t s : Set α<GOAL>μ s = μ.trim s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PartialOrder α<VAR>a b c x : α<GOAL>x ∈ Ico a b \ {a} ↔ x ∈ Ioo a b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : Rel α β<GOAL>⊥.inv = ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : CommRing B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : Algebra A B<VAR>inst✝ : IsIntegralClosure A R B<VAR>h : optParam (IsIntegral R 0) ⋯<GOAL>(algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : LinearOrder α<VAR>inst✝² : OrderTopology α<VAR>inst✝¹ : DenselyOrdered α<VAR>a✝ b✝ : α<VAR>s : Set α<VAR>inst✝ : NoMinOrder α<VAR>a b : α<VAR>h : a < b<GOAL>frontier (Ico a b) = {a, b}
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<VAR>hx3 : x ≠ 0<VAR>y : ℝ<VAR>hy1 : 0 < y<VAR>hy2 : y ≤ 3 * π / 2<GOAL>cos y < 1 / √(y ^ 2 + 1)
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<VAR>hx3 : x ≠ 0<VAR>y : ℝ<VAR>hy1 : 0 < y<VAR>hy2 : y ≤ 3 * π / 2<VAR>hy3 : 0 < y ^ 2 + 1<GOAL>cos y < 1 / √(y ^ 2 + 1)
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<VAR>hx3 : x ≠ 0<VAR>y : ℝ<VAR>hy1 : 0 < y<VAR>hy2 : y ≤ 3 * π / 2<VAR>hy3 : 0 < y ^ 2 + 1<VAR>hy2' : y < π / 2<GOAL>cos y < 1 / √(y ^ 2 + 1)
<VAR>x✝ x : ℝ<VAR>hx1 : -(3 * π / 2) ≤ x<VAR>hx2 : x ≤ 3 * π / 2<VAR>hx3 : x ≠ 0<VAR>y : ℝ<VAR>hy1 : 0 < y<VAR>hy2 : y ≤ 3 * π / 2<VAR>hy3 : 0 < y ^ 2 + 1<VAR>hy1' : π / 2 ≤ y<GOAL>cos y < 1 / √(y ^ 2 + 1)
<VAR>C : Type u_1<VAR>A : Type u_2<VAR>inst✝⁶ : Category.{?u.41960, u_1} C<VAR>inst✝⁵ : Category.{?u.41964, u_2} A<VAR>F : C ⥤ A<VAR>M : Type u_3<VAR>inst✝⁴ : AddMonoid M<VAR>inst✝³ : HasShift C M<VAR>G : Type u_4<VAR>inst✝² : AddGroup G<VAR>inst✝¹ : HasShift C G<VAR>inst✝ : F.ShiftSequence M<VAR>n m a a' a'' : M<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<GOAL>m + n + a = a''
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)<VAR>hr : r ≤ 0<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>ι : Type u_1<VAR>inst✝¹ : Fintype ι<VAR>p✝ : ℝ<VAR>hp✝ : 1 ≤ p✝<VAR>inst✝ : Nonempty ι<VAR>p : ℝ<VAR>hp : 1 ≤ p<VAR>r : ℝ<VAR>h₁ : ∀ (x : ι → ℝ), 0 ≤ ∑ i : ι, |x i| ^ p<VAR>h₂ : ∀ (x : ι → ℝ), 0 ≤ (∑ i : ι, |x i| ^ p) ^ (1 / p)<VAR>hr : 0 < r<GOAL>volume {x | (∑ i : ι, |x i| ^ p) ^ (1 / p) < r} = ENNReal.ofReal r ^ card ι * ENNReal.ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (↑(card ι) / p + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>C : Levenshtein.Cost α β δ<VAR>inst✝ : CanonicallyLinearOrderedAddCommMonoid δ<VAR>xs : List α<VAR>ys₁ ys₂ : List β<GOAL>(↑(suffixLevenshtein C xs ys₂)).minimum ≤ (↑(suffixLevenshtein C xs (ys₁ ++ ys₂))).minimum
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → H γ<VAR>x : Multiset α<GOAL>traverse (Comp.mk ∘ Functor.map h ∘ g) x = Comp.mk (traverse h <$> traverse g x)
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → H γ<VAR>x : Multiset α<GOAL>∀ (a : List α), traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a⟧ = Comp.mk (traverse h <$> traverse g ⟦a⟧)
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → H γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>traverse (Comp.mk ∘ Functor.map h ∘ g) ⟦a✝⟧ = Comp.mk (traverse h <$> traverse g ⟦a✝⟧)
<VAR>F : Type u → Type u<VAR>inst✝⁵ : Applicative F<VAR>inst✝⁴ : CommApplicative F<VAR>α' β' : Type u<VAR>f : α' → F β'<VAR>G H : Type u_1 → Type u_1<VAR>inst✝³ : Applicative G<VAR>inst✝² : Applicative H<VAR>inst✝¹ : CommApplicative G<VAR>inst✝ : CommApplicative H<VAR>α β γ : Type u_1<VAR>g : α → G β<VAR>h : β → H γ<VAR>x : Multiset α<VAR>a✝ : List α<GOAL>Comp.mk (((fun x => ofList <$> x) ∘ Traversable.traverse h) <$> Traversable.traverse g a✝) = Comp.mk ((Quotient.lift (Functor.map ofList ∘ Traversable.traverse h) ⋯ ∘ ofList) <$> Traversable.traverse g a✝)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Ring T<VAR>s : Subring R<VAR>x : R × S<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (RingHom.fst R S) s
<VAR>μ : YoungDiagram<VAR>i a b : ℕ<GOAL>(a, b) ∈ μ.row i ↔ (a, b) ∈ {i} ×ˢ Finset.range (μ.rowLen i)
<VAR>μ : YoungDiagram<VAR>i a b : ℕ<GOAL>a = i → (b < μ.rowLen a ↔ b < μ.rowLen i)
<VAR>μ : YoungDiagram<VAR>a b : ℕ<GOAL>b < μ.rowLen a ↔ b < μ.rowLen a
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hr : 0 ≤ r<GOAL>r.toNNReal = ‖r‖₊
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hr : 0 ≤ r<GOAL>⟨r, hr⟩ = ‖r‖₊
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a a₁ a₂ b b₁ b₂ : E<VAR>r r₁ r₂ : ℝ<VAR>hr : 0 ≤ r<GOAL>↑⟨r, hr⟩ = ↑‖r‖₊
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>inst✝¹ inst✝ : CommSemiring R<VAR>n : ℕ<VAR>φ ψ : MvPolynomial σ R<VAR>h : ∀ d ∈ φ.support, d.degree ≠ n<GOAL>(homogeneousComponent n) φ = 0