ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : ↑(chainBotCoeff (⇑α) β) < ↑n<GOAL>rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n + chainTopCoeff (⇑α) β<GOAL>rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : CharZero K<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra K L<VAR>inst✝³ : IsKilling K L<VAR>inst✝² : FiniteDimensional K L<VAR>H : LieSubalgebra K L<VAR>inst✝¹ : H.IsCartanSubalgebra<VAR>inst✝ : IsTriangularizable K (↥H) L<VAR>α β : Weight K (↥H) L<VAR>hα : α.IsNonZero<VAR>n : ℕ<VAR>hn : chainLength α β < n + chainTopCoeff (⇑α) β<VAR>this : rootSpace H (-((n + chainTopCoeff (⇑α) β) • ⇑α) + ⇑(chainTop (⇑α) β)) = ⊥<GOAL>rootSpace H (-↑n • ⇑α + ⇑β) = ⊥
<VAR>R : Type u_1<VAR>n : ℤ<GOAL>Squarefree n.natAbs ↔ Squarefree n
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i j : ℕ<VAR>w : ¬(ComplexShape.up ℕ).Rel i j<GOAL>(fun i j => C.d (i + 1) (j + 1)) i j = 0
<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>C : CochainComplex V ℕ<VAR>i j : ℕ<VAR>w : ¬(ComplexShape.up ℕ).Rel i j<GOAL>¬(ComplexShape.up ℕ).Rel (i + 1) (j + 1)
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : LindelofSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>IsLindelof univ
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>h : LindelofSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<GOAL>IsLindelof (range f)
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>(a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>(a + b) % c + a % c + b % c + c * ((a + b) / c) = (a + b) % c + a % c + b % c + c * (a / c + b / c + if c ≤ a % c + b % c then 1 else 0)
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>(a + b) % c + c * ((a + b) / c) + a % c + b % c = (a % c + c * (a / c) + (b % c + c * (b / c)) + c * if c ≤ a % c + b % c then 1 else 0) + (a + b) % c
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>a + (b + (a % c + b % c)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) = (a + b + if c ≤ a % c + b % c then c * 1 else c * 0) + (a + b) % c
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : 0 < c<GOAL>a + (b + ((a + b) % c + if c ≤ a % c + b % c then c else 0)) = (a + b + if c ≤ a % c + b % c then c else 0) + (a + b) % c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LT α<VAR>inst✝ : LT β<VAR>s t : Set α<VAR>l : List α<VAR>a : α<VAR>n m : ℕ<GOAL>↑n ≤ s.chainHeight + ↑m ↔ ∃ l ∈ s.subchain, n ≤ l.length + m
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>MDifferentiableAt 𝓘(𝕜, E) 𝓘(𝕜, E') f x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>E' : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : E → E'<VAR>s : Set E<VAR>x : E<GOAL>ContinuousAt f x ∧ DifferentiableAt 𝕜 f x ↔ DifferentiableAt 𝕜 f x
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.4974<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<GOAL>MeasurableSpace.comap (Function.eval i) (m i) ≤ MeasurableSpace.generateFrom ((fun t => {i}.pi t) '' univ.pi fun i => {s | MeasurableSet s})
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.4974<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<GOAL>MeasurableSpace.comap (Function.eval i) (m i) ≤ MeasurableSpace.generateFrom ((fun a => Function.eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.4974<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<GOAL>MeasurableSpace.generateFrom {t | ∃ s, MeasurableSet s ∧ Function.eval i ⁻¹' s = t} ≤ MeasurableSpace.generateFrom ((fun a => Function.eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s})
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.4974<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<VAR>S : Set ((x : ι) → α x)<GOAL>S ∈ {t | ∃ s, MeasurableSet s ∧ Function.eval i ⁻¹' s = t} → S ∈ (fun a => Function.eval i ⁻¹' a i) '' univ.pi fun i => {s | MeasurableSet s}
<VAR>ι : Type u_2<VAR>α✝ : ι → Type ?u.4974<VAR>α : ι → Type u_1<VAR>m : (i : ι) → MeasurableSpace (α i)<VAR>i : ι<VAR>S : Set ((x : ι) → α x)<GOAL>∀ (x : Set (α i)), MeasurableSet x → Function.eval i ⁻¹' x = S → ∃ x, (∀ (i : ι), MeasurableSet (x i)) ∧ Function.eval i ⁻¹' x i = S
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a i : M<VAR>l : List M<VAR>hil : (∀ x ∈ l, x = 1) → l.prod = 1<VAR>hl : ∀ x ∈ i :: l, x = 1<GOAL>(i :: l).prod = 1
<VAR>S : Type u_1<VAR>R R' : Type u<VAR>M : Type v<VAR>inst✝¹⁸ : CommSemiring S<VAR>inst✝¹⁷ : Semiring R<VAR>inst✝¹⁶ : CommSemiring R'<VAR>inst✝¹⁵ : AddCommMonoid M<VAR>inst✝¹⁴ : Algebra S R<VAR>inst✝¹³ : Algebra S R'<VAR>inst✝¹² : Module S M<VAR>inst✝¹¹ : Module R M<VAR>inst✝¹⁰ : Module Rᵐᵒᵖ M<VAR>inst✝⁹ : SMulCommClass R Rᵐᵒᵖ M<VAR>inst✝⁸ : IsScalarTower S R M<VAR>inst✝⁷ : IsScalarTower S Rᵐᵒᵖ M<VAR>inst✝⁶ : Module R' M<VAR>inst✝⁵ : Module R'ᵐᵒᵖ M<VAR>inst✝⁴ : IsCentralScalar R' M<VAR>inst✝³ : IsScalarTower S R' M<VAR>A : Type u_2<VAR>inst✝² : Semiring A<VAR>inst✝¹ : Algebra S A<VAR>inst✝ : Algebra R' A<VAR>f : R →ₐ[S] A<VAR>g : M →ₗ[S] A<VAR>hg : ∀ (x y : M), g x * g y = 0<VAR>hfg : ∀ (r : R) (x : M), g (r •> x) = f r * g x<VAR>hgf : ∀ (r : R) (x : M), g (x <• r) = g x * f r<VAR>m : M<GOAL>f 0 + g m = g m
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹² : NormedAddCommGroup E<VAR>inst✝¹¹ : NormedSpace ℝ E<VAR>hE : CompleteSpace E<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : SMulCommClass ℝ 𝕜 E<VAR>inst✝⁷ : NormedAddCommGroup F<VAR>inst✝⁶ : NormedSpace ℝ F<VAR>inst✝⁵ : CompleteSpace F<VAR>G : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>f✝ g : α → E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>X : Type u_6<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>ν : Measure α<VAR>inst✝ : MeasurableSpace α<VAR>f : α → E<VAR>a : α<VAR>hfm : StronglyMeasurable f<VAR>this✝¹ : MeasurableSpace E := borel E<VAR>this✝ : BorelSpace E<GOAL>∫ (x : α), f x ∂Measure.dirac a = f a
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<GOAL>Tendsto (fun p => ∑ i : α, a i * b i ^ p) atBot atTop
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop<GOAL>Tendsto (fun p => ∑ i : α, a i * b i ^ p) atBot atTop
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop<VAR>p : ℝ<GOAL>a (max_bi b) * b (max_bi b) ^ p ≤ ∑ i : α, a i * b i ^ p
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop<VAR>p : ℝ<VAR>i : α<VAR>x✝ : i ∈ univ<GOAL>0 ≤ (fun i => a i * b i ^ p) i
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop<VAR>p : ℝ<VAR>i : α<VAR>x✝ : i ∈ univ<VAR>h₁ : 0 < a i<GOAL>0 ≤ (fun i => a i * b i ^ p) i
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>h₁✝ : Tendsto (fun p => a (max_bi b) * b (max_bi b) ^ p) atBot atTop<VAR>p : ℝ<VAR>i : α<VAR>x✝ : i ∈ univ<VAR>h₁ : 0 < a i<VAR>h₂ : 0 < b i<GOAL>0 ≤ (fun i => a i * b i ^ p) i
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H K : Subgroup G<VAR>S T : Set G<VAR>h : IsComplement S T<VAR>x : G<GOAL>x ∈ S * T
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hom : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : TopologicalGroup α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group β<VAR>inst✝¹ : FunLike hom β α<VAR>inst✝ : MonoidHomClass hom β α<VAR>e : hom<VAR>de : DenseInducing ⇑e<VAR>x₀ : α<GOAL>Tendsto (fun t => t.2 / t.1) (comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hom : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : TopologicalGroup α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group β<VAR>inst✝¹ : FunLike hom β α<VAR>inst✝ : MonoidHomClass hom β α<VAR>e : hom<VAR>de : DenseInducing ⇑e<VAR>x₀ : α<VAR>comm : ((fun x => x.2 / x.1) ∘ fun t => (e t.1, e t.2)) = ⇑e ∘ fun t => t.2 / t.1<GOAL>Tendsto (fun t => t.2 / t.1) (comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>hom : Type u_3<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : Group α<VAR>inst✝⁴ : TopologicalGroup α<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : Group β<VAR>inst✝¹ : FunLike hom β α<VAR>inst✝ : MonoidHomClass hom β α<VAR>e : hom<VAR>de : DenseInducing ⇑e<VAR>x₀ : α<VAR>comm : ((fun x => x.2 / x.1) ∘ fun t => (e t.1, e t.2)) = ⇑e ∘ fun t => t.2 / t.1<VAR>lim : Tendsto (fun x => x.2 / x.1) (𝓝 (x₀, x₀)) (𝓝 (e 1))<GOAL>Tendsto (fun t => t.2 / t.1) (comap (fun p => (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
<VAR>R✝ : Type u_1<VAR>inst✝³ : CommRing R✝<VAR>inst✝² : IsDomain R✝<VAR>n : ℕ<VAR>R : Type u_2<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<GOAL>(∏ μ ∈ primitiveRoots n R, (X - C μ)).roots = (primitiveRoots n R).val
<GOAL>∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)
<VAR>c : ℝ<VAR>h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))<GOAL>∃ a, 0 < a ∧ ∀ (n : ℕ), a ≤ stirlingSeq (n + 1)
<VAR>c : ℝ<VAR>h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))<VAR>n : ℕ<GOAL>rexp c ≤ stirlingSeq (n + 1)
<VAR>c : ℝ<VAR>h : ∀ (n : ℕ), c ≤ Real.log (stirlingSeq (n + 1))<VAR>n : ℕ<GOAL>c ≤ Real.log (stirlingSeq (n + 1))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<VAR>hp_pos_real : 0 < p.toReal<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<VAR>hp_pos_real : 0 < p.toReal<VAR>hf_eLpNorm : eLpNorm (↑f) p μ < ⊤<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<VAR>hp_pos_real : 0 < p.toReal<VAR>hf_eLpNorm : ∀ a ∈ f.range, ↑‖a‖₊ ^ p.toReal * μ (↑f ⁻¹' {a}) < ⊤<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<VAR>hp_pos_real : 0 < p.toReal<VAR>hyf : y ∈ f.range<VAR>hf_eLpNorm : ↑‖y‖₊ ^ p.toReal * μ (↑f ⁻¹' {y}) < ⊤<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>𝕜 : Type u_6<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedAddCommGroup F<VAR>μ : Measure α<VAR>p : ℝ≥0∞<VAR>hp_pos : p ≠ 0<VAR>hp_ne_top : p ≠ ⊤<VAR>f : α →ₛ E<VAR>hf : Memℒp (↑f) p μ<VAR>y : E<VAR>hy_ne : y ≠ 0<VAR>hp_pos_real : 0 < p.toReal<VAR>hyf : y ∈ f.range<VAR>hf_eLpNorm : ↑‖y‖₊ ^ p.toReal < ⊤ ∧ μ (↑f ⁻¹' {y}) < ⊤ ∨ ↑‖y‖₊ ^ p.toReal = 0 ∨ μ (↑f ⁻¹' {y}) = 0<GOAL>μ (↑f ⁻¹' {y}) < ⊤
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M : Type u_2<VAR>inst✝⁸ : AddCommMonoid M<VAR>inst✝⁷ : Module R M<VAR>N : Type u_3<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R N<VAR>ι : Type u_4<VAR>inst✝⁴ : DecidableEq ι<VAR>S : Type u_5<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>inst✝¹ : Module S M<VAR>inst✝ : IsScalarTower R S M<VAR>i : ι<VAR>n : N<GOAL>(finsuppScalarLeft R N ι).symm (Finsupp.single i n) = Finsupp.single i 1 ⊗ₜ[R] n
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (z : ℂ) in 𝓝[≠] c, DifferentiableAt ℂ f z<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<GOAL>Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<GOAL>Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})<GOAL>Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x<VAR>ho : (fun z => f z - f c) =o[𝓝[≠] c] fun z => (z - c)⁻¹<VAR>this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})<VAR>H : DifferentiableOn ℂ (update f c (limUnder (𝓝[≠] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}<GOAL>Tendsto f (𝓝[≠] c) (𝓝 (limUnder (𝓝[≠] c) f))
<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>z : ℤ<GOAL>¬p ∣ (↑z).den
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x✝ : α<VAR>inst✝² : AddMonoid α<VAR>inst✝¹ : Group γ<VAR>inst✝ : DistribMulAction γ α<VAR>h : Periodic f c<VAR>a : γ<VAR>x : α<GOAL>(fun x => f (a • x)) (x + a⁻¹ • c) = (fun x => f (a • x)) x
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid β<VAR>S : Multiset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<GOAL>(map g1 S).prod ∣ (map g2 S).prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid β<VAR>S : Multiset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<GOAL>(map g1 0).prod ∣ (map g2 0).prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid β<VAR>S : Multiset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<GOAL>∀ {a : α} {s : Multiset α}, a ∈ S → s ⊆ S → (map g1 s).prod ∣ (map g2 s).prod → (map g1 (insert a s)).prod ∣ (map g2 (insert a s)).prod
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid β<VAR>S : Multiset α<VAR>g1 g2 : α → β<VAR>h : ∀ a ∈ S, g1 a ∣ g2 a<VAR>a : α<VAR>T : Multiset α<VAR>haS : a ∈ S<VAR>a✝ : T ⊆ S<VAR>IH : (map g1 T).prod ∣ (map g2 T).prod<GOAL>(map g1 (insert a T)).prod ∣ (map g2 (insert a T)).prod
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f : MonoidAlgebra R M<GOAL>∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>m : M<GOAL>∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = (of R M) m
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>f g : MonoidAlgebra R M<VAR>ihf : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f<VAR>ihg : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = g<GOAL>∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f + g
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommMonoid M<VAR>inst✝ : CommSemiring R<VAR>S : Set M<VAR>hS : closure S = ⊤<VAR>r : R<VAR>f : MonoidAlgebra R M<VAR>ih : ∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = f<GOAL>∃ a, (MvPolynomial.aeval fun s => (of R M) ↑s) a = r • f
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>s : Set α<VAR>h : Ici a ⊆ s<GOAL>map Subtype.val atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>s : Set α<VAR>h : Ici a ⊆ s<VAR>this : Nonempty ↑s<GOAL>map Subtype.val atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>s : Set α<VAR>h : Ici a ⊆ s<VAR>this✝ : Nonempty ↑s<VAR>this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)<GOAL>map Subtype.val atTop = atTop
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : SemilatticeSup α<VAR>a : α<VAR>s : Set α<VAR>h : Ici a ⊆ s<VAR>this✝ : Nonempty ↑s<VAR>this : Directed (fun x x_1 => x ≥ x_1) fun x => 𝓟 (Ici x)<GOAL>(∀ (i : α), Ici i ∈ ⨅ i, 𝓟 (Subtype.val '' Ici i)) ∧ ∀ (i : ↑s), Subtype.val '' Ici i ∈ ⨅ a, 𝓟 (Ici a)
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>↑(den A r) ∣ p.leadingCoeff
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>↑(den A r) ∣ p.leadingCoeff * num A r ^ p.natDegree
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>↑(den A r) ∣ (p.scaleRoots ?s).coeff p.natDegree * num A r ^ p.natDegree
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>A
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<GOAL>∀ (j : ℕ), j ≠ p.natDegree → ↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ p.natDegree<VAR>h : ¬j < p.natDegree<GOAL>↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ (p.scaleRoots ↑(den A r)).natDegree<VAR>h : ¬j < (p.scaleRoots ↑(den A r)).natDegree<GOAL>↑(den A r) ∣ (p.scaleRoots ↑(den A r)).coeff j * num A r ^ j
<VAR>A : Type u_1<VAR>K : Type u_2<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : IsDomain A<VAR>inst✝³ : UniqueFactorizationMonoid A<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra A K<VAR>inst✝ : IsFractionRing A K<VAR>p : A[X]<VAR>r : K<VAR>hr : (aeval r) p = 0<VAR>j : ℕ<VAR>hj : j ≠ (p.scaleRoots ↑(den A r)).natDegree<VAR>h : ¬j < (p.scaleRoots ↑(den A r)).natDegree<GOAL>↑(den A r) ∣ 0
<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✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α.IsNonZero<GOAL>α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) ≠ 0
<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✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = 0<GOAL>¬α.IsNonZero
<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✝ : CharZero K<VAR>α : Weight K (↥H) L<VAR>hα : α ((cartanEquivDual H).symm (Weight.toLinear K (↥H) L α)) = 0<GOAL>(cartanEquivDual H).symm (Weight.toLinear K (↥H) L α) ∈ Weight.ker ⊓ (lieIdealSubalgebra K (↥H) (corootSpace ⇑α)).toSubmodule
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>δ : Type u_5<VAR>ε : Type u_6<VAR>inst✝ : Monoid α<VAR>f g : Filter α<VAR>s : Set α<VAR>a : α<VAR>m n✝ n : ℕ<VAR>hn : n ≠ 0<GOAL>⊥ ^ n = ⊥