ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>d : ℕ<VAR>u : PrimeMultiset<GOAL>(d • u).prod = u.prod ^ d
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t✝ : Set α<VAR>μ ν : Measure α<VAR>inst✝ : Finite β<VAR>t : β → Set α<GOAL>IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>f g : α → E<VAR>s t✝ : Set α<VAR>μ ν : Measure α<VAR>inst✝ : Finite β<VAR>t : β → Set α<VAR>val✝ : Fintype β<GOAL>IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ
<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>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hs : f.source ⊆ s<VAR>hx : x ∈ f.source ∪ sᶜ<GOAL>G.IsLocalStructomorphWithinAt (↑f) s x ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<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>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hs : f.source ⊆ s<VAR>hx : x ∈ f.source ∪ sᶜ<GOAL>(x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source) ↔ x ∈ s → ∃ e ∈ G, e.source ⊆ f.source ∧ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<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>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hs : f.source ⊆ s<VAR>hx : x ∈ f.source ∪ sᶜ<VAR>x✝¹ : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>x✝ : e ∈ G<GOAL>e.source ⊆ f.source ∧ EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source ↔ e.source ⊆ f.source ∧ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<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>G : StructureGroupoid H<VAR>inst✝ : ClosedUnderRestriction G<VAR>f : PartialHomeomorph H H<VAR>s : Set H<VAR>x : H<VAR>hs : f.source ⊆ s<VAR>hx : x ∈ f.source ∪ sᶜ<VAR>x✝¹ : x ∈ s<VAR>e : PartialHomeomorph H H<VAR>x✝ : e ∈ G<VAR>h2e : e.source ⊆ f.source<GOAL>EqOn (↑f) (↑e) (s ∩ e.source) ∧ x ∈ e.source ↔ EqOn (↑f) (↑e) e.source ∧ x ∈ e.source
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : AEFinStronglyMeasurable f μ<VAR>t : Set α := hf.sigmaFiniteSet<GOAL>f =ᶠ[ae μ] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : AEFinStronglyMeasurable f μ<VAR>t : Set α := hf.sigmaFiniteSet<GOAL>f =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : AEFinStronglyMeasurable f μ<VAR>t : Set α := hf.sigmaFiniteSet<VAR>this : SigmaFinite (μ.restrict t)<GOAL>f =ᶠ[ae (μ.restrict t)] 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : AEFinStronglyMeasurable f μ<VAR>t : Set α := hf.sigmaFiniteSet<VAR>this : SigmaFinite (μ.restrict t)<GOAL>∀ (s : Set α), MeasurableSet s → (μ.restrict t) s < ⊤ → IntegrableOn f s (μ.restrict t)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℝ E<VAR>inst✝ : CompleteSpace E<VAR>p : ℝ≥0∞<VAR>f : α → E<VAR>hf_int_finite : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → IntegrableOn f s μ<VAR>hf_zero : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫ (x : α) in s, f x ∂μ = 0<VAR>hf : AEFinStronglyMeasurable f μ<VAR>t : Set α := hf.sigmaFiniteSet<VAR>this : SigmaFinite (μ.restrict t)<GOAL>∀ (s : Set α), MeasurableSet s → (μ.restrict t) s < ⊤ → ∫ (x : α) in s, f x ∂μ.restrict t = 0
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Connected<GOAL>H.Preconnected
<VAR>V : Type u<VAR>V' : Type v<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>H : G.Subgraph<VAR>h : H.Preconnected ∧ H.verts.Nonempty<GOAL>H.Preconnected
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>h₁ : EssFiniteType R S<VAR>h₂ : EssFiniteType S T<GOAL>EssFiniteType R T
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>h₁ : ∃ σ, ∀ (s : S), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ<VAR>h₂ : ∃ σ, ∀ (s : T), ∃ t ∈ adjoin S ↑σ, IsUnit t ∧ s * t ∈ adjoin S ↑σ<GOAL>∃ σ, ∀ (s : T), ∃ t ∈ adjoin R ↑σ, IsUnit t ∧ s * t ∈ adjoin R ↑σ
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>X Y Z : Scheme<VAR>𝒰 : X.OpenCover<VAR>f : X ⟶ Z<VAR>g : Y ⟶ Z<VAR>inst✝ : ∀ (i : 𝒰.J), HasPullback (𝒰.map i ≫ f) g<VAR>i j k : 𝒰.J<GOAL>t' 𝒰 f g i j k ≫ t' 𝒰 f g j k i ≫ t' 𝒰 f g k i j ≫ pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.snd (𝒰.map i ≫ f) g = pullback.snd (fV 𝒰 f g i j) (fV 𝒰 f g i k) ≫ pullback.fst (pullback.fst (𝒰.map i ≫ f) g ≫ 𝒰.map i) (𝒰.map k) ≫ pullback.snd (𝒰.map i ≫ f) g
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : f.Disjoint g<GOAL>_root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<GOAL>_root_.Disjoint f.cycleFactorsFinset g.cycleFactorsFinset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<GOAL>∀ ⦃a : Perm α⦄, a ∈ f.cycleFactorsFinset → a ∉ g.cycleFactorsFinset
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<VAR>x : Perm α<VAR>hx : x ∈ f.cycleFactorsFinset<VAR>hy : x ∈ g.cycleFactorsFinset<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<VAR>x : Perm α<VAR>hx : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = f a<VAR>hy : x.IsCycle ∧ ∀ (a : α), x a ≠ a → x a = g a<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<VAR>x : Perm α<VAR>hf : ∀ (a : α), x a ≠ a → x a = f a<VAR>a : α<VAR>ha : x a ≠ a<VAR>hg : ∀ (a : α), x a ≠ a → x a = g a<GOAL>False
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f g : Perm α<VAR>h : _root_.Disjoint f.support g.support<VAR>x : Perm α<VAR>hf : ∀ (a : α), x a ≠ a → x a = f a<VAR>a : α<VAR>ha : x a ≠ a<VAR>hg : ∀ (a : α), x a ≠ a → x a = g a<VAR>this : a ∈ ⊥<GOAL>False
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s : Finmap β<VAR>x : (i : α) × β i<GOAL>(x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }
<VAR>α : Type u<VAR>β : α → Type v<VAR>inst✝ : DecidableEq α<VAR>s : Finmap β<VAR>x : (i : α) × β i<VAR>this : x ∈ s.entries → x.fst ∈ s.keys<GOAL>(x ∈ s.keys.sigma fun i => (lookup i s).toFinset) ↔ x ∈ { val := s.entries, nodup := ⋯ }
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<GOAL>UniqueDiffWithinAt 𝕜 univ x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x y : E<VAR>s t : Set E<GOAL>Dense ↑(Submodule.span 𝕜 univ) ∧ x ∈ closure univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s t : Set α<VAR>x : α<VAR>S : Set (Set α)<GOAL>lowerClosure (⋃₀ S) = ⨆ s ∈ S, lowerClosure s
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>h : z.re = w.re<VAR>h₀ : 0 < z.im / w.im<GOAL>dist z w = dist (log z.im) (log w.im)
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>h : z.re = w.re<VAR>h₀ : 0 < z.im / w.im<GOAL>dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = w.im * |(z.im / w.im - w.im / z.im) / 2|
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>h : z.re = w.re<VAR>h₀ : 0 < z.im / w.im<GOAL>dist z.im (w.im * ((z.im / w.im + w.im / z.im) / 2)) = |w.im| * |(z.im / w.im - w.im / z.im) / 2|
<VAR>z w : ℍ<VAR>r R : ℝ<VAR>h : z.re = w.re<VAR>h₀ : 0 < z.im / w.im<GOAL>|z.im - w.im * ((z.im / w.im + w.im / z.im) / 2)| = |w.im * ((z.im / w.im - w.im / z.im) / 2)|
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>|(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w‖ ≤ (2 * π) ^ n * (|(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w‖)
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>1 ≤ (2 * π) ^ n
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>1 ≤ 2 * π
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>(2 * π) ^ n * (|(L v) w| ^ n * ‖iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₂ f) w‖) = ‖(fourierPowSMulRight (-L.flip) (iteratedFDeriv ℝ k (fourierIntegral 𝐞 μ L.toLinearMap₂ f)) w n) fun x => v‖
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>((2 * π) ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ) * ‖v‖ ^ n = ‖v‖ ^ n * (2 * π * ‖L‖) ^ k * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>E : Type u_1<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedSpace ℂ E<VAR>V : Type u_2<VAR>W : Type u_3<VAR>inst✝⁸ : NormedAddCommGroup V<VAR>inst✝⁷ : NormedSpace ℝ V<VAR>inst✝⁶ : NormedAddCommGroup W<VAR>inst✝⁵ : NormedSpace ℝ W<VAR>L : V →L[ℝ] W →L[ℝ] ℝ<VAR>f : V → E<VAR>inst✝⁴ : SecondCountableTopology V<VAR>inst✝³ : MeasurableSpace V<VAR>inst✝² : BorelSpace V<VAR>μ✝ : Measure V<VAR>inst✝¹ : FiniteDimensional ℝ V<VAR>μ : Measure V<VAR>inst✝ : μ.IsAddHaarMeasure<VAR>K N : ℕ∞<VAR>hf : ContDiff ℝ N f<VAR>h'f : ∀ (k n : ℕ), ↑k ≤ K → ↑n ≤ N → Integrable (fun v => ‖v‖ ^ k * ‖iteratedFDeriv ℝ n f v‖) μ<VAR>k n : ℕ<VAR>hk : ↑k ≤ K<VAR>hn : ↑n ≤ N<VAR>v : V<VAR>w : W<GOAL>(2 ^ k * π ^ k * (2 * ↑k + 2) ^ n * ‖L‖ ^ k * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ) * ‖v‖ ^ n = ‖v‖ ^ n * (2 ^ k * π ^ k * ‖L‖ ^ k) * (2 * ↑k + 2) ^ n * ∑ p ∈ Finset.range (k + 1) ×ˢ Finset.range (n + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 f v‖ ∂μ
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Fork (𝟙 X) f<VAR>i : IsLimit c<GOAL>c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 (((Functor.const WalkingParallelPair).obj c.pt).obj zero)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Fork (𝟙 X) f<VAR>i : IsLimit c<VAR>this : Mono c.ι := mono_of_isLimit_fork i<GOAL>c.ι ≫ i.lift (Fork.ofι f ⋯) = 𝟙 (((Functor.const WalkingParallelPair).obj c.pt).obj zero)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X✝ Y : C<VAR>f✝ g : X✝ ⟶ Y<VAR>X : C<VAR>f : X ⟶ X<VAR>hf : f ≫ f = f<VAR>c : Fork (𝟙 X) f<VAR>i : IsLimit c<VAR>this : Mono c.ι := mono_of_isLimit_fork i<GOAL>c.ι ≫ 𝟙 X = c.ι
<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<GOAL>insepDegree F ↥⊥ = 1
<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>this : Cardinal.lift.{u, v} (insepDegree F ↥⊥) = Cardinal.lift.{v, u} (insepDegree F F)<GOAL>insepDegree F ↥⊥ = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<GOAL>cyclotomic n R = (X ^ n - 1) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<GOAL>cyclotomic n R = (cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<GOAL>cyclotomic n R = (cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R) /ₘ ∏ i ∈ n.properDivisors, cyclotomic i R
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<GOAL>0 + (∏ i ∈ n.properDivisors, cyclotomic i R) * cyclotomic n R = cyclotomic n R * ∏ x ∈ n.properDivisors, cyclotomic x R ∧ degree 0 < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<GOAL>(∏ i ∈ n.properDivisors, cyclotomic i R) * cyclotomic n R = cyclotomic n R * ∏ i ∈ n.properDivisors, cyclotomic i R ∧ ⊥ < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<GOAL>⊥ < (∏ i ∈ n.properDivisors, cyclotomic i R).degree
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<GOAL>(∏ i ∈ n.properDivisors, cyclotomic i R).degree ≠ ⊥
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>n : ℕ<VAR>hpos : 0 < n<VAR>a✝ : Nontrivial R<VAR>prod_monic : (∏ i ∈ n.properDivisors, cyclotomic i R).Monic<VAR>h : (∏ i ∈ n.properDivisors, cyclotomic i R).degree = ⊥<GOAL>False
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u✝ v✝ w✝ u v w : V<VAR>h : G.Adj u v<VAR>p : G.Walk v w<GOAL>(cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support
<VAR>i j : ℤ<GOAL>i.gcd j = 0 ↔ i = 0 ∧ j = 0
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedRing R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto f l atBot<GOAL>Tendsto (fun x => f x * r) l atBot
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>l : Filter α<VAR>f : α → R<VAR>r : R<VAR>inst✝¹ : LinearOrderedRing R<VAR>inst✝ : Archimedean R<VAR>hr : 0 < r<VAR>hf : Tendsto (fun x => -f x) l atTop<GOAL>Tendsto (fun x => -f x * r) l atTop
<VAR>k : Type u_1<VAR>E : Type u_2<VAR>PE : Type u_3<VAR>inst✝³ : OrderedRing k<VAR>inst✝² : OrderedAddCommGroup E<VAR>inst✝¹ : Module k E<VAR>inst✝ : OrderedSMul k E<VAR>a a' b b' : E<VAR>r r' : k<VAR>h : r < 1<GOAL>(lineMap a b) r < b ↔ (lineMap a b) r < (lineMap a b) 1
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m : M<VAR>s : ↥S<GOAL>s • mk' f m s = f m
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => r * f x) l atTop ↔ 0 < r
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<VAR>hrf : Tendsto (fun x => r * f x) l atTop<VAR>hr : r ≤ 0<GOAL>False
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedSemifield α<VAR>l : Filter β<VAR>f : β → α<VAR>r c : α<VAR>n : ℕ<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<VAR>hrf : Tendsto (fun x => r * f x) l atTop<VAR>hr : r ≤ 0<VAR>x : β<VAR>hx : 0 ≤ f x<VAR>hrx : 0 < r * f x<GOAL>False
<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>E : K ⥤ J<VAR>j✝ : K<GOAL>ι (E ⋙ F) j✝ ≫ pre F E ≫ colim.map α = ι (E ⋙ F) j✝ ≫ colim.map (whiskerLeft E α) ≫ pre G E
<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>E : K ⥤ J<VAR>j✝ : K<GOAL>α.app (E.obj j✝) ≫ ι G (E.obj j✝) = (whiskerLeft E α).app j✝ ≫ ι G (E.obj j✝)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : LE α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<VAR>ha : MulLECancellable a<GOAL>a ≤ a * b ↔ a * 1 ≤ a * b