ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>S : Set (Sublattice α)<GOAL>a ∈ sInf S ↔ ∀ L ∈ S, a ∈ L
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : Lattice α<VAR>inst✝¹ : Lattice β<VAR>inst✝ : Lattice γ<VAR>L M : Sublattice α<VAR>f : LatticeHom α β<VAR>s t : Set α<VAR>a : α<VAR>S : Set (Sublattice α)<GOAL>a ∈ ↑(sInf S) ↔ ∀ L ∈ S, a ∈ L
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<VAR>ha : Odd a<GOAL>Odd (a ^ 0)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<VAR>ha : Odd a<GOAL>Odd 1
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n✝ : ℕ<VAR>ha : Odd a<VAR>n : ℕ<GOAL>Odd (a ^ (n + 1))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n✝ : ℕ<VAR>ha : Odd a<VAR>n : ℕ<GOAL>Odd (a ^ n * a)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : N ⊗[R] M<GOAL>(rTensor M (g ∘ₗ f)) x = (rTensor M g) ((rTensor M f) x)
<VAR>R : Type u_1<VAR>inst✝¹⁶ : CommSemiring R<VAR>R' : Type u_2<VAR>inst✝¹⁵ : Monoid R'<VAR>R'' : Type u_3<VAR>inst✝¹⁴ : Semiring R''<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>S : Type u_8<VAR>T : Type u_9<VAR>inst✝¹³ : AddCommMonoid M<VAR>inst✝¹² : AddCommMonoid N<VAR>inst✝¹¹ : AddCommMonoid P<VAR>inst✝¹⁰ : AddCommMonoid Q<VAR>inst✝⁹ : AddCommMonoid S<VAR>inst✝⁸ : AddCommMonoid T<VAR>inst✝⁷ : Module R M<VAR>inst✝⁶ : Module R N<VAR>inst✝⁵ : Module R P<VAR>inst✝⁴ : Module R Q<VAR>inst✝³ : Module R S<VAR>inst✝² : Module R T<VAR>inst✝¹ : DistribMulAction R' M<VAR>inst✝ : Module R'' M<VAR>g : P →ₗ[R] Q<VAR>f : N →ₗ[R] P<VAR>x : N ⊗[R] M<GOAL>(⇑(rTensor M g) ∘ ⇑(rTensor M f)) x = (rTensor M g) ((rTensor M f) x)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f (μ.trim hm)<GOAL>eLpNorm f p (μ.trim hm) = eLpNorm f p μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>m m0 : MeasurableSpace α<VAR>p : ℝ≥0∞<VAR>q : ℝ<VAR>μ : Measure α<VAR>inst✝ : NormedAddCommGroup E<VAR>hm : m ≤ m0<VAR>f : α → E<VAR>hf : AEStronglyMeasurable f (μ.trim hm)<GOAL>eLpNorm (AEStronglyMeasurable.mk f hf) p (μ.trim hm) = eLpNorm (AEStronglyMeasurable.mk f hf) p μ
<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>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : SemilatticeSup ι<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<GOAL>CauchySeq f ↔ Tendsto (fun n => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)
<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>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : SemilatticeSup ι<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<GOAL>Tendsto (fun n => (eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ).toReal) atTop (𝓝 0) ↔ Tendsto (fun n => eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ) atTop (𝓝 0)
<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>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : SemilatticeSup ι<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>n : ι × ι<GOAL>eLpNorm (↑↑(f n.1) - ↑↑(f n.2)) p μ ≠ ⊤
<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>ι : Type u_5<VAR>inst✝¹ : Nonempty ι<VAR>inst✝ : SemilatticeSup ι<VAR>hp : Fact (1 ≤ p)<VAR>f : ι → ↥(Lp E p μ)<VAR>n : ι × ι<GOAL>eLpNorm (↑↑(f n.1 - f n.2)) p μ ≠ ⊤
<VAR>J : Type u_1<VAR>inst✝ : Category.{u_2, u_1} J<VAR>K : J ⥤ Type u<VAR>c : Cocone K<VAR>hc : IsColimit c<VAR>lc : Cocone (K ⋙ uliftFunctor.{v, u})<GOAL>descSet hc ∅ = ∅
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β✝ : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>f1 f2 : α →₀ M<VAR>hd : Disjoint f1.support f2.support<VAR>β : Type u_16<VAR>inst✝ : CommMonoid β<VAR>g : α → M → β<GOAL>(f1 + f2).prod g = f1.prod g * f2.prod g
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>γ : Type u_3<VAR>A : Type u_4<VAR>B : Type u_5<VAR>C : Type u_6<VAR>inst✝⁴ : AddCommMonoid A<VAR>inst✝³ : AddCommMonoid B<VAR>inst✝² : AddCommMonoid C<VAR>t : ι → A → C<VAR>h0 : ∀ (i : ι), t i 0 = 0<VAR>h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y<VAR>s : Finset α<VAR>f : α → ι →₀ A<VAR>i : ι<VAR>g✝ : ι →₀ A<VAR>k : ι → A → γ → B<VAR>x : γ<VAR>β✝ : Type u_7<VAR>M : Type u_8<VAR>M' : Type u_9<VAR>N : Type u_10<VAR>P : Type u_11<VAR>G : Type u_12<VAR>H : Type u_13<VAR>R : Type u_14<VAR>S : Type u_15<VAR>inst✝¹ : AddCommMonoid M<VAR>f1 f2 : α →₀ M<VAR>hd : Disjoint f1.support f2.support<VAR>β : Type u_16<VAR>inst✝ : CommMonoid β<VAR>g : α → M → β<VAR>this : ∀ {f1 f2 : α →₀ M}, Disjoint f1.support f2.support → ∏ x ∈ f1.support, g x (f1 x + f2 x) = f1.prod g<GOAL>(f1 + f2).prod g = f1.prod g * f2.prod g
<VAR>ι : Type u_1<VAR>V : Type u<VAR>inst✝¹ : Category.{v, u} V<VAR>inst✝ : HasZeroMorphisms V<VAR>X₀ X₁ X₂ : V<VAR>d₀ : X₀ ⟶ X₁<VAR>d₁ : X₁ ⟶ X₂<VAR>s : d₀ ≫ d₁ = 0<VAR>succ : (S : ShortComplex V) → (X₄ : V) ×' (d₂ : S.X₃ ⟶ X₄) ×' S.g ≫ d₂ = 0<GOAL>(if 2 = 1 + 1 then d₁ ≫ 𝟙 X₂ else 0) = d₁
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>l l' : Filter α<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>t : Set α<VAR>i : ι<VAR>p' : ι' → Prop<VAR>s' : ι' → Set α<VAR>i' : ι'<VAR>h : l.HasBasis (fun x => True) s<GOAL>l = ⨅ i, 𝓟 (s i)
<VAR>n✝ : ℕ<VAR>α : Type u_1<VAR>n : ℕ<VAR>v : Vector α n<GOAL>(map id v).toList = v.toList
<VAR>M : Type u<VAR>inst✝³ : Monoid M<VAR>α : Type v<VAR>inst✝² : MulAction M α<VAR>β : Type u_1<VAR>inst✝¹ : MulAction M β<VAR>a : α<VAR>inst✝ : Fintype ↑(orbit M a)<GOAL>a ∈ fixedPoints M α ↔ Fintype.card ↑(orbit M a) = 1
<VAR>M : Type u<VAR>inst✝³ : Monoid M<VAR>α : Type v<VAR>inst✝² : MulAction M α<VAR>β : Type u_1<VAR>inst✝¹ : MulAction M β<VAR>a : α<VAR>inst✝ : Fintype ↑(orbit M a)<GOAL>(∀ (m : M), m • a = a) ↔ ∃ x, ∀ (y : ↑(orbit M a)), y = x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a✝ b✝ c d a b : α<GOAL>a ⊔ b ⇨ a = b ⇨ a
<VAR>R : Type u<VAR>ι : Type u_1<VAR>inst✝ : CommSemiring R<VAR>I J K L : Ideal R<VAR>m✝ : Multiset R<VAR>a : R<VAR>m : Multiset R<VAR>ih : (Multiset.map (fun x => span {x}) m).prod = span {m.prod}<GOAL>(Multiset.map (fun x => span {x}) (a ::ₘ m)).prod = span {(a ::ₘ m).prod}
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Function.Surjective ⇑f
<VAR>X Y : TopCat<VAR>f : X ⟶ Y<GOAL>Epi f ↔ Epi ((forget TopCat).map f)
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.17548, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex V c<VAR>i j : ι<VAR>hij : ¬c.symm.Rel i j<GOAL>(X.d j i).op = 0
<VAR>ι : Type u_1<VAR>V : Type u_2<VAR>inst✝¹ : Category.{?u.17548, u_2} V<VAR>c : ComplexShape ι<VAR>inst✝ : HasZeroMorphisms V<VAR>X : HomologicalComplex V c<VAR>x✝⁴ x✝³ x✝² : ι<VAR>x✝¹ : c.symm.Rel x✝⁴ x✝³<VAR>x✝ : c.symm.Rel x✝³ x✝²<GOAL>(fun i j => (X.d j i).op) x✝⁴ x✝³ ≫ (fun i j => (X.d j i).op) x✝³ x✝² = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>hp : p ∈ R[X]⁰<GOAL>(taylor r) p ∈ R[X]⁰
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>hp : p ∈ R[X]⁰<GOAL>∀ (x : R[X]), x * (taylor r) p = 0 → x = 0
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>hdomain : IsDomain R<VAR>r s : R<VAR>p q : R[X]<VAR>f : RatFunc R<VAR>hp : p ∈ R[X]⁰<VAR>x : R[X]<VAR>hx : x * (taylor r) p = 0<VAR>this : x = (taylor (r - r)) x<GOAL>x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : Countable ι<VAR>t : ι → Set α<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>f : (i : ι) → ↑(t i) → β<VAR>hfm : ∀ (i : ι), Measurable (f i)<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>htU : ⋃ i, t i = univ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (liftCover t f hf htU ⁻¹' s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : Countable ι<VAR>t : ι → Set α<VAR>htm : ∀ (i : ι), MeasurableSet (t i)<VAR>f : (i : ι) → ↑(t i) → β<VAR>hfm : ∀ (i : ι), Measurable (f i)<VAR>hf : ∀ (i j : ι) (x : α) (hxi : x ∈ t i) (hxj : x ∈ t j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩<VAR>htU : ⋃ i, t i = univ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet (⋃ i, Subtype.val '' (f i ⁻¹' s))
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s : Submodule K V<VAR>h : s < ⊤<GOAL>finrank K ↥s < finrank K V
<VAR>K : Type u<VAR>V : Type v<VAR>inst✝³ : DivisionRing K<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>s : Submodule K V<VAR>h : s < ⊤<GOAL>finrank K ↥s < finrank K ↥s + finrank K (V ⧸ s)
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MulZeroClass β<VAR>f f' : α → β<VAR>x : α<VAR>hf : HasCompactSupport f<GOAL>HasCompactSupport (f * f')
<VAR>X : Type u_1<VAR>α : Type u_2<VAR>α' : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>δ : Type u_6<VAR>M : Type u_7<VAR>E : Type u_8<VAR>R : Type u_9<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : MulZeroClass β<VAR>f f' : α → β<VAR>x : α<VAR>hf : f =ᶠ[coclosedCompact α] 0<GOAL>f * f' =ᶠ[coclosedCompact α] 0
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : OrderedRing R<VAR>inst✝ : LinearOrderedRing S<VAR>hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r<VAR>f : R →+* S<VAR>s : R<VAR>h : 0 ≤ s ^ 2<GOAL>0 ≤ f (s ^ 2)
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝¹ : OrderedRing R<VAR>inst✝ : LinearOrderedRing S<VAR>hR : ∀ (r : R), 0 ≤ r → ∃ s, s ^ 2 = r<VAR>f : R →+* S<VAR>s : R<VAR>h : 0 ≤ s ^ 2<GOAL>0 ≤ f s ^ 2
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝³ : Monoid R<VAR>inst✝² : AddMonoid M<VAR>inst✝¹ : DistribMulAction R M<VAR>inst✝ : DistribMulAction Rᵐᵒᵖ M<VAR>r : R<VAR>n : ℕ<GOAL>(inl r ^ n).snd = (inl (r ^ n)).snd
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>n : ℕ<VAR>S : ComposableArrows C n<VAR>hS : S.Exact<VAR>i : ℕ<VAR>hk : autoParam (i + 1 + 1 ≤ n) _auto✝<GOAL>(S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ ⋯).Exact
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure = univ<GOAL>‖S.normedMk‖ = 0
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure = univ<VAR>x : M<GOAL>‖S.normedMk x‖ ≤ 0 * ‖x‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure = univ<VAR>x : M<VAR>hker : x ∈ S.normedMk.ker.topologicalClosure<GOAL>‖S.normedMk x‖ ≤ 0 * ‖x‖
<VAR>M : Type u_1<VAR>N : Type u_2<VAR>inst✝¹ : SeminormedAddCommGroup M<VAR>inst✝ : SeminormedAddCommGroup N<VAR>S : AddSubgroup M<VAR>h : ↑S.topologicalClosure = univ<VAR>x : M<VAR>hker : x ∈ S.topologicalClosure<GOAL>‖S.normedMk x‖ ≤ 0 * ‖x‖
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq N<VAR>inst✝ : Zero N<VAR>f✝ g✝ f g : α →₀ N<VAR>a : α<GOAL>a ∈ f.neLocus g ↔ f a ≠ g a
<VAR>α✝ : Type u_1<VAR>M✝ : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R✝ : Type u_5<VAR>S : Type u_6<VAR>inst✝¹⁰ : Semiring R✝<VAR>inst✝⁹ : Semiring S<VAR>inst✝⁸ : AddCommMonoid M✝<VAR>inst✝⁷ : Module R✝ M✝<VAR>inst✝⁶ : AddCommMonoid N<VAR>inst✝⁵ : Module R✝ N<VAR>inst✝⁴ : AddCommMonoid P<VAR>inst✝³ : Module R✝ P<VAR>α : Type u_7<VAR>β : Type u_8<VAR>R : Type u_9<VAR>M : Type u_10<VAR>inst✝² : Semiring R<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>f : α →₀ β →₀ M<VAR>xy : α × β<GOAL>((finsuppProdLEquiv R).symm f) xy = (f xy.1) xy.2
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h1 : IsPurelyInseparable F E<VAR>h2 : IsPurelyInseparable E K<GOAL>IsPurelyInseparable F K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h1 : IsPurelyInseparable F E<VAR>h2 : IsPurelyInseparable E K<VAR>q : ℕ<VAR>h✝ : ExpChar F q<GOAL>IsPurelyInseparable F K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>h1 : IsPurelyInseparable F E<VAR>h2 : IsPurelyInseparable E K<VAR>q : ℕ<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<GOAL>IsPurelyInseparable F K
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>q : ℕ<VAR>h2 : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range<VAR>h1 : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<GOAL>∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap F K).range
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁶ : Field F<VAR>inst✝⁵ : Field E<VAR>inst✝⁴ : Algebra F E<VAR>K : Type w<VAR>inst✝³ : Field K<VAR>inst✝² : Algebra F K<VAR>inst✝¹ : Algebra E K<VAR>inst✝ : IsScalarTower F E K<VAR>q : ℕ<VAR>h2✝ : ∀ (x : K), ∃ n, x ^ q ^ n ∈ (algebraMap E K).range<VAR>h1✝ : ∀ (x : E), ∃ n, x ^ q ^ n ∈ (algebraMap F E).range<VAR>h✝ : ExpChar F q<VAR>this : ExpChar E q<VAR>x : K<VAR>n : ℕ<VAR>y : E<VAR>h2 : (algebraMap E K) y = x ^ q ^ n<VAR>m : ℕ<VAR>z : F<VAR>h1 : (algebraMap F E) z = y ^ q ^ m<GOAL>(algebraMap F K) z = x ^ q ^ (n + m)
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>t : Set ℝ<VAR>hfs : HasConstantSpeedOnWith f s l<VAR>hft : HasConstantSpeedOnWith f t l<VAR>x : ℝ<VAR>hs : IsGreatest s x<VAR>ht : IsLeast t x<GOAL>HasConstantSpeedOnWith f (s ∪ t) l
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : ℝ → E<VAR>s : Set ℝ<VAR>l : ℝ≥0<VAR>t : Set ℝ<VAR>hfs : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))<VAR>hft : ∀ ⦃x : ℝ⦄, x ∈ t → ∀ ⦃y : ℝ⦄, y ∈ t → x ≤ y → eVariationOn f (t ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))<VAR>x : ℝ<VAR>hs : IsGreatest s x<VAR>ht : IsLeast t x<GOAL>∀ ⦃x : ℝ⦄, x ∈ s ∪ t → ∀ ⦃y : ℝ⦄, y ∈ s ∪ t → x ≤ y → eVariationOn f ((s ∪ t) ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : Group α<VAR>s t : Set α<VAR>a b : α<GOAL>(fun x => x * a) ⁻¹' {b} = {b * a⁻¹}
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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<GOAL>(zeroRootSubalgebra R L H).normalizer = zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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<GOAL>(zeroRootSubalgebra R L H).normalizer ≤ zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x : L<VAR>hx : x ∈ (zeroRootSubalgebra R L H).normalizer<GOAL>x ∈ zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x : L<VAR>hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H<GOAL>x ∈ zeroRootSubalgebra R L H
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x : L<VAR>hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H<GOAL>∀ (y : ↥H), ∃ k, ((toEnd R (↥H) L) y ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x : L<VAR>hx : ∀ y ∈ zeroRootSubalgebra R L H, ⁅x, y⁆ ∈ zeroRootSubalgebra R L H<VAR>y : L<VAR>hy : y ∈ H<GOAL>∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x y : L<VAR>hy : y ∈ H<VAR>hx : ⁅x, y⁆ ∈ zeroRootSubalgebra R L H<GOAL>∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x y : L<VAR>hy : y ∈ H<VAR>hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0<GOAL>∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x y : L<VAR>hy : y ∈ H<VAR>hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0<VAR>k : ℕ<VAR>hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅x, y⁆ = 0<GOAL>∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x y : L<VAR>hy : y ∈ H<VAR>hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0<VAR>k : ℕ<VAR>hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0<GOAL>∃ k, ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) 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>H : LieSubalgebra R L<VAR>inst✝⁴ : IsNilpotent R ↥H<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>x y : L<VAR>hy : y ∈ H<VAR>hx : ∀ (y_1 : ↥H), ∃ k, ((toEnd R (↥H) L) y_1 ^ k) ⁅x, y⁆ = 0<VAR>k : ℕ<VAR>hk : ((toEnd R (↥H) L) ⟨y, hy⟩ ^ k) ⁅y, x⁆ = 0<GOAL>((toEnd R (↥H) L) ⟨y, hy⟩ ^ (k + 1)) x = 0
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>hdom : f.domain ≠ ⊤<GOAL>∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module ℝ E<VAR>s : ConvexCone ℝ E<VAR>f : E →ₗ.[ℝ] ℝ<VAR>nonneg : ∀ (x : ↥f.domain), ↑x ∈ s → 0 ≤ ↑f x<VAR>dense : ∀ (y : E), ∃ x, ↑x + y ∈ s<VAR>hdom : f.domain ≠ ⊤<VAR>y : E<VAR>hy : y ∉ f.domain<GOAL>∃ g, f < g ∧ ∀ (x : ↥g.domain), ↑x ∈ s → 0 ≤ ↑g x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{?u.9364, u_1} C<VAR>inst✝⁶ : Category.{?u.9368, u_2} D<VAR>inst✝⁵ : Category.{?u.9372, u_3} E<VAR>inst✝⁴ : Category.{?u.9376, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>m + n + a = a''
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>E : Type u_3<VAR>E' : Type u_4<VAR>inst✝⁷ : Category.{u_7, u_1} C<VAR>inst✝⁶ : Category.{u_6, u_2} D<VAR>inst✝⁵ : Category.{?u.9372, u_3} E<VAR>inst✝⁴ : Category.{?u.9376, u_4} E'<VAR>A : Type u_5<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift D A<VAR>inst✝¹ : HasShift E A<VAR>inst✝ : HasShift E' A<VAR>F G H : SingleFunctors C D A<VAR>n m a a' a'' : A<VAR>ha' : n + a = a'<VAR>ha'' : m + a' = a''<VAR>X : C<GOAL>(F.shiftIso (m + n) a a'' ⋯).inv.app X = (F.shiftIso n a a' ha').inv.app X ≫ (shiftFunctor D n).map ((F.shiftIso m a' a'' ha'').inv.app X) ≫ (shiftFunctorAdd D m n).inv.app ((F.functor a'').obj X)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : Preorder β<VAR>s t : Finset α<VAR>f : Finset α → β<GOAL>StrictMono f ↔ ∀ (s : Finset α) ⦃a : α⦄ (ha : a ∉ s), f s < f (cons a s ha)