ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>inst✝⁵ : MetricSpace α<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>v : VitaliFamily μ<VAR>E : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : SecondCountableTopology α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : IsLocallyFiniteMeasure μ<VAR>ρ : Measure α<VAR>inst✝ : IsLocallyFiniteMeasure ρ<VAR>hρ : ρ ≪ μ<VAR>p q : ℝ≥0<VAR>hpq : p < q<VAR>s : Set α := {x | ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)}<VAR>o : ℕ → Set α := spanningSets (ρ + μ)<VAR>u : ℕ → Set α := fun n => s ∩ {x | v.limRatio ρ x < ↑p} ∩ o n<VAR>w : ℕ → Set α := fun n => s ∩ {x | ↑q < v.limRatio ρ x} ∩ o n<VAR>m n : ℕ<VAR>I : (ρ + μ) (u m) ≠ ⊤<VAR>J : (ρ + μ) (w n) ≠ ⊤<VAR>A : ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ↑p * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<VAR>B : ↑q * μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) ≤ ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))<VAR>h : ¬μ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) = 0<GOAL>ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n)) < ρ (toMeasurable (ρ + μ) (u m) ∩ toMeasurable (ρ + μ) (w n))
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>hST : IsComplement S T<VAR>hHT : IsComplement (↑H) T<VAR>hSK : IsComplement S ↑K<VAR>g : G<VAR>h1 : 1 ∈ S<GOAL>↑(hST.equiv g).1 = 1 ↔ g ∈ T
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>k : ℕ<VAR>f : R[X]<VAR>r : R<VAR>hk : 0 < k<GOAL>(hasseDeriv k) (C r) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in f ×ˢ g, p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<GOAL>(∀ᶠ (x : α × β) in map (fun p => (p.2, p.1)) (g ×ˢ f), p x) ↔ ∀ᶠ (y : β × α) in g ×ˢ f, p y.swap
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>f =o[𝓝 b] g ↔ (f ∘ ↑e) =o[𝓝 (↑e.symm b)] (g ∘ ↑e)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : TopologicalSpace β<VAR>E : Type u_3<VAR>inst✝¹ : Norm E<VAR>F : Type u_4<VAR>inst✝ : Norm F<VAR>e : PartialHomeomorph α β<VAR>b : β<VAR>hb : b ∈ e.target<VAR>f : β → E<VAR>g : β → F<GOAL>(∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 b) f g) ↔ ∀ ⦃c : ℝ⦄, 0 < c → IsBigOWith c (𝓝 (↑e.symm b)) (f ∘ ↑e) (g ∘ ↑e)
<VAR>ι : Type u_1<VAR>I✝ J I : Box ι<VAR>s t : Set ι<VAR>h : s ≠ t<GOAL>Disjoint ↑(I.splitCenterBox s) ↑(I.splitCenterBox t)
<VAR>ι : Type u_1<VAR>I✝ J I : Box ι<VAR>s t : Set ι<VAR>h : s ≠ t<GOAL>↑(I.splitCenterBox s) ⊓ ↑(I.splitCenterBox t) ≤ ⊥
<VAR>ι : Type u_1<VAR>I✝ J I : Box ι<VAR>s t : Set ι<VAR>h : s ≠ t<VAR>y : ι → ℝ<VAR>hs : y ∈ ↑(I.splitCenterBox s)<VAR>ht : y ∈ ↑(I.splitCenterBox t)<VAR>i : ι<GOAL>i ∈ s ↔ i ∈ t
<VAR>ι : Type u_1<VAR>I✝ J I : Box ι<VAR>s t : Set ι<VAR>h : s ≠ t<VAR>y : ι → ℝ<VAR>hs : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ s<VAR>ht : y ∈ I ∧ ∀ (i : ι), (I.lower i + I.upper i) / 2 < y i ↔ i ∈ t<VAR>i : ι<GOAL>i ∈ s ↔ i ∈ t
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w : V<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableRel G.Adj<VAR>inst✝ : DecidableEq V<VAR>c : G.ConnectedComponent<VAR>hM : M.IsPerfectMatching<GOAL>Even (Fintype.card ↑c.supp)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : Ring S<VAR>inst✝² : Algebra R S<VAR>m : Type u_3<VAR>inst✝¹ : Fintype m<VAR>inst✝ : DecidableEq m<VAR>b : Basis m R S<VAR>x x' : S<VAR>h : (leftMulMatrix b) x = (leftMulMatrix b) x'<GOAL>((lmul R S) x) 1 = ((lmul R S) x') 1
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝ : LinearOrder ι<VAR>f : Filtration ι m<VAR>τ π : Ω → ι<VAR>hτ : IsStoppingTime f τ<VAR>i : ι<VAR>this : {ω | i < τ ω} = {ω | τ ω ≤ i}ᶜ<GOAL>MeasurableSet {ω | τ ω ≤ i}ᶜ
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝¹⁷ : Semiring R₁<VAR>inst✝¹⁶ : Semiring R₂<VAR>inst✝¹⁵ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>M₁ : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M₁<VAR>inst✝¹³ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹² : TopologicalSpace M'₁<VAR>inst✝¹¹ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁰ : TopologicalSpace M₂<VAR>inst✝⁹ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝⁸ : TopologicalSpace M₃<VAR>inst✝⁷ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝⁶ : TopologicalSpace M₄<VAR>inst✝⁵ : AddCommMonoid M₄<VAR>inst✝⁴ : Module R₁ M₁<VAR>inst✝³ : Module R₁ M'₁<VAR>inst✝² : Module R₂ M₂<VAR>inst✝¹ : Module R₃ M₃<VAR>inst✝ : ContinuousAdd M₂<VAR>ι : Type u_9<VAR>t : Finset ι<VAR>f : ι → M₁ →SL[σ₁₂] M₂<GOAL>⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d)
<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✝ F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>k : K<GOAL>(isoOfEquivalence e w).hom ≫ limit.π G k = limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)
<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✝ F : J ⥤ C<VAR>inst✝¹ : HasLimit F<VAR>G : K ⥤ C<VAR>inst✝ : HasLimit G<VAR>e : J ≌ K<VAR>w : e.functor ⋙ G ≅ F<VAR>k : K<GOAL>(limit.isLimit G).lift ((Cones.equivalenceOfReindexing e.symm ((isoWhiskerLeft e.inverse w).symm ≪≫ e.invFunIdAssoc G)).functor.obj (limit.cone F)) ≫ limit.π G k = limit.π F (e.inverse.obj k) ≫ w.inv.app (e.inverse.obj k) ≫ G.map (e.counit.app k)
<VAR>K : Type u_1<VAR>E : Type u_2<VAR>inst✝ : RCLike K<VAR>z w : K<GOAL>z < 0 ↔ re z < 0 ∧ im z = 0
<VAR>α✝ : Type u<VAR>β : Type v<VAR>f✝ fa g : α✝ → α✝<VAR>x✝ y : α✝<VAR>fb : β → β<VAR>m n k : ℕ<VAR>e : Perm α✝<VAR>α : Type u_1<VAR>f : α → α<VAR>x : α<GOAL>x ∈ fixedPoints f ↔ f x = x
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : Weight K (↥H) L<GOAL>↑(corootSpace ⇑α) = span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : Weight K (↥H) L<GOAL>↑(corootSpace ⇑α) ≤ span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)}
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>L : Type u_3<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : LieRing L<VAR>inst✝⁷ : LieAlgebra R L<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : LieAlgebra K L<VAR>inst✝⁴ : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝³ : H.IsCartanSubalgebra<VAR>inst✝² : IsTriangularizable K (↥H) L<VAR>inst✝¹ : IsKilling K L<VAR>inst✝ : PerfectField K<VAR>α : Weight K (↥H) L<GOAL>span K {(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)} ≤ ↑(corootSpace ⇑α)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : ∀ (k : n), ∑ j ∈ Finset.univ.erase k, ‖A k j‖ < ‖A k k‖<GOAL>A.det ≠ 0
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : A.det = 0<GOAL>∃ k, ‖A k k‖ ≤ ∑ j ∈ Finset.univ.erase k, ‖A k j‖
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : A.det = 0<GOAL>∃ k, 0 ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : A.det = 0<GOAL>Module.End.HasEigenvalue (Matrix.toLin' A) 0
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>h : A.det = 0<GOAL>⊥ ≠ LinearMap.ker (Matrix.toLin' A)
<VAR>R : Type u_1<VAR>inst✝ : CommMonoidWithZero R<VAR>n : ℕ<VAR>χ✝ : DirichletCharacter R n<VAR>χ : DirichletCharacter R 1<VAR>a✝ : (ZMod 1)ˣ<GOAL>χ ↑a✝ = 1 ↑a✝
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<GOAL>C x hx
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<GOAL>∃ (h : x ∈ ⨆ i, S i), C x h
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x✝ : G<VAR>hx✝ : x✝ ∈ ⨆ i, S i<VAR>i : ι<VAR>x : G<VAR>hx : x ∈ S i<GOAL>(fun x => ∃ (h : x ∈ ⨆ i, S i), C x h) x
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x : G<VAR>hx : x ∈ ⨆ i, S i<GOAL>(fun x => ∃ (h : x ∈ ⨆ i, S i), C x h) 1
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>ι : Sort u_5<VAR>S : ι → Subgroup G<VAR>C : (x : G) → x ∈ ⨆ i, S i → Prop<VAR>hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯<VAR>h1 : C 1 ⋯<VAR>hmul : ∀ (x y : G) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯<VAR>x✝ : G<VAR>hx : x✝ ∈ ⨆ i, S i<VAR>x y : G<GOAL>(fun x => ∃ (h : x ∈ ⨆ i, S i), C x h) x → (fun x => ∃ (h : x ∈ ⨆ i, S i), C x h) y → (fun x => ∃ (h : x ∈ ⨆ i, S i), C x h) (x * y)
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<GOAL>Disjoint (LinearMap.range (ι R)) 1
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<GOAL>∀ x ∈ LinearMap.range (ι R), x ∈ 1 → x = 0
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x : M<VAR>r : R<VAR>hx : (ι R) x = (Algebra.linearMap R (TensorAlgebra R M)) r<GOAL>(Algebra.linearMap R (TensorAlgebra R M)) r = 0
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>M : Type u_2<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>x : M<VAR>r : R<VAR>hx : x = 0 ∧ r = 0<GOAL>(Algebra.linearMap R (TensorAlgebra R M)) r = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t s : Set α<GOAL>(⇑ofDual ⁻¹' s).OrdConnected ↔ s.OrdConnected
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>s✝ t s : Set α<GOAL>(∀ (x x_1 : { a // toDual a ∈ ⇑ofDual ⁻¹' s }), ⇑ofDual ⁻¹' Icc ↑x_1 ↑x ⊆ ⇑ofDual ⁻¹' s) ↔ ∀ (x x_1 : { a // a ∈ s }), Icc ↑x ↑x_1 ⊆ s
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>G : Cᵒᵖ<GOAL>IsCoseparator (unop G) ↔ IsSeparator G
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : LocallyConstant X (Fin 2)<VAR>h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}<GOAL>f = g
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : LocallyConstant X (Fin 2)<VAR>h : ∀ (x : X), f x = 0 ↔ g x = 0<GOAL>f = g
<VAR>X✝ : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>inst✝¹ : TopologicalSpace X✝<VAR>X : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>f g : LocallyConstant X (Fin 2)<VAR>h : ∀ (x : X), f x = 0 ↔ g x = 0<VAR>x : X<GOAL>f x = g x
<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 L<VAR>ζ✝ : L<VAR>hζ✝ : IsPrimitiveRoot ζ✝ ↑n<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K A<VAR>inst✝¹ : IsDomain A<VAR>ζ : A<VAR>inst✝ : IsCyclotomicExtension {n} K A<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>h : Irreducible (cyclotomic (↑n) K)<GOAL>minpoly K (ζ - 1) = (cyclotomic (↑n) K).comp (X + 1)
<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 L<VAR>ζ✝ : L<VAR>hζ✝ : IsPrimitiveRoot ζ✝ ↑n<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K A<VAR>inst✝¹ : IsDomain A<VAR>ζ : A<VAR>inst✝ : IsCyclotomicExtension {n} K A<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<GOAL>minpoly K (ζ - 1) = (cyclotomic (↑n) K).comp (X + 1)
<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 L<VAR>ζ✝ : L<VAR>hζ✝ : IsPrimitiveRoot ζ✝ ↑n<VAR>inst✝⁴ : Field K<VAR>inst✝³ : Algebra K L<VAR>inst✝² : Algebra K A<VAR>inst✝¹ : IsDomain A<VAR>ζ : A<VAR>inst✝ : IsCyclotomicExtension {n} K A<VAR>hζ : IsPrimitiveRoot ζ ↑n<VAR>h : Irreducible (cyclotomic (↑n) K)<VAR>this : NeZero ↑↑n<GOAL>(minpoly K ζ).comp (X - Polynomial.C (-1)) = (minpoly K ζ).comp (X + 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>s : Set α<VAR>hs : s.Nontrivial<GOAL>s.einfsep < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>r : 𝕜<GOAL>Tendsto (fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝³ : LinearOrderedField 𝕜<VAR>inst✝² : Archimedean 𝕜<VAR>inst✝¹ : TopologicalSpace 𝕜<VAR>inst✝ : OrderTopology 𝕜<VAR>r : 𝕜<GOAL>Tendsto (abs ∘ fun n => r ^ n) atTop (𝓝 0) ↔ |r| < 1
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a b c d : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hba : b < a<VAR>hdc : d < c<GOAL>a * d + b * c < a * c + b * d
<VAR>α : Type u<VAR>β : Type u_1<VAR>inst✝⁶ : Semiring α<VAR>inst✝⁵ : PartialOrder α<VAR>a b c d : α<VAR>inst✝⁴ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : MulPosStrictMono α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>inst✝ : ContravariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x < x_1<VAR>hba : b < a<VAR>hdc : d < c<GOAL>b * c + a * d < b * d + a * c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝¹ : SeminormedRing α<VAR>inst✝ : NormOneClass α<VAR>a : α<VAR>n : ℕ<GOAL>‖a ^ Nat.zero‖₊ ≤ ‖a‖₊ ^ Nat.zero
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<VAR>k'_comp : IsCompact k'<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<VAR>k'_comp : IsCompact k'<VAR>g' : P × G → G → E' := fun p x => g p.1 (p.2 - x)<VAR>s' : Set (P × G) := s ×ˢ t<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedAddCommGroup E'<VAR>inst✝¹³ : NormedAddCommGroup E''<VAR>inst✝¹² : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g✝ g'✝ : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>inst✝⁹ : NormedSpace 𝕜 E'<VAR>inst✝⁸ : NormedSpace 𝕜 E''<VAR>inst✝⁷ : NormedSpace 𝕜 F<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝⁶ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>inst✝⁵ : NormedSpace ℝ F<VAR>inst✝⁴ : AddGroup G<VAR>inst✝³ : TopologicalSpace G<VAR>inst✝² : TopologicalAddGroup G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : TopologicalSpace P<VAR>g : P → G → E'<VAR>s : Set P<VAR>k : Set G<VAR>hk : IsCompact k<VAR>hgs : ∀ (p : P) (x : G), p ∈ s → x ∉ k → g p x = 0<VAR>hf : LocallyIntegrable f μ<VAR>hg : ContinuousOn (↿g) (s ×ˢ univ)<VAR>H : ¬∀ p ∈ s, ∀ (x : G), g p x = 0<VAR>this : LocallyCompactSpace G<VAR>q₀ : P<VAR>x₀ : G<VAR>hq₀ : (q₀, x₀).1 ∈ s<VAR>t : Set G<VAR>t_comp : IsCompact t<VAR>ht : t ∈ 𝓝 x₀<VAR>k' : Set G := -k +ᵥ t<VAR>k'_comp : IsCompact k'<VAR>g' : P × G → G → E' := fun p x => g p.1 (p.2 - x)<VAR>s' : Set (P × G) := s ×ˢ t<VAR>A : ContinuousOn (uncurry g') (s' ×ˢ univ)<GOAL>ContinuousWithinAt (fun q => (f ⋆[L, μ] g q.1) q.2) (s ×ˢ univ) (q₀, x₀)