ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f₁ g₁ f₂ g₂ : C ⟶ D<VAR>h₁ : Homotopy f₁ g₁<VAR>h₂ : Homotopy f₂ g₂<VAR>i : ι<GOAL>(f₁ + f₂).f i = (dNext i) (h₁.hom + h₂.hom) + (prevD i) (h₁.hom + h₂.hom) + (g₁ + g₂).f i
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : Preadditive V<VAR>c : ComplexShape ι<VAR>C D E : HomologicalComplex V c<VAR>f g : C ⟶ D<VAR>h k : D ⟶ E<VAR>i✝ : ι<VAR>f₁ g₁ f₂ g₂ : C ⟶ D<VAR>h₁ : Homotopy f₁ g₁<VAR>h₂ : Homotopy f₂ g₂<VAR>i : ι<GOAL>(dNext i) h₁.hom + (prevD i) h₁.hom + g₁.f i + ((dNext i) h₂.hom + (prevD i) h₂.hom + g₂.f i) = (dNext i) h₁.hom + (dNext i) h₂.hom + ((prevD i) h₁.hom + (prevD i) h₂.hom) + (g₁.f i + g₂.f i)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p f' : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f f' s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ u ∈ 𝓝[insert x s] x, ∃ p, HasFTaylorSeriesUpToOn (↑m) f p u
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p f' : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f f' s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>s ∈ 𝓝[insert x s] x ∧ ∃ p, HasFTaylorSeriesUpToOn (↑m) f p s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p f' : E → FormalMultilinearSeries 𝕜 E F<VAR>hf : HasFTaylorSeriesUpToOn n f f' s<VAR>x : E<VAR>hx : x ∈ s<VAR>m : ℕ<VAR>hm : ↑m ≤ n<GOAL>∃ p, HasFTaylorSeriesUpToOn (↑m) f p s
<VAR>G : Type u_1<VAR>inst✝ : Group G<VAR>H : Subgroup G<VAR>g : ConjAct G<GOAL>Commensurable (g • H) H ↔ Commensurable H (g⁻¹ • H)
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c : ℝ<GOAL>integral I l (fun x => c • f x) vol = c • integral I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<GOAL>integral I l (fun x => 0 • f x) vol = 0 • integral I l f vol
<VAR>ι : Type u<VAR>E : Type v<VAR>F : Type w<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>I J : Box ι<VAR>π : TaggedPrepartition I<VAR>inst✝ : Fintype ι<VAR>l : IntegrationParams<VAR>f g : (ι → ℝ) → E<VAR>vol : ι →ᵇᵃ[⊤] E →L[ℝ] F<VAR>y y' : F<VAR>c : ℝ<VAR>hc : c ≠ 0<GOAL>integral I l (fun x => c • f x) vol = c • integral I l f vol
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsConnected A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ τ : Aut A<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a : ↑(F.obj A)<GOAL>autMap f (σ * τ) = autMap f σ * autMap f τ
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{u₂, u₁} C<VAR>inst✝³ : GaloisCategory C<VAR>F✝ : C ⥤ FintypeCat<VAR>inst✝² : FiberFunctor F✝<VAR>A B : C<VAR>inst✝¹ : IsConnected A<VAR>inst✝ : IsGalois B<VAR>f : A ⟶ B<VAR>σ τ : Aut A<VAR>F : C ⥤ FintypeCat := GaloisCategory.getFiberFunctor C<VAR>a : ↑(F.obj A)<GOAL>(fun f_1 => F.map f_1.hom (F.map f a)) (autMap f (σ * τ)) = (fun f_1 => F.map f_1.hom (F.map f a)) (autMap f σ * autMap f τ)
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁸ : MeasurableSpace G<VAR>inst✝⁷ : MeasurableSpace H<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<GOAL>∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁸ : MeasurableSpace G<VAR>inst✝⁷ : MeasurableSpace H<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>U : Set G<VAR>hUk : k ⊆ U<VAR>hU : IsOpen U<VAR>hμUk : μ U < μ k + ε<GOAL>∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁸ : MeasurableSpace G<VAR>inst✝⁷ : MeasurableSpace H<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>U : Set G<VAR>hUk : k ⊆ U<VAR>hU : IsOpen U<VAR>hμUk : μ U < μ k + ε<VAR>V : Set G<VAR>hV1 : V ∈ 𝓝 1<VAR>hVkU : V * k ⊆ U<GOAL>∀ᶠ (g : G) in 𝓝 1, μ (g • k \ k) < ε
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝⁸ : MeasurableSpace G<VAR>inst✝⁷ : MeasurableSpace H<VAR>inst✝⁶ : TopologicalSpace G<VAR>inst✝⁵ : BorelSpace G<VAR>μ : Measure G<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalGroup G<VAR>inst✝² : LocallyCompactSpace G<VAR>inst✝¹ : IsFiniteMeasureOnCompacts μ<VAR>inst✝ : μ.InnerRegularCompactLTTop<VAR>k : Set G<VAR>hk : IsCompact k<VAR>h'k : IsClosed k<VAR>ε : ℝ≥0∞<VAR>hε : ε ≠ 0<VAR>U : Set G<VAR>hUk : k ⊆ U<VAR>hU : IsOpen U<VAR>hμUk : μ U < μ k + ε<VAR>V : Set G<VAR>hV1 : V ∈ 𝓝 1<VAR>hVkU : V * k ⊆ U<VAR>g : G<VAR>hg : g ∈ V<GOAL>μ (g • k \ k) < ε
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>h : a < b<GOAL>a + (b - a) / 2 < b
<VAR>b : EReal<VAR>h : b ≤ 0<VAR>a a' : EReal<VAR>h' : a ≤ a'<GOAL>a' * b⁻¹ ≤ a * b⁻¹
<VAR>b : EReal<VAR>h : b ≤ 0<VAR>a a' : EReal<VAR>h' : a ≤ a'<GOAL>a * (-b)⁻¹ ≤ a' * (-b)⁻¹
<VAR>b : EReal<VAR>h : b ≤ 0<VAR>a a' : EReal<VAR>h' : a ≤ a'<VAR>this : 0 ≤ -b<GOAL>a * (-b)⁻¹ ≤ a' * (-b)⁻¹
<VAR>x y a b : ℝ<GOAL>0 < a → 0 < b → 0 < a * b
<VAR>x y b : ℝ<VAR>a : CauSeq ℚ abs<GOAL>0 < mk a → 0 < b → 0 < mk a * b
<VAR>x y : ℝ<VAR>a b : CauSeq ℚ abs<GOAL>0 < mk a → 0 < mk b → 0 < mk a * mk b
<VAR>R : Type u_1<VAR>M✝ : Type u_2<VAR>inst✝¹⁹ : CommSemiring R<VAR>inst✝¹⁸ : AddCommMonoid M✝<VAR>inst✝¹⁷ : Module R M✝<VAR>R₁ : Type u_3<VAR>M₁ : Type u_4<VAR>inst✝¹⁶ : CommRing R₁<VAR>inst✝¹⁵ : AddCommGroup M₁<VAR>inst✝¹⁴ : Module R₁ M₁<VAR>R₂ : Type u_5<VAR>M₂ : Type u_6<VAR>inst✝¹³ : CommSemiring R₂<VAR>inst✝¹² : AddCommMonoid M₂<VAR>inst✝¹¹ : Module R₂ M₂<VAR>R₃ : Type u_7<VAR>M₃ : Type u_8<VAR>inst✝¹⁰ : CommRing R₃<VAR>inst✝⁹ : AddCommGroup M₃<VAR>inst✝⁸ : Module R₃ M₃<VAR>V : Type u_9<VAR>K : Type u_10<VAR>inst✝⁷ : Field K<VAR>inst✝⁶ : AddCommGroup V<VAR>inst✝⁵ : Module K V<VAR>B : BilinForm R M✝<VAR>B₁ : BilinForm R₁ M₁<VAR>B₂ : BilinForm R₂ M₂<VAR>A : Type u_11<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : IsDomain A<VAR>inst✝² : Module A M₃<VAR>B₃ : BilinForm A M₃<VAR>ι : Type u_12<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>M : Matrix ι ι R₃<VAR>h : M.Nondegenerate<VAR>x : ι → R₃<VAR>hx : ∀ (n : ι → R₃), ((Matrix.toBilin' M) x) n = 0<VAR>y : ι → R₃<GOAL>x ⬝ᵥ M *ᵥ y = 0
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>n.Perfect ↔ ∑ i ∈ n.divisors, i = 2 * n
<VAR>n : ℕ<VAR>h : 0 < n<GOAL>∑ i ∈ n.properDivisors, i = n ↔ ∑ i ∈ n.properDivisors, i + n = n + n
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>M✝ : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>M : Matroid α<GOAL>M.closure univ = M.E
<VAR>a : Ordinal.{u_1}<VAR>h : a < ω<GOAL>a + ω = ω
<VAR>n : ℕ<VAR>h : ↑n < ω<GOAL>↑n + ω = ω
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<GOAL>(l.rotate n)[m]? = l[(m + n) % l.length]?
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<GOAL>(drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<VAR>hm : m < (drop (n % l.length) l).length<GOAL>(drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
<VAR>α : Type u<VAR>l : List α<VAR>n m : ℕ<VAR>hml : m < l.length<VAR>hm : (drop (n % l.length) l).length ≤ m<GOAL>(drop (n % l.length) l ++ take (n % l.length) l)[m]? = l[(m + n) % l.length]?
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<GOAL>finrank F ↥F⟮α⟯ = 1 ↔ α ∈ ⊥
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>α : E<VAR>S : Set E<VAR>K L : IntermediateField F E<GOAL>{α} ⊆ ↑⊥ ↔ α ∈ ⊥
<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✝⁴ : FunLike F α β<VAR>inst✝³ : Lattice α<VAR>inst✝² : Lattice β<VAR>inst✝¹ : Lattice γ<VAR>inst✝ : Lattice δ<VAR>g : LatticeHom β γ<VAR>f₁ f₂ : LatticeHom α β<VAR>hg : Injective ⇑g<VAR>h : g.comp f₁ = g.comp f₂<VAR>a : α<GOAL>g (f₁ a) = g (f₂ a)
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Pow M ℕ+<VAR>inst✝ : PNatPowAssoc M<VAR>x : M<VAR>m n : ℕ+<GOAL>x ^ (m * n) = (x ^ n) ^ m
<VAR>M : Type u_1<VAR>inst✝² : Mul M<VAR>inst✝¹ : Pow M ℕ+<VAR>inst✝ : PNatPowAssoc M<VAR>x : M<VAR>m n : ℕ+<GOAL>x ^ (n * m) = (x ^ n) ^ m
<VAR>C₁ : Type u_1<VAR>C₂ : Type u_2<VAR>C₃ : Type u_3<VAR>inst✝³ : Category.{u_9, u_1} C₁<VAR>inst✝² : Category.{u_8, u_2} C₂<VAR>inst✝¹ : Category.{u_7, u_3} C₃<VAR>F : C₁ ⥤ C₂ ⥤ C₃<VAR>I : Type u_4<VAR>J : Type u_5<VAR>K : Type u_6<VAR>p : I × J → K<VAR>X : GradedObject I C₁<VAR>Y : GradedObject J C₂<VAR>A : C₃<VAR>k : K<VAR>inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p<VAR>f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)<VAR>i : I<VAR>j : J<VAR>hij : p (i, j) = k<GOAL>ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Lattice α<VAR>inst✝ : Lattice β<VAR>a✝ a₁ a₂ b✝ b₁ b₂ c x a b : α<GOAL>[[a, b]] = [[b, a]]
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>t : Set α<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>ht : t.Countable<VAR>f : α → Set X<VAR>hc : ∀ i ∈ t, IsClosed (f i)<VAR>hU : s ⊆ ⋃ i ∈ t, f i<VAR>this : Countable ↑t<GOAL>Dense (⋃ i ∈ t, interior (f i))
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>ι : Sort u_3<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : BaireSpace X<VAR>t : Set α<VAR>s : Set X<VAR>hs : IsGδ s<VAR>hd : Dense s<VAR>ht : t.Countable<VAR>f : α → Set X<VAR>this : Countable ↑t<VAR>hc : ∀ (x : ↑t), IsClosed (f ↑x)<VAR>hU : s ⊆ ⋃ x, f ↑x<GOAL>Dense (⋃ x, interior (f ↑x))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hfI : f a = f b<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hfI : f a = f b<VAR>ne : (Icc a b).Nonempty<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hfI : f a = f b<VAR>ne : (Icc a b).Nonempty<VAR>c : X<VAR>cmem : c ∈ Icc a b<VAR>cle : ∀ x ∈ Icc a b, f c ≤ f x<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder X<VAR>inst✝⁵ : DenselyOrdered X<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : OrderTopology X<VAR>inst✝² : LinearOrder Y<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : OrderTopology Y<VAR>f : X → Y<VAR>a b : X<VAR>l : Y<VAR>hab : a < b<VAR>hfc : ContinuousOn f (Icc a b)<VAR>hfI : f a = f b<VAR>ne : (Icc a b).Nonempty<VAR>c : X<VAR>cmem : c ∈ Icc a b<VAR>cle : ∀ x ∈ Icc a b, f c ≤ f x<VAR>C : X<VAR>Cmem : C ∈ Icc a b<VAR>Cge : ∀ x ∈ Icc a b, f x ≤ f C<GOAL>∃ c ∈ Ioo a b, IsExtrOn f (Icc a b) c
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>s = {a} ∨ s.Nontrivial
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s : Finset α<VAR>a b : α<VAR>ha : a ∈ s<GOAL>↑s = {a} ∨ s.Nontrivial
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>M M' : Ideal α<VAR>hM : M.IsMaximal<VAR>hM' : M'.IsMaximal<VAR>hne : M ≠ M'<GOAL>M ⊔ M' = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝ : Semiring α<VAR>I : Ideal α<VAR>a b : α<VAR>M M' : Ideal α<VAR>hM : M.IsMaximal<VAR>hM' : M'.IsMaximal<VAR>h : M ⊔ M' ≠ ⊤<GOAL>M = M'
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>x : R<VAR>hp : ¬1 < p<GOAL>x ∈ pNilradical R p ↔ ∃ n, x ^ p ^ n = 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>x : R<VAR>hp : ¬1 < p<GOAL>x = 0 ↔ ∃ n, x ^ p ^ n = 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>x : R<VAR>hp : ¬1 < p<VAR>x✝ : ∃ n, x ^ p ^ n = 0<VAR>n : ℕ<VAR>h : x ^ p ^ n = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>x : R<VAR>hp✝ : ¬1 < p<VAR>x✝ : ∃ n, x ^ p ^ n = 0<VAR>n : ℕ<VAR>h : x ^ p ^ n = 0<VAR>hp : p = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝ : CommSemiring R<VAR>p : ℕ<VAR>x : R<VAR>hp✝ : ¬1 < p<VAR>x✝ : ∃ n, x ^ p ^ n = 0<VAR>n : ℕ<VAR>h : x ^ p ^ n = 0<VAR>hp : p = 1<GOAL>x = 0
<VAR>Ω : Type u_1<VAR>ι : Type u_2<VAR>β✝ : Type u_3<VAR>γ✝ : Type u_4<VAR>κ : ι → Type u_5<VAR>β : Type u_6<VAR>β' : Type u_7<VAR>γ : Type u_8<VAR>γ' : Type u_9<VAR>_mΩ : MeasurableSpace Ω<VAR>μ : Measure Ω<VAR>f : Ω → β<VAR>g : Ω → β'<VAR>mβ : MeasurableSpace β<VAR>mβ' : MeasurableSpace β'<GOAL>IndepFun f g μ ↔ ∀ (s : Set β) (t : Set β'), MeasurableSet s → MeasurableSet t → μ (f ⁻¹' s ∩ g ⁻¹' t) = μ (f ⁻¹' s) * μ (g ⁻¹' t)
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>F : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : FunLike F M M₁<VAR>inst✝⁴ : AddMonoidHomClass F M M₁<VAR>inst✝³ : Module (ZMod n) M<VAR>inst✝² : Module (ZMod n) M₁<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubgroupClass S M<VAR>x : M<VAR>K : S<VAR>hx : x ∈ K<VAR>c : ZMod n<GOAL>c • x ∈ K
<VAR>n : ℕ<VAR>M : Type u_1<VAR>M₁ : Type u_2<VAR>F : Type u_3<VAR>S : Type u_4<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : AddCommGroup M₁<VAR>inst✝⁵ : FunLike F M M₁<VAR>inst✝⁴ : AddMonoidHomClass F M M₁<VAR>inst✝³ : Module (ZMod n) M<VAR>inst✝² : Module (ZMod n) M₁<VAR>inst✝¹ : SetLike S M<VAR>inst✝ : AddSubgroupClass S M<VAR>x : M<VAR>K : S<VAR>hx : x ∈ K<VAR>c : ZMod n<GOAL>c.cast • x ∈ K
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m (ForInStep β)<VAR>l : List α<VAR>init : β<GOAL>forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)
<VAR>m : Type u_1 → Type u_2<VAR>α : Type u_3<VAR>β : Type u_1<VAR>inst✝¹ : Monad m<VAR>inst✝ : LawfulMonad m<VAR>f : α → β → m (ForInStep β)<VAR>head✝ : α<VAR>tail✝ : List α<VAR>tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)<VAR>init : β<GOAL>(do let x ← f head✝ init match x with | ForInStep.done b => pure b | ForInStep.yield b => do let a ← ForInStep.bindList f tail✝ (ForInStep.yield b) pure a.run) = do let x ← f head✝ init let a ← ForInStep.bindList f tail✝ x pure a.run
<VAR>p : ℕ<VAR>R : Type u_1<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CharP R p<VAR>x : 𝕎 R<GOAL>verschiebung (frobenius x) = frobenius (verschiebung x)
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a : R<VAR>n✝ : ℕ<VAR>H : -1 ≤ a<VAR>n : ℕ<GOAL>1 + ↑n * (a - 1) ≤ a ^ n
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a : R<VAR>n✝ : ℕ<VAR>H : -1 ≤ a<VAR>n : ℕ<VAR>this : -2 ≤ a - 1<GOAL>1 + ↑n * (a - 1) ≤ a ^ n
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>(∀ (n : ℕ∞), ContDiff 𝕜 n f) ↔ ∀ (n : ℕ), ContDiff 𝕜 (↑n) f
<VAR>α : Type u_1<VAR>inst✝ : DecidableEq α<VAR>l t₁ t₂ : List α<VAR>h : t₁ ~ t₂<GOAL>l.diff t₁ = l.diff t₂
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this : LieRingModule L M := LieRingModule.compLieHom M f<GOAL>LieModule.IsNilpotent R L₂ M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this : LieModule R L M := compLieHom M f<GOAL>LieModule.IsNilpotent R L₂ M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<GOAL>LieModule.IsNilpotent R L₂ M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<VAR>surj_id : Surjective ⇑LinearMap.id<GOAL>LieModule.IsNilpotent R L₂ M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this✝ : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<VAR>surj_id : Surjective ⇑LinearMap.id<VAR>this : LieModule.IsNilpotent R L M<GOAL>LieModule.IsNilpotent R L₂ M
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this✝ : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<VAR>surj_id : Surjective ⇑LinearMap.id<VAR>this : LieModule.IsNilpotent R L M<GOAL>∀ (x : L) (m : M), ⁅f x, LinearMap.id m⁆ = LinearMap.id ⁅x, m⁆
<VAR>R : Type u₁<VAR>L : Type u₂<VAR>L₂ : Type u₃<VAR>M✝ : Type u₄<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<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>f : L →ₗ⁅R⁆ L₂<VAR>hf : Surjective ⇑f<VAR>h : LieAlgebra.IsEngelian R L<VAR>M : Type u₄<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L₂ M<VAR>_i4 : LieModule R L₂ M<VAR>h' : ∀ (x : L₂), IsNilpotent ((toEnd R L₂ M) x)<VAR>this✝¹ : LieRingModule L M := LieRingModule.compLieHom M f<VAR>this✝ : LieModule R L M := compLieHom M f<VAR>hnp : ∀ (x : L), IsNilpotent ((toEnd R L M) x)<VAR>surj_id : Surjective ⇑LinearMap.id<VAR>this : LieModule.IsNilpotent R L M<VAR>x✝ : L<VAR>m✝ : M<GOAL>⁅f x✝, LinearMap.id m✝⁆ = LinearMap.id ⁅x✝, m✝⁆