ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>S : Set (HeightOneSpectrum R)<VAR>K : Type v<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : (↥(S.integer K))ˣ<VAR>v : HeightOneSpectrum R<VAR>hv : v ∉ S<GOAL>v.valuation ↑(Units.mk0 ↑↑x ⋯) * v.valuation ↑x.inv = 1
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>ι : Type u_4<VAR>inst✝³ : DivisionRing k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>p : Fin 3 → P<GOAL>Collinear k (Set.range p) ↔ ¬AffineIndependent k p
<VAR>V : Type u_1<VAR>V₁ : Type u_2<VAR>V₂ : Type u_3<VAR>V₃ : Type u_4<VAR>inst✝³ : SeminormedAddCommGroup V<VAR>inst✝² : SeminormedAddCommGroup V₁<VAR>inst✝¹ : SeminormedAddCommGroup V₂<VAR>inst✝ : SeminormedAddCommGroup V₃<VAR>f g : NormedAddGroupHom V₁ V₂<VAR>K : ℝ≥0<VAR>h : ∀ (x : V₁), ‖x‖ ≤ ↑K * ‖f x‖<VAR>x y : V₁<GOAL>dist x y ≤ ↑K * dist (f x) (f y)
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f g : R⟦X⟧<VAR>m : ℕ<GOAL>(trunc n (↑(trunc n f) * g)).coeff m = (trunc n (f * g)).coeff m
<VAR>R✝ : Type u_1<VAR>R : Type u_2<VAR>inst✝ : CommSemiring R<VAR>n : ℕ<VAR>f g : R⟦X⟧<VAR>m : ℕ<GOAL>(if m < n then (coeff R m) (↑(trunc n f) * g) else 0) = if m < n then (coeff R m) (f * g) else 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<GOAL>(a :: l).toFinset.val = (insert a l.toFinset).val
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>E : Type u_4<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>ℱ : Filtration ι m<VAR>f : ι → Ω → E<VAR>μ : Measure Ω<VAR>h : ∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))<GOAL>StronglyMeasurable (Classical.choose h)
<VAR>Ω : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>m : MeasurableSpace Ω<VAR>inst✝⁵ : TopologicalSpace β<VAR>inst✝⁴ : MetrizableSpace β<VAR>mβ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : Preorder ι<VAR>E : Type u_4<VAR>inst✝¹ : Zero E<VAR>inst✝ : TopologicalSpace E<VAR>ℱ : Filtration ι m<VAR>f : ι → Ω → E<VAR>μ : Measure Ω<VAR>h : ¬∃ g, StronglyMeasurable g ∧ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n => f n ω) atTop (𝓝 (g ω))<GOAL>StronglyMeasurable 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t : Set α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on f)<VAR>h : ∀ (i : ι), NullMeasurableSet (f i) μ<GOAL>μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s t✝ : Set α<VAR>inst✝ : Countable ι<VAR>f : ι → Set α<VAR>hd : Pairwise (AEDisjoint μ on f)<VAR>h : ∀ (i : ι), NullMeasurableSet (f i) μ<VAR>t : ι → Set α<VAR>_ht_sub : ∀ (i : ι), t i ⊆ f i<VAR>ht_eq : ∀ (i : ι), f i =ᶠ[ae μ] t i<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>htd : Pairwise (Disjoint on t)<GOAL>μ (⋃ i, f i) = ∑' (i : ι), μ (f i)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ ν : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedAddCommGroup G<VAR>f : ↥(Lp E 0 μ)<GOAL>‖f‖ = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<GOAL>Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Tendsto (fun a => ⟪y, (f a) x⟫_𝕜) l (𝓝 ⟪y, A x⟫_𝕜)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁶ : RCLike 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace 𝕜 F<VAR>inst✝ : CompleteSpace F<VAR>α : Type u_4<VAR>l : Filter α<VAR>f : α → E →WOT[𝕜]F<VAR>A : E →WOT[𝕜]F<GOAL>Tendsto f l (𝓝 A) ↔ ∀ (x : E) (y : F), Tendsto (fun a => ((InnerProductSpace.toDual 𝕜 F) y) ((f a) x)) l (𝓝 (((InnerProductSpace.toDual 𝕜 F) y) (A x)))
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : SemilatticeSup α<VAR>a b c d : α<GOAL>a ⊔ b ≤ a ∧ a ≤ a ⊔ b ↔ b ≤ a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>A' : Type u_1<VAR>B : Type u_2<VAR>a b : R<VAR>n : ℕ<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : CommSemiring A'<VAR>inst✝⁴ : Semiring B<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra R A'<VAR>inst✝¹ : Algebra R B<VAR>p q : R[X]<VAR>x : A<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<VAR>r : R<VAR>h : eval₂ f (f r) p = 0<GOAL>f (eval r p) = f 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p q : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<GOAL>∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<GOAL>∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<GOAL>∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<GOAL>∃ a b, 0 < b ∧ ∀ x ∈ corootSpace α, (a • α + b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<GOAL>(a • α + ↑b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<VAR>N : ℤ → Submodule R M := fun k => ↑(weightSpace M (k • α + χ))<GOAL>(a • α + ↑b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<VAR>N : ℤ → Submodule R M := fun k => ↑(weightSpace M (k • α + χ))<VAR>h₁ : CompleteLattice.Independent fun i => N ↑i<GOAL>(a • α + ↑b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<VAR>N : ℤ → Submodule R M := fun k => ↑(weightSpace M (k • α + χ))<VAR>h₁ : CompleteLattice.Independent fun i => N ↑i<VAR>h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)<GOAL>(a • α + ↑b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<VAR>N : ℤ → Submodule R M := fun k => ↑(weightSpace M (k • α + χ))<VAR>h₁ : CompleteLattice.Independent fun i => N ↑i<VAR>h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)<VAR>h₃ : ↑(weightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, N i<GOAL>(a • α + ↑b • χ) x = 0
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹³ : CommRing R<VAR>inst✝¹² : LieRing L<VAR>inst✝¹¹ : LieAlgebra R L<VAR>M : Type u_3<VAR>inst✝¹⁰ : AddCommGroup M<VAR>inst✝⁹ : Module R M<VAR>inst✝⁸ : LieRingModule L M<VAR>inst✝⁷ : LieModule R L M<VAR>H : LieSubalgebra R L<VAR>α χ : ↥H → R<VAR>p✝ q✝ : ℤ<VAR>inst✝⁶ : H.IsCartanSubalgebra<VAR>inst✝⁵ : IsNoetherian R L<VAR>inst✝⁴ : IsDomain R<VAR>inst✝³ : IsPrincipalIdealRing R<VAR>inst✝² : CharZero R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>hα : α ≠ 0<VAR>hχ : weightSpace M χ ≠ ⊥<VAR>p : ℤ<VAR>hp₀ : p < 0<VAR>q : ℤ<VAR>hq₀ : q > 0<VAR>hp : weightSpace M (p • α + χ) = ⊥<VAR>hq : weightSpace M (q • α + χ) = ⊥<VAR>a : ℤ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ)) • i<VAR>b : ℕ := ∑ i ∈ Finset.Ioo p q, finrank R ↥↑(weightSpace M (i • α + χ))<VAR>hb : 0 < b<VAR>x : ↥H<VAR>hx : x ∈ corootSpace α<VAR>N : ℤ → Submodule R M := fun k => ↑(weightSpace M (k • α + χ))<VAR>h₁ : CompleteLattice.Independent fun i => N ↑i<VAR>h₂ : ∀ (i : ℤ), MapsTo ⇑((toEnd R (↥H) M) x) ↑(N i) ↑(N i)<VAR>h₃ : ↑(weightSpaceChain M α χ p q) = ⨆ i ∈ Finset.Ioo p q, N i<GOAL>(a • α + ↑b • χ) x = ∑ i ∈ Finset.Ioo p q, (LinearMap.trace R ↥(N i)) (LinearMap.restrict ((toEnd R (↥H) M) x) ⋯)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝¹ : Ring R<VAR>a b : R<VAR>n : ℕ<VAR>inst✝ : NoZeroDivisors R<GOAL>a ^ 2 = 1 ↔ a = 1 ∨ a = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a : ι → ℝ≥0∞<VAR>s : Finset ι<VAR>h : ∀ i ∈ s, Tendsto (f i) x (𝓝 (a i))<VAR>h' : ∀ i ∈ s, a i ≠ ⊤<GOAL>Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a : ι → ℝ≥0∞<VAR>h : ∀ i ∈ ∅, Tendsto (f i) x (𝓝 (a i))<VAR>h' : ∀ i ∈ ∅, a i ≠ ⊤<GOAL>Tendsto (fun b => ∏ c ∈ ∅, f c b) x (𝓝 (∏ c ∈ ∅, a c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝¹ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a✝ : ι → ℝ≥0∞<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>IH : (∀ i ∈ s, Tendsto (f i) x (𝓝 (a✝ i))) → (∀ i ∈ s, a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a✝ c))<VAR>h : ∀ i ∈ insert a s, Tendsto (f i) x (𝓝 (a✝ i))<VAR>h' : ∀ i ∈ insert a s, a✝ i ≠ ⊤<GOAL>Tendsto (fun b => ∏ c ∈ insert a s, f c b) x (𝓝 (∏ c ∈ insert a s, a✝ c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝¹ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a✝ : ι → ℝ≥0∞<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>IH : (∀ i ∈ s, Tendsto (f i) x (𝓝 (a✝ i))) → (∀ i ∈ s, a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a✝ c))<VAR>h : ∀ i ∈ insert a s, Tendsto (f i) x (𝓝 (a✝ i))<VAR>h' : ∀ i ∈ insert a s, a✝ i ≠ ⊤<GOAL>Tendsto (fun b => f a b * ∏ c ∈ s, f c b) x (𝓝 (a✝ a * ∏ c ∈ s, a✝ c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝¹ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a✝ : ι → ℝ≥0∞<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>IH : (∀ i ∈ s, Tendsto (f i) x (𝓝 (a✝ i))) → (∀ i ∈ s, a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a✝ c))<VAR>h : ∀ i ∈ insert a s, Tendsto (f i) x (𝓝 (a✝ i))<VAR>h' : ∀ i ∈ insert a s, a✝ i ≠ ⊤<GOAL>a✝ a ≠ 0 ∨ ∏ c ∈ s, a✝ c ≠ ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝¹ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a✝ : ι → ℝ≥0∞<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>IH : (∀ i ∈ s, Tendsto (f i) x (𝓝 (a✝ i))) → (∀ i ∈ s, a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a✝ c))<VAR>h : ∀ i ∈ insert a s, Tendsto (f i) x (𝓝 (a✝ i))<VAR>h' : ∀ i ∈ insert a s, a✝ i ≠ ⊤<GOAL>Tendsto (fun a => ∏ c ∈ s, f c a) x (𝓝 (∏ c ∈ s, a✝ c))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>a✝¹ b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>x✝ y z ε ε₁ ε₂ : ℝ≥0∞<VAR>s✝ : Set ℝ≥0∞<VAR>ι : Type u_4<VAR>f : ι → α → ℝ≥0∞<VAR>x : Filter α<VAR>a✝ : ι → ℝ≥0∞<VAR>a : ι<VAR>s : Finset ι<VAR>has : a ∉ s<VAR>IH : (∀ i ∈ s, Tendsto (f i) x (𝓝 (a✝ i))) → (∀ i ∈ s, a✝ i ≠ ⊤) → Tendsto (fun b => ∏ c ∈ s, f c b) x (𝓝 (∏ c ∈ s, a✝ c))<VAR>h : ∀ i ∈ insert a s, Tendsto (f i) x (𝓝 (a✝ i))<VAR>h' : ∀ i ∈ insert a s, a✝ i ≠ ⊤<GOAL>∏ c ∈ s, a✝ c ≠ 0 ∨ a✝ a ≠ ⊤
<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>p : ι →₀ M<VAR>n : N<VAR>i : ι<GOAL>((finsuppLeft R M N ι) (p ⊗ₜ[R] n)) i = p i ⊗ₜ[R] n
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝⁵ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>n p : ℕ<VAR>inst✝⁴ : Module.Free R ↑S.X₁<VAR>inst✝³ : Module.Free R ↑S.X₃<VAR>inst✝² : Module.Finite R ↑S.X₁<VAR>inst✝¹ : Module.Finite R ↑S.X₃<VAR>hN : FiniteDimensional.finrank R ↑S.X₁ = n<VAR>hP : FiniteDimensional.finrank R ↑S.X₃ = p<VAR>inst✝ : StrongRankCondition R<GOAL>FiniteDimensional.finrank R ↑S.X₂ = n + p
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝⁵ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>n p : ℕ<VAR>inst✝⁴ : Module.Free R ↑S.X₁<VAR>inst✝³ : Module.Free R ↑S.X₃<VAR>inst✝² : Module.Finite R ↑S.X₁<VAR>inst✝¹ : Module.Finite R ↑S.X₃<VAR>hN : FiniteDimensional.finrank R ↑S.X₁ = n<VAR>hP : FiniteDimensional.finrank R ↑S.X₃ = p<VAR>inst✝ : StrongRankCondition R<GOAL>Module.rank R ↑S.X₂ = ↑(n + p)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>inst✝⁵ : Ring R<VAR>S : ShortComplex (ModuleCat R)<VAR>hS : S.Exact<VAR>hS' : S.ShortExact<VAR>v : ι → ↑S.X₁<VAR>n p : ℕ<VAR>inst✝⁴ : Module.Free R ↑S.X₁<VAR>inst✝³ : Module.Free R ↑S.X₃<VAR>inst✝² : Module.Finite R ↑S.X₁<VAR>inst✝¹ : Module.Finite R ↑S.X₃<VAR>hN : FiniteDimensional.finrank R ↑S.X₁ = n<VAR>hP : FiniteDimensional.finrank R ↑S.X₃ = p<VAR>inst✝ : StrongRankCondition R<GOAL>Module.rank R ↑S.X₁ + Module.rank R ↑S.X₃ = ↑(FiniteDimensional.finrank R ↑S.X₁ + FiniteDimensional.finrank R ↑S.X₃)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>h : ∀ i ∈ l, ContinuousOn (f i) t<VAR>x : X<VAR>hx : x ∈ t<GOAL>ContinuousWithinAt (fun a => (List.map (fun i => f i a) l).prod) t x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>h : ∀ i ∈ l, ContinuousOn (f i) t<VAR>x : X<VAR>hx : x ∈ t<GOAL>ContinuousAt (t.restrict fun a => (List.map (fun i => f i a) l).prod) ⟨x, hx⟩
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>h : ∀ i ∈ l, ContinuousOn (f i) t<VAR>x : X<VAR>hx : x ∈ t<VAR>i : ι<VAR>hi : i ∈ l<GOAL>Tendsto (fun b => f i ↑b) (𝓝 ⟨x, hx⟩) (𝓝 (f i ↑⟨x, hx⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>x : X<VAR>hx : x ∈ t<VAR>i : ι<VAR>hi : i ∈ l<VAR>h : ContinuousWithinAt (f i) t x<GOAL>Tendsto (fun b => f i ↑b) (𝓝 ⟨x, hx⟩) (𝓝 (f i ↑⟨x, hx⟩))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>X : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace M<VAR>inst✝¹ : Monoid M<VAR>inst✝ : ContinuousMul M<VAR>f : ι → X → M<VAR>l : List ι<VAR>t : Set X<VAR>x : X<VAR>hx : x ∈ t<VAR>i : ι<VAR>hi : i ∈ l<VAR>h : ContinuousAt (t.restrict (f i)) ⟨x, hx⟩<GOAL>Tendsto (fun b => f i ↑b) (𝓝 ⟨x, hx⟩) (𝓝 (f i ↑⟨x, hx⟩))
<VAR>X : Type u_1<VAR>X' : Type u_2<VAR>Y : Type u_3<VAR>Y' : Type u_4<VAR>Z : Type u_5<VAR>Z' : Type u_6<VAR>inst✝⁵ : TopologicalSpace X<VAR>inst✝⁴ : TopologicalSpace X'<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Y'<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace Z'<VAR>e : PartialHomeomorph X Y<VAR>eX eX' : PartialHomeomorph X X'<VAR>eY eY' : PartialHomeomorph Y Y'<VAR>h : (eX.prod eY).source.Nonempty<VAR>x : X<VAR>y : Y<VAR>this✝² : Nonempty X<VAR>this✝¹ : Nonempty X'<VAR>this✝ : Nonempty Y<VAR>this : Nonempty Y'<GOAL>eX.prod eY = eX'.prod eY' ↔ eX = eX' ∧ eY = eY'
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 0<GOAL>∃ n, ∀ (z : ℍ), g • z = T ^ n • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 0<VAR>had : (↑g).det = 1<GOAL>∃ n, ∀ (z : ℍ), g • z = T ^ n • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 0<VAR>had : ↑g 0 0 * ↑g 1 1 = 1<GOAL>∃ n, ∀ (z : ℍ), g • z = T ^ n • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 0<VAR>had : ↑g 0 0 * ↑g 1 1 = 1<VAR>ha : ↑g 0 0 = 1<VAR>hd : ↑g 1 1 = 1<GOAL>∃ n, ∀ (z : ℍ), g • z = T ^ n • z
<VAR>g : SL(2, ℤ)<VAR>z : ℍ<VAR>hc : ↑g 1 0 = 0<VAR>had : ↑g 0 0 * ↑g 1 1 = 1<VAR>ha : ↑g 0 0 = -1<VAR>hd : ↑g 1 1 = -1<GOAL>∃ n, ∀ (z : ℍ), g • z = T ^ n • z
<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>m₁ m₂ m₃ : M<VAR>X : C<GOAL>(F.obj m₃).map ((F.μIso m₁ m₂).inv.app X) = (F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.μIso m₁ (m₂ ⊗ m₃)).inv.app X ≫ (F.μIso m₂ m₃).inv.app ((F.obj m₁).obj 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>m₁ m₂ m₃ : M<VAR>X : C<GOAL>inv ((F.obj m₃).map ((F.μIso m₁ m₂).inv.app X)) = inv ((F.μ (m₁ ⊗ m₂) m₃).app X ≫ (F.map (α_ m₁ m₂ m₃).hom).app X ≫ (F.μIso m₁ (m₂ ⊗ m₃)).inv.app X ≫ (F.μIso m₂ m₃).inv.app ((F.obj m₁).obj 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>m₁ m₂ m₃ : M<VAR>X : C<GOAL>inv ((F.obj m₃).map ((F.μIso m₁ m₂).inv.app X)) = (F.obj m₃).map ((F.μ m₁ m₂).app X)