ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<GOAL>ContinuousWithinAt f s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, EB × F) n (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) s x₀ ↔ (ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (↑(extChartAt IB (f x₀).proj) ∘ fun x => (f x).proj) s x₀) ∧ ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<GOAL>ContinuousWithinAt f s x₀ → (ContMDiffWithinAt IM 𝓘(𝕜, EB × F) n (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) s x₀ ↔ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (↑(extChartAt IB (f x₀).proj) ∘ fun x => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀)
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, EB × F) n (↑(extChartAt (IB.prod 𝓘(𝕜, F)) (f x₀)) ∘ f) s x₀ ↔ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (↑(extChartAt IB (f x₀).proj) ∘ fun x => (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (↑(extChartAt 𝓘(𝕜, F) (↑(trivializationAt F E (f x₀).proj) (f x₀)).2) ∘ fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<GOAL>ContMDiffWithinAt IM (𝓘(𝕜, EB).prod 𝓘(𝕜, F)) n (fun x => (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1, (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2)) s x₀ ↔ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (fun x => ↑(extChartAt IB (f x₀).proj) (f x).proj) s x₀ ∧ ContMDiffWithinAt IM 𝓘(𝕜, F) n (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, EB) n (Prod.fst ∘ fun x => (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1, (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2)) s x₀ ↔ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (fun x => ↑(extChartAt IB (f x₀).proj) (f x).proj) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<VAR>h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀<GOAL>ContMDiffWithinAt IM 𝓘(𝕜, EB) n (Prod.fst ∘ fun x => (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1, (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2)) s x₀ ↔ ContMDiffWithinAt IM 𝓘(𝕜, EB) n (fun x => ↑(extChartAt IB (f x₀).proj) (f x).proj) s x₀
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<VAR>h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀<VAR>x : M<VAR>hx : x ∈ (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet<GOAL>(Prod.fst ∘ fun x => (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1, (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2)) x = (fun x => ↑(extChartAt IB (f x₀).proj) (f x).proj) x
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>B' : Type u_3<VAR>F : Type u_4<VAR>M : Type u_5<VAR>E : B → Type u_6<VAR>inst✝¹⁶ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁵ : NormedAddCommGroup F<VAR>inst✝¹⁴ : NormedSpace 𝕜 F<VAR>inst✝¹³ : TopologicalSpace (TotalSpace F E)<VAR>inst✝¹² : (x : B) → TopologicalSpace (E x)<VAR>EB : Type u_7<VAR>inst✝¹¹ : NormedAddCommGroup EB<VAR>inst✝¹⁰ : NormedSpace 𝕜 EB<VAR>HB : Type u_8<VAR>inst✝⁹ : TopologicalSpace HB<VAR>IB : ModelWithCorners 𝕜 EB HB<VAR>E' : B → Type u_9<VAR>inst✝⁸ : (x : B) → Zero (E' x)<VAR>EM : Type u_10<VAR>inst✝⁷ : NormedAddCommGroup EM<VAR>inst✝⁶ : NormedSpace 𝕜 EM<VAR>HM : Type u_11<VAR>inst✝⁵ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : ChartedSpace HM M<VAR>Is : SmoothManifoldWithCorners IM M<VAR>n : ℕ∞<VAR>inst✝² : TopologicalSpace B<VAR>inst✝¹ : ChartedSpace HB B<VAR>inst✝ : FiberBundle F E<VAR>f : M → TotalSpace F E<VAR>s : Set M<VAR>x₀ : M<VAR>hf : ContinuousWithinAt f s x₀<VAR>h1 : (fun x => (f x).proj) ⁻¹' (trivializationAt F E (f x₀).proj).baseSet ∈ 𝓝[s] x₀<GOAL>(Prod.fst ∘ fun x => (↑(extChartAt IB (f x₀).proj) (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).1, (↑(trivializationAt F E (f x₀).proj).toPartialEquiv (f x)).2)) x₀ = ↑(extChartAt IB (f x₀).proj) (f x₀).proj
<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>H : Type u_8<VAR>F : Type u_9<VAR>inst✝³ : MulOneClass M<VAR>inst✝² : MulOneClass N<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MonoidHomClass F M N<VAR>f : F<VAR>a b : M<VAR>h : a * b = 1<GOAL>f a * f b = 1
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : LieRing L<VAR>inst✝⁴ : LieAlgebra R L<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : LieRingModule L M<VAR>inst✝ : LieModule R L M<VAR>N N' : LieSubmodule R L M<VAR>I J : LieIdeal R L<VAR>S : Set (LieSubmodule R L M)<GOAL>↑(sSup S) = ⨆ N ∈ S, ↑N
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>x y : R<VAR>inst✝ : Semiring R<VAR>h_comm : Commute x y<VAR>n : ℕ<VAR>hn : x ^ n = 0<VAR>m : ℕ<VAR>hm : y ^ m = 0<GOAL>IsNilpotent (x + y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → ℝ≥0<VAR>hf : Summable f<VAR>i : β → α<VAR>hi : Function.Injective i<GOAL>Summable (f ∘ i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>f : α → ℝ≥0<VAR>hf : Summable fun a => ↑(f a)<VAR>i : β → α<VAR>hi : Function.Injective i<GOAL>Summable fun a => ↑((f ∘ i) a)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set (Set Ω)<VAR>s' : Set (Set Ω)<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>t1 t2 : Set Ω<VAR>ht1 : t1 ∈ ⋂ n, s n<VAR>ht2 : t2 ∈ s'<VAR>n : ι<VAR>h : IndepSets (s n) s' κ μ<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (t1 ∩ t2) = (κ a) t1 * (κ a) t2
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>derivedLengthOfIdeal R L I = k + 1 ↔ IsLieAbelian ↥↑(derivedSeriesOfIdeal R L k I) ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>k : ℕ<GOAL>derivedLengthOfIdeal R L I = k + 1 ↔ derivedSeriesOfIdeal R L (k + 1) I = ⊥ ∧ derivedSeriesOfIdeal R L k I ≠ ⊥
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>k : ℕ<VAR>s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}<GOAL>sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
<VAR>R : Type u<VAR>L : Type v<VAR>M : Type w<VAR>L' : Type w₁<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : LieRing L<VAR>inst✝² : LieAlgebra R L<VAR>inst✝¹ : LieRing L'<VAR>inst✝ : LieAlgebra R L'<VAR>I✝ J : LieIdeal R L<VAR>f : L' →ₗ⁅R⁆ L<VAR>I : LieIdeal R L<VAR>k : ℕ<VAR>s : Set ℕ := {k | derivedSeriesOfIdeal R L k I = ⊥}<VAR>hs : ∀ (k₁ k₂ : ℕ), k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s<GOAL>sInf s = k + 1 ↔ k + 1 ∈ s ∧ k ∉ s
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<GOAL>Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ span K {v₀}
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝⁴ : Ring K<VAR>inst✝³ : StrongRankCondition K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>s : Submodule K V<VAR>inst✝ : Module.Free K ↥s<VAR>this : Nontrivial K<GOAL>Module.rank K ↥s ≤ 1 ↔ ∃ v₀, s ≤ span K {v₀}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : PartialOrder α<VAR>s : Set α<GOAL>IsLowerSet s ↔ ∀ ⦃a : α⦄, a ∈ s → Iio a ⊆ s
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>n : ℕ<VAR>x✝ : n + 2 ≠ 0<GOAL>(I ^ (n + 2)).radical = I.radical
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : CartesianClosed C<VAR>inst✝ : Reflective i<VAR>h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A<GOAL>ExponentialIdeal i
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>inst✝³ : Category.{v₁, u₂} D<VAR>i : D ⥤ C<VAR>inst✝² : HasFiniteProducts C<VAR>inst✝¹ : CartesianClosed C<VAR>inst✝ : Reflective i<VAR>h : (A : C) → i ⋙ exp A ⋙ reflector i ⋙ i ≅ i ⋙ exp A<GOAL>∀ (B : D) (A : C), (A ⟹ i.obj B) ∈ i.essImage
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>inst✝² : Group G<VAR>inst✝¹ : Group G'<VAR>H K L : Subgroup G<VAR>inst✝ : K.Normal<GOAL>K.relindex (K ⊔ H) = K.relindex H
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>h : IsEmpty ((i : ι) → α i)<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this✝ : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<VAR>this : IsTrans ι (Function.swap r)<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this✝¹ : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<VAR>this✝ : IsTrans ι (Function.swap r)<VAR>this : IsIrrefl ι (Function.swap r)<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this✝² : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<VAR>this✝¹ : IsTrans ι (Function.swap r)<VAR>this✝ : IsIrrefl ι (Function.swap r)<VAR>this : Fintype ι<GOAL>WellFounded (Pi.Lex r fun {i} => s i)
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this✝² : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<VAR>this✝¹ : IsTrans ι (Function.swap r)<VAR>this✝ : IsIrrefl ι (Function.swap r)<VAR>this : Fintype ι<VAR>i : ι<VAR>a : α i<GOAL>¬s i a 0
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>r : ι → ι → Prop<VAR>s : (i : ι) → α i → α i → Prop<VAR>inst✝¹ : IsStrictTotalOrder ι r<VAR>inst✝ : Finite ι<VAR>hs : ∀ (i : ι), WellFounded (s i)<VAR>x : (i : ι) → α i<VAR>this✝² : (i : ι) → Zero (α i) := fun i => { zero := ⋯.min ⊤ ⋯ }<VAR>this✝¹ : IsTrans ι (Function.swap r)<VAR>this✝ : IsIrrefl ι (Function.swap r)<VAR>this : Fintype ι<GOAL>WellFounded (Function.swap r)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Injective ⇑f<GOAL>Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Injective ⇑f<VAR>n : ℕ<VAR>hn : ∀ b ≥ n, Codisjoint (LinearMap.ker (f ^ b)) (LinearMap.range (f ^ b))<GOAL>Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Injective ⇑f<VAR>n : ℕ<VAR>hn : Codisjoint (LinearMap.ker (f ^ (n + 1))) (LinearMap.range (f ^ (n + 1)))<GOAL>Surjective ⇑f
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝³ : Ring R<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsArtinian R M<VAR>f : M →ₗ[R] M<VAR>s : Injective ⇑f<VAR>n : ℕ<VAR>hn : Surjective ⇑(f ^ (n + 1))<GOAL>Surjective ⇑f
<VAR>G : Type u_1<VAR>inst✝¹ : Group G<VAR>inst✝ : IsKleinFour G<VAR>h : IsCyclic G<VAR>_inst : Fintype G := Fintype.ofFinite G<GOAL>False
<GOAL>∃ k, -π - π = 2 * π * ↑k
<GOAL>-π - π = 2 * π * ↑(-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>f✝ g : α → ℝ≥0∞<VAR>f : α → ℝ≥0<VAR>r : ℝ≥0<VAR>hr : HasSum f r<GOAL>↑(tsum f) = ∑' (a : α), ↑(f a)
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>(∀ x ∈ S, _root_.IsAlgebraic R x) ↔ Algebra.IsAlgebraic R ↥S
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<GOAL>(∀ (x : ↥S), _root_.IsAlgebraic R ↑x) ↔ ∀ (x : ↥S), _root_.IsAlgebraic R x
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<VAR>p : R[X]<GOAL>(aeval ↑x) p = 0 ↔ (aeval x) p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<VAR>p : R[X]<VAR>h : Function.Injective ⇑S.val<GOAL>(aeval ↑x) p = 0 ↔ (aeval x) p = 0
<VAR>R : Type u<VAR>A : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x : ↥S<VAR>p : R[X]<VAR>h : Function.Injective ⇑S.val<GOAL>(aeval ↑x) p = 0 ↔ S.val ((aeval x) p) = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>h : a ∈ t<GOAL>insert a s ∩ t = insert a (s ∩ t)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>LiftPropWithinAt P g s x ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>H : Type u_1<VAR>M : Type u_2<VAR>H' : Type u_3<VAR>M' : Type u_4<VAR>X : Type u_5<VAR>inst✝⁸ : TopologicalSpace H<VAR>inst✝⁷ : TopologicalSpace M<VAR>inst✝⁶ : ChartedSpace H M<VAR>inst✝⁵ : TopologicalSpace H'<VAR>inst✝⁴ : TopologicalSpace M'<VAR>inst✝³ : ChartedSpace H' M'<VAR>inst✝² : TopologicalSpace X<VAR>G : StructureGroupoid H<VAR>G' : StructureGroupoid H'<VAR>e e' : PartialHomeomorph M H<VAR>f f' : PartialHomeomorph M' H'<VAR>P : (H → H') → Set H → H → Prop<VAR>g g' : M → M'<VAR>s t : Set M<VAR>x : M<VAR>Q : (H → H) → Set H → H → Prop<VAR>hG : G.LocalInvariantProp G' P<VAR>inst✝¹ : HasGroupoid M G<VAR>inst✝ : HasGroupoid M' G'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>hf : f ∈ maximalAtlas M' G'<VAR>xf : g x ∈ f.source<GOAL>ContinuousWithinAt g s x ∧ P (↑(chartAt H' (g x)) ∘ g ∘ ↑(chartAt H x).symm) (↑(chartAt H x).symm ⁻¹' s) (↑(chartAt H x) x) ↔ ContinuousWithinAt g s x ∧ P (↑f ∘ g ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)
<VAR>a b c b' c' : ℕ<VAR>h1 : a.pow b' = c'<VAR>hb : 2 * b' + 1 = b<VAR>hc : c' * (c' * a) = c<GOAL>(Int.negOfNat a).pow b = Int.negOfNat c
<VAR>a b c b' c' : ℕ<VAR>h1 : a.pow b' = c'<VAR>hb : 2 * b' + 1 = b<VAR>hc : c' * (c' * a) = c<GOAL>Int.ofNat a ^ b' * Int.ofNat a ^ b' * -Int.ofNat a = -Int.ofNat (a.pow b' * (a.pow b' * a))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : PseudoMetricSpace P<VAR>inst✝ : NormedAddTorsor E P<VAR>s t : Set E<VAR>hs : Convex ℝ s<VAR>x : E<VAR>x✝² : x ∈ s<VAR>y : E<VAR>x✝¹ : y ∈ s<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>x✝ : a + b = 1<GOAL>‖a • x‖ + ‖b • y‖ = a * ‖x‖ + b * ‖y‖