ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<VAR>this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : l.IsCountablyGenerated<VAR>inst✝ : l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))<VAR>u : ℕ → ι<VAR>hu : Tendsto u atTop l<VAR>this : AEMeasurable f (μ.restrict (⋃ i, φ (u i)))<GOAL>∀ᵐ (x : α) ∂μ, x ∈ ⋃ i, φ (u i)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DivisionMonoid α<VAR>s t : Finset α<GOAL>IsUnit ↑s ↔ IsUnit s
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : NeZero p<VAR>n : ℕ<GOAL>(W_ R n).vars ⊆ range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>hp : NeZero p<VAR>n : ℕ<GOAL>((map (Int.castRingHom R)) (W_ ℤ n)).vars ⊆ (W_ ℤ n).vars
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : ℝ[X]<GOAL>(g.toContinuousMapOn (Set.Icc (-‖f‖) ‖f‖)).comp (↑f).attachBound ∈ A
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : CompactSpace X<VAR>A : Subalgebra ℝ C(X, ℝ)<VAR>f : ↥A<VAR>g : ℝ[X]<GOAL>↑((Polynomial.aeval f) g) ∈ A
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : A₀.a ≅ A₁.a<VAR>w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝<GOAL>F.map h.inv ≫ A₀.str = A₁.str ≫ h.inv
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>F : C ⥤ C<VAR>A A₀ A₁ A₂ : Algebra F<VAR>f : A₀ ⟶ A₁<VAR>g : A₁ ⟶ A₂<VAR>h : A₀.a ≅ A₁.a<VAR>w : autoParam (F.map h.hom ≫ A₁.str = A₀.str ≫ h.hom) _auto✝<GOAL>F.map (h.inv ≫ h.hom) ≫ A₁.str = A₁.str
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : Field E<VAR>inst✝³ : Algebra F E<VAR>K : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra F K<VAR>inst✝ : Algebra.IsSeparable F E<GOAL>insepDegree F E = 1
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z✝ z : K<GOAL>z / I = -(z * I)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>p.length = Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>1 ≤ Fintype.card α
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : Fintype α<VAR>inst✝² : Fintype β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>G : SimpleGraph α<VAR>a b : α<VAR>p✝ : G.Walk a b<VAR>p : G.Walk a a<VAR>hp : p.IsHamiltonianCycle<GOAL>Nonempty α
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (1 / z) ≤ y ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (1 / z) ≤ y ^ 1 ↔ x ≤ y ^ z
<VAR>x y : ℝ≥0∞<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ^ (1 / z) ≤ y ^ (z * z⁻¹) ↔ x ≤ y ^ z
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>p : G.Walk u v<VAR>hp : p.length = G.dist u v<GOAL>p.IsPath
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype p<VAR>inst✝ : AddCommMonoid R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>A.trace = A 0 0 + A 1 1 + A 2 2
<VAR>ι : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>p : Type u_4<VAR>α : Type u_5<VAR>R : Type u_6<VAR>S : Type u_7<VAR>inst✝³ : Fintype m<VAR>inst✝² : Fintype n<VAR>inst✝¹ : Fintype p<VAR>inst✝ : AddCommMonoid R<VAR>A : Matrix (Fin 3) (Fin 3) R<GOAL>A.trace = A 0 0 + (A 1 1 + (A 2 2 + 0))
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono_of_mem : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x<VAR>h : LiftPropWithinAt P g s x<VAR>hst : s ∈ 𝓝[t] x<GOAL>LiftPropWithinAt P g t x
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono_of_mem : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x<VAR>hst : s ∈ 𝓝[t] x<VAR>h : ContinuousWithinAt g s x ∧ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)<GOAL>ContinuousWithinAt g t x ∧ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' t) (↑(chartAt H x) x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁶ : TopologicalSpace H<VAR>inst✝⁵ : TopologicalSpace M<VAR>inst✝⁴ : ChartedSpace H M<VAR>inst✝³ : TopologicalSpace H'<VAR>inst✝² : TopologicalSpace M'<VAR>inst✝¹ : ChartedSpace H' M'<VAR>inst✝ : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>mono_of_mem : ∀ ⦃s : Set H⦄ ⦃x : H⦄ ⦃t : Set H⦄ ⦃f : H → H'⦄, s ∈ 𝓝[t] x → P f s x → P f t x<VAR>hst : s ∈ 𝓝[t] x<VAR>h : ContinuousWithinAt g s x ∧ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x)<GOAL>↑(chartAt H x).symm ⁻¹' s ∈ 𝓝[↑(chartAt H x).symm ⁻¹' t] ↑(chartAt H x) x
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n : α<GOAL>gcd k (m * n) ∣ gcd k m * gcd k n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n m' n' : α<VAR>hm' : m' ∣ m<VAR>hn' : n' ∣ n<VAR>h : gcd k (m * n) = m' * n'<GOAL>gcd k (m * n) ∣ gcd k m * gcd k n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n m' n' : α<VAR>hm' : m' ∣ m<VAR>hn' : n' ∣ n<VAR>h : gcd k (m * n) = m' * n'<GOAL>m' * n' ∣ gcd k m * gcd k n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n m' n' : α<VAR>hm' : m' ∣ m<VAR>hn' : n' ∣ n<VAR>h : gcd k (m * n) = m' * n'<VAR>hm'n' : m' * n' ∣ k<GOAL>m' * n' ∣ gcd k m * gcd k n
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n m' n' : α<VAR>hm' : m' ∣ m<VAR>hn' : n' ∣ n<VAR>h : gcd k (m * n) = m' * n'<VAR>hm'n' : m' * n' ∣ k<GOAL>m' ∣ gcd k m
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : GCDMonoid α<VAR>k m n m' n' : α<VAR>hm' : m' ∣ m<VAR>hn' : n' ∣ n<VAR>h : gcd k (m * n) = m' * n'<VAR>hm'n' : m' * n' ∣ k<GOAL>n' ∣ gcd k n
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G✝ : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>G : SimpleGraph V<VAR>e : V ≃ W<VAR>x✝¹ x✝ : W<GOAL>(SimpleGraph.comap (⇑e.symm.toEmbedding) G).Adj x✝¹ x✝ ↔ (SimpleGraph.map e.toEmbedding G).Adj x✝¹ x✝
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>w x✝ y z : ℝ<VAR>x : ℝ≥0<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>(↑x ^ (↑n)⁻¹) ^ n = ↑x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>x dx y dy : α<VAR>h : dy < dx<VAR>hx : 0 < dx<GOAL>Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>x dx y dy : α<VAR>h : dy < dx<VAR>hx : 0 < dx<VAR>h' : x < y<GOAL>Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>x dx y dy : α<VAR>h : dy < dx<VAR>hx : 0 < dx<VAR>h' : y ≤ x<GOAL>Nonempty ↑(Ico x (x + dx) \ Ico y (y + dy))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>o : Part α<VAR>a : α<VAR>h : a ∈ o<VAR>f : α → Part β<GOAL>o.bind f = f a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h : ae μ ≤ ae ν<VAR>s : Set α<GOAL>ν s = 0 → μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>f : α → β<VAR>h : ae μ ≤ ae ν<VAR>s : Set α<GOAL>(∀ᵐ (a : α) ∂ν, a ∉ s) → ∀ᵐ (a : α) ∂μ, a ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s s₁✝ s₂✝ t t₁ t₂ u v : Finset α<VAR>a✝ b : α<VAR>s₁ s₂ : Finset α<VAR>a : α<VAR>h : a ∉ s₁<GOAL>s₁ ∩ insert a s₂ = s₁ ∩ s₂
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<GOAL>basicOpen 𝒜 (f * g) ≤ basicOpen 𝒜 g
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f g : A<GOAL>basicOpen 𝒜 f ⊓ basicOpen 𝒜 g ≤ basicOpen 𝒜 g
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f'✝ f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s✝ t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x₀ : 𝕜<VAR>hf : HasDerivAt f f' x₀<VAR>s : Set 𝕜<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖f'‖ ≤ ↑C
<VAR>α : Type u<VAR>σ σ' : Type v<VAR>M : εNFA α σ<VAR>S : Set σ<VAR>x : List α<VAR>s : σ<VAR>a✝ a : α<GOAL>M.stepSet ∅ a = ∅
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>a : Γ<VAR>L R : ListBlank Γ<VAR>n : ℕ<GOAL>(move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) = { head := a, left := L, right := R }.nth (↑(n + 1) + 1 - 1)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>a : Γ<VAR>L R : ListBlank Γ<VAR>n : ℕ<GOAL>(move Dir.left { head := a, left := L, right := R }).nth (↑(n + 1) + 1) = { head := a, left := L, right := R }.nth ↑(n + 1)
<VAR>Γ : Type u_1<VAR>inst✝ : Inhabited Γ<VAR>a : Γ<VAR>L R : ListBlank Γ<VAR>n : ℕ<GOAL>(ListBlank.cons a R).nth (n + 1) = R.nth n
<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 : φ.totalDegree < n<GOAL>(homogeneousComponent n) φ = 0
<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 : φ.totalDegree < n<GOAL>∀ d ∈ φ.support, d.degree ≠ n
<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 : ∀ b ∈ φ.support, (b.sum fun x e => e) < n<GOAL>∀ d ∈ φ.support, d.degree ≠ n
<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 : ∀ b ∈ φ.support, (b.sum fun x e => e) < n<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ φ.support<GOAL>d.degree ≠ n
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : Set E<GOAL>IsClosed (((dualPairing 𝕜 E).flip.flip.polar ∘ ⇑OrderDual.ofDual) ((dualPairing 𝕜 E).flip.polar s))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : SeminormedRing α<VAR>inst✝ : NormOneClass α<VAR>l : List α<GOAL>(map norm l).prod = (fun a => ↑a) (map nnnorm l).prod
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<GOAL>P.Λ (↑P.k - s) = P.ε • P.symm.Λ s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (t ^ (-1))) (-s) = |(-1)|⁻¹ • mellin P.g (-s / ↑(-1))<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin (fun t => P.g (1 / t)) (↑P.k - s + -↑P.k)<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)<GOAL>mellin P.f (↑P.k - s) = P.ε • mellin P.g s
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s<GOAL>mellin P.f (↑P.k - s) = mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s)
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (↑P.k - s - 1) • P.f t = ↑t ^ (↑P.k - s - 1) • (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * (↑t ^ (-↑P.k) * (P.ε⁻¹ * ↑(t ^ P.k))))) • P.f t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<GOAL>↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>P : StrongFEPair E<VAR>s : ℂ<VAR>step1 : mellin (fun t => P.g (1 / t)) (-s) = mellin P.g s<VAR>step2 : mellin (fun t => ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = mellin P.g s<VAR>step3 : mellin (fun t => P.ε • ↑t ^ (-↑P.k) • P.g (1 / t)) (↑P.k - s) = P.ε • mellin P.g s<VAR>t : ℝ<VAR>ht : t ∈ Ioi 0<VAR>this : ↑t ^ ↑P.k ≠ 0<GOAL>↑t ^ (↑P.k - s - 1) • P.f t = (↑t ^ (↑P.k - s - 1) * (P.ε * ((↑t ^ ↑P.k)⁻¹ * (P.ε⁻¹ * ↑t ^ ↑P.k)))) • P.f t
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s t : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>hf : HasDerivAtFilter f f' x✝ L<VAR>hf' : f' ≠ 0<VAR>x : 𝕜<GOAL>‖x‖ ≤ ↑‖f'‖₊⁻¹ * ‖(smulRight 1 f') x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n : ℕ<GOAL>edist (f n) a ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>m ∈ {x | (fun c => edist (f n) (f c) ≤ ∑' (m : ℕ), d (n + m)) x}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>edist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>∑ i ∈ Finset.Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : PseudoEMetricSpace α<VAR>f : ℕ → α<VAR>d : ℕ → ℝ≥0∞<VAR>hf : ∀ (n : ℕ), edist (f n) (f n.succ) ≤ d n<VAR>a : α<VAR>ha : Tendsto f atTop (𝓝 a)<VAR>n m : ℕ<VAR>hnm : m ≥ n<GOAL>∑ k ∈ Finset.range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<GOAL>¬IsFiniteMeasure μ ↔ μ univ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>h : ¬IsFiniteMeasure μ<GOAL>μ univ = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>ι : Type u_4<VAR>m0 : MeasurableSpace α<VAR>inst✝ : MeasurableSpace β<VAR>μ ν ν₁ ν₂ : Measure α<VAR>s t : Set α<VAR>h : ¬IsFiniteMeasure μ<VAR>h' : ¬μ univ = ⊤<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hμ : IsFiniteMeasure μ<GOAL>(fun s => if MeasurableSet s then (μ s).toReal else 0) ∅ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => (fun s => if MeasurableSet s then (μ s).toReal else 0) (f i)) ((fun s => if MeasurableSet s then (μ s).toReal else 0) (⋃ i, f i))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => (μ (f i)).toReal) (∑' (i : ℕ), μ (f i)).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>HasSum (fun i => (μ (f i)).toReal) (∑' (a : ℕ), (μ (f a)).toReal)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>hμ : IsFiniteMeasure μ<VAR>f : ℕ → Set α<VAR>hf₁ : ∀ (i : ℕ), MeasurableSet (f i)<VAR>hf₂ : Pairwise (Disjoint on f)<GOAL>∀ (a : ℕ), μ (f a) ≠ ⊤
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>-((v Q) m * e0 Q) = e0 Q * (v Q) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝² : CommRing R<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>m : M<GOAL>(v Q) m * e0 Q = -(e0 Q * (v Q) m)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝² : _root_.RCLike 𝕜<VAR>inst✝¹ : AddCommGroup F<VAR>inst✝ : Module 𝕜 F<VAR>c : Core 𝕜 F<VAR>x y z : F<GOAL>⟪x - y, z⟫_𝕜 = ⟪x, z⟫_𝕜 - ⟪y, z⟫_𝕜
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<GOAL>normUnit (a * ↑(normUnit a)) = 1
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>a✝ : Nontrivial α<GOAL>normUnit (a * ↑(normUnit a)) = 1
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a✝ : Nontrivial α<GOAL>normUnit (0 * ↑(normUnit 0)) = 1
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>a✝ : Nontrivial α<VAR>h : a ≠ 0<GOAL>normUnit (a * ↑(normUnit a)) = 1
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>m✝ : OuterMeasure α<VAR>β : Type u_3<VAR>f : α → β<VAR>m m' : OuterMeasure α<VAR>s : Set β<GOAL>((map f) (m ⊔ m')) s = ((map f) m ⊔ (map f) m') s
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>m : M<GOAL>‖S.normedMk m‖ ≤ 1 * ‖m‖
<VAR>α : Type u_1<VAR>inst✝ : DivisionRing α<VAR>n : ℤ<VAR>h : Odd n<GOAL>(-1) ^ n = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p q : α → Prop<VAR>inst✝¹ : DecidablePred p<VAR>inst✝ : DecidablePred q<VAR>s t : Finset α<GOAL>filter p s = s ↔ ∀ x ∈ s, p x
<VAR>x✝ y✝ z x y : ℝ<GOAL>|x ^ y| ≤ rexp (log x * y)
<VAR>x✝ y✝ z x y : ℝ<GOAL>|x| ^ y ≤ rexp (log x * y)