ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>V : Type u_3<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Semiring R<VAR>inst✝ : Module R V<VAR>k : ℕ<VAR>r : R<VAR>f : LaurentSeries V<VAR>x✝ : ℤ<GOAL>({ toFun := fun f => ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯, map_add' := ⋯ }.toFun (r • f)).coeff x✝ = ((RingHom.id R) r • { toFun := fun f => ofSuppBddBelow (fun n => Ring.choose (n + ↑k) k • f.coeff (n + ↑k)) ⋯, map_add' := ⋯ }.toFun f).coeff x✝
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>a : ℤ<GOAL>legendreSym p a = legendreSym p (a % ↑p)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n k : ℕ<GOAL>multiplicity p (n + 1) ≤ multiplicity p ((n + 1).choose (k + 1)) + multiplicity p (k + 1)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n k : ℕ<GOAL>multiplicity p (n + 1) ≤ multiplicity p ((n + 1).choose (k + 1) * (k + 1))
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n k : ℕ<GOAL>n + 1 ∣ (n + 1).choose (k + 1) * (k + 1)
<VAR>p : ℕ<VAR>hp : Prime p<VAR>n k : ℕ<GOAL>n + 1 ∣ n.succ * n.choose k
<VAR>i : ℤ<GOAL>i.natAbs.lcm (natAbs 1) = i.natAbs
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>ht : NullMeasurableSet t μ<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>(μ.restrict (s ∩ t) + μ.restrict (s \ t)) u = (μ.restrict s) u
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t s : Set α<VAR>ht : NullMeasurableSet t μ<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>μ (u ∩ s ∩ t) + μ (u ∩ s ∩ tᶜ) = μ (u ∩ s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f✝ g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝ : AddZeroClass α<VAR>f : α → β<VAR>x : α<GOAL>f (x + 0) = f x
<VAR>x y : EReal<VAR>h : x < y<VAR>z : ℝ<GOAL>↑z + x < ↑z + y
<VAR>K : Type u<VAR>inst✝² : CommRing K<VAR>inst✝¹ : IsDomain K<VAR>L : Type u_1<VAR>inst✝ : CommGroupWithZero L<VAR>φ : K[X] →*₀ L<VAR>hφ : K[X]⁰ ≤ Submonoid.comap φ L⁰<VAR>p q : K[X]<GOAL>(liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) p) / (liftMonoidWithZeroHom φ hφ) ((algebraMap K[X] (RatFunc K)) q) = φ p / φ q
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) ∅ ∂ν a = (κ a) (s ×ˢ ∅)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∀ t ∈ range Iic, ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∀ (t : Set ℝ), MeasurableSet t → ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t) → ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) tᶜ ∂ν a = (κ a) (s ×ˢ tᶜ)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>κ : Kernel α (β × ℝ)<VAR>ν : Kernel α β<VAR>f : α × β → StieltjesFunction<VAR>inst✝ : IsFiniteKernel κ<VAR>hf : IsCondKernelCDF f κ ν<VAR>a : α<VAR>s : Set β<VAR>hs : MeasurableSet s<VAR>t : Set ℝ<VAR>ht : MeasurableSet t<GOAL>∀ (f_1 : ℕ → Set ℝ), Pairwise (Disjoint on f_1) → (∀ (i : ℕ), MeasurableSet (f_1 i)) → (∀ (i : ℕ), ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (f_1 i) ∂ν a = (κ a) (s ×ˢ f_1 i)) → ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) (⋃ i, f_1 i) ∂ν a = (κ a) (s ×ˢ ⋃ i, f_1 i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>hc : 0 < c<GOAL>IsBigOWith c⁻¹ l f g ↔ ∀ᶠ (x : α) in l, c * ‖f x‖ ≤ ‖g x‖
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝ : Preorder α<GOAL>𝓝 atTop = ⨅ x, 𝓟 (Iic (𝓟 (Ici x)))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace Y<VAR>inst✝³ : TopologicalSpace Z<VAR>inst✝² : TopologicalSpace W<VAR>inst✝¹ : TopologicalSpace ε<VAR>inst✝ : TopologicalSpace ζ<VAR>f : X → Y<VAR>g : Z → W<VAR>hf : Inducing f<VAR>hg : Inducing g<VAR>x✝ : X × Z<VAR>x : X<VAR>z : Z<GOAL>𝓝 (x, z) = comap (Prod.map f g) (𝓝 (Prod.map f g (x, z)))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>a b c d : α<GOAL>a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : Nontrivial α<VAR>p q r : α<VAR>h : DvdNotUnit p q<VAR>h' : q ~ᵤ r<GOAL>DvdNotUnit p r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : Nontrivial α<VAR>p r : α<VAR>u : αˣ<VAR>h : DvdNotUnit p (r * ↑u)<VAR>h' : r * ↑u ~ᵤ r<GOAL>DvdNotUnit p r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : Nontrivial α<VAR>p r : α<VAR>u : αˣ<VAR>h' : r * ↑u ~ᵤ r<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx : ¬IsUnit x ∧ r * ↑u = p * x<GOAL>DvdNotUnit p r
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝¹ : CommMonoidWithZero α<VAR>inst✝ : Nontrivial α<VAR>p r : α<VAR>u : αˣ<VAR>h' : r * ↑u ~ᵤ r<VAR>hp : p ≠ 0<VAR>x : α<VAR>hx : ¬IsUnit x ∧ r * ↑u = p * x<GOAL>r = p * (x * ↑u⁻¹)
<VAR>J : Type u_1<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : HasInitial C<VAR>inst✝ : DecidableEq J<VAR>j : J<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(singleObjApplyIso j X).inv ≫ (single j).map f j = f ≫ (singleObjApplyIso j Y).inv
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>b ⇨ a = a ⇨ b ↔ a = b
<VAR>x y : ℝ<GOAL>cos x ^ 2 = 1 - sin x ^ 2
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>l : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>inst✝⁸ : Fintype n<VAR>inst✝⁷ : Fintype m<VAR>inst✝⁶ : DecidableEq n<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R M₁<VAR>inst✝² : Module R M₂<VAR>v₁ : Basis n R M₁<VAR>v₂ : Basis m R M₂<VAR>M₃ : Type u_7<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>v₃ : Basis l R M₃<GOAL>(toLinAlgEquiv v₁) 1 = LinearMap.id
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ p₄ : P<VAR>h : Wbtw ℝ p₁ p₂ p₃<VAR>hne : p₁ ≠ p₂<GOAL>Collinear ℝ {p₁, p₂, p₁, p₃}
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.εIso.inv.app X) = (F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>M : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} M<VAR>inst✝ : MonoidalCategory M<VAR>F : MonoidalFunctor M (C ⥤ C)<VAR>n : M<VAR>X : C<GOAL>(F.obj n).map (F.εIso.inv.app X ≫ F.ε.app X) = ((F.μ (𝟙_ M) n).app X ≫ (F.map (λ_ n).hom).app X) ≫ (F.obj n).map (F.ε.app X)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p = 0<GOAL>∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p = 0<GOAL>∀ x ∈ s, f x = 0 ∨ g x = 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∑ i ∈ s, f i ^ p = 0<VAR>i : ι<VAR>his : i ∈ s<GOAL>f i = 0
<VAR>ι : Type u<VAR>s : Finset ι<VAR>f g : ι → ℝ≥0<VAR>p q : ℝ<VAR>hpq : p.IsConjExponent q<VAR>hf : ∀ x ∈ s, f x ^ p = 0<VAR>i : ι<VAR>his : i ∈ s<GOAL>f i = 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>V' : Type u_3<VAR>P : Type u_4<VAR>P' : Type u_5<VAR>inst✝⁶ : OrderedRing R<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module R V<VAR>inst✝³ : AddTorsor V P<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module R V'<VAR>inst✝ : AddTorsor V' P'<VAR>x y z : P<GOAL>Sbtw R x y z ↔ Sbtw R z y x
<GOAL>Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))
<VAR>this : Tendsto (fun x => riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))<GOAL>Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))
<VAR>this : Tendsto (fun x => riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))<GOAL>Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))
<VAR>θ : ℝ<GOAL>(↑θ).toReal = θ ↔ θ ∈ Set.Ioc (-π) π
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<GOAL>StronglyMeasurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<GOAL>StronglyMeasurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<GOAL>StronglyMeasurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<GOAL>StronglyMeasurable (uncurry u)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<GOAL>StronglyMeasurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2<GOAL>StronglyMeasurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>StronglyMeasurable (U n)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>StronglyMeasurable ((fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2))
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>ι✝ : Type u_4<VAR>inst✝⁸ : Countable ι✝<VAR>α : Type u_5<VAR>β : Type u_6<VAR>ι : Type u_7<VAR>inst✝⁷ : TopologicalSpace ι<VAR>inst✝⁶ : MetrizableSpace ι<VAR>inst✝⁵ : MeasurableSpace ι<VAR>inst✝⁴ : SecondCountableTopology ι<VAR>inst✝³ : OpensMeasurableSpace ι<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : PseudoMetrizableSpace β<VAR>inst✝ : MeasurableSpace α<VAR>u : ι → α → β<VAR>hu_cont : ∀ (x : α), Continuous fun i => u i x<VAR>h : ∀ (i : ι), StronglyMeasurable (u i)<VAR>this✝¹ : MeasurableSpace β := borel β<VAR>this✝ : BorelSpace β<VAR>t_sf : ℕ → ι →ₛ ι<VAR>ht_sf : ∀ (j : ι) (x : α), Tendsto (fun n => u (↑(t_sf n) j) x) atTop (𝓝 (u j x))<VAR>U : ℕ → ι × α → β := fun n p => u (↑(t_sf n) p.1) p.2<VAR>h_tendsto : Tendsto U atTop (𝓝 fun p => u p.1 p.2)<VAR>n : ℕ<VAR>h_str_meas : StronglyMeasurable fun p => u (↑p.1) p.2<VAR>this : (fun p => u (↑(t_sf n) p.1) p.2) = (fun p => u (↑p.1) p.2) ∘ fun p => (⟨↑(t_sf n) p.1, ⋯⟩, p.2)<GOAL>Measurable fun p => ⟨↑(t_sf n) p.1, ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>x y z : α<VAR>ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ t : Set α<VAR>d : ℝ≥0∞<VAR>f : β → α<VAR>s : Set β<GOAL>diam (f '' s) ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) ≤ d
<VAR>A : Type u<VAR>B : Type v<VAR>inst✝¹ : CommGroup A<VAR>inst✝ : CommGroup B<VAR>f : A →* B<VAR>h : (QuotientGroup.mk' f.range).ker = ker 1<GOAL>f.range = ⊤
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m : ℕ<VAR>hcop : m.Coprime n<GOAL>(map (Int.castRingHom K) (minpoly ℤ μ)).IsRoot (μ ^ m)
<VAR>n : ℕ<VAR>K : Type u_1<VAR>inst✝² : CommRing K<VAR>μ : K<VAR>h : IsPrimitiveRoot μ n<VAR>inst✝¹ : IsDomain K<VAR>inst✝ : CharZero K<VAR>m : ℕ<VAR>hcop : m.Coprime n<GOAL>eval₂ (Int.castRingHom K) (μ ^ m) (minpoly ℤ (μ ^ m)) = 0
<VAR>F✝ : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p : K[X]<VAR>F : IntermediateField K L<VAR>h : Splits (algebraMap K L) p<VAR>hF : ∀ x ∈ p.rootSet L, x ∈ F<GOAL>Splits (algebraMap K ↥F) p
<VAR>F✝ : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Algebra K L<VAR>p : K[X]<VAR>F : IntermediateField K L<VAR>h : Splits (algebraMap K L) p<VAR>hF : ∀ x ∈ p.aroots L, x ∈ F.val.fieldRange<GOAL>Splits (algebraMap K ↥F) p
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlroot : (cyclotomic l K).IsRoot x<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlroot : (cyclotomic l K).IsRoot x<VAR>hlzero : NeZero l<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlroot : (cyclotomic l K).IsRoot x<VAR>hlzero : NeZero l<VAR>this : NeZero ↑l<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlroot : IsPrimitiveRoot x l<VAR>hlzero : NeZero l<VAR>this : NeZero ↑l<GOAL>∃ r, x = (-ζ) ^ r
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁷ : CommRing A<VAR>inst✝⁶ : CommRing B<VAR>inst✝⁵ : Algebra A B<VAR>inst✝⁴ : IsCyclotomicExtension {n} A B<VAR>inst✝³ : Field K<VAR>inst✝² inst✝¹ : NumberField K<VAR>inst✝ : IsCyclotomicExtension {n} ℚ K<VAR>hno : Odd ↑n<VAR>ζ x : K<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>hx : IsOfFinOrder x<VAR>hnegζ : IsPrimitiveRoot (-ζ) (2 * ↑n)<VAR>k : ℕ<VAR>hkpos : 0 < k<VAR>hkn : x ^ k = 1<VAR>l : ℕ<VAR>hl : l ∈ k.divisors<VAR>hlroot : IsPrimitiveRoot x l<VAR>hlzero : NeZero l<VAR>this : NeZero ↑l<VAR>a : ℕ<VAR>ha : 2 * ↑n = l * a<GOAL>∃ r, x = (-ζ) ^ r