ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>P ?m.19557 (↑(e.symm ≫ₕ e').symm ⁻¹' (↑e.symm ⁻¹' s)) (↑e' x) ↔ P (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>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>(g ∘ ↑e.symm) ∘ ↑(e.symm ≫ₕ e').symm =ᶠ[𝓝 (↑e' x)] ?m.19557
<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>g : M → H'<VAR>he : e ∈ maximalAtlas M G<VAR>xe : x ∈ e.source<VAR>he' : e' ∈ maximalAtlas M G<VAR>xe' : x ∈ e'.source<GOAL>H → H'
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<GOAL>(↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>hr : r < 0<GOAL>(↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(↑(unitLattice K) ∩ Metric.closedBall 0 r).Finite
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>F : Type u_3<VAR>K : Type u_4<VAR>P Q : Cubic R<VAR>a b c d a' b' c' d' : R<VAR>inst✝ : Semiring R<VAR>ha : P.a = 0<VAR>hb : P.b = 0<VAR>hc : P.c = 0<VAR>hd : P.d = 0<GOAL>P.toPoly.degree = ⊥
<VAR>a b c d : ℝ≥0∞<VAR>r p✝ q✝ : ℝ≥0<VAR>p q : ℝ<VAR>h : 0 ≤ q<GOAL>ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<GOAL>∀ᶠ (n : ℕ) in Filter.atTop, f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<GOAL>Set.Ici k ⊆ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<VAR>k' : ℕ<VAR>hk' : k ≤ k'<GOAL>k' ∈ {x | (fun n => f ^ n • val z ∈ ⇑(algebraMap A (at Submonoid.powers f)) '' ↑(𝒜 (n • m))) x}
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<VAR>k' : ℕ<VAR>hk' : k ≤ k'<GOAL>∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<VAR>k' : ℕ<VAR>hk' : k ≤ k'<VAR>hfk : ¬f ^ k = 0<GOAL>∃ x ∈ 𝒜 (k' • m), (algebraMap A (at Submonoid.powers f)) x = f ^ k' • val z
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<VAR>k' : ℕ<VAR>hk' : k ≤ k'<VAR>hfk : ¬f ^ k = 0<GOAL>∃ x ∈ 𝒜 ((k' - k + k) • m), (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) * num z)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>inst✝⁵ : AddCommMonoid ι<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ι → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>x : Submonoid A<VAR>f : A<VAR>m : ι<VAR>hf : f ∈ 𝒜 m<VAR>z : Away 𝒜 f<VAR>k : ℕ<VAR>hk : f ^ k = den z<VAR>k' : ℕ<VAR>hk' : k ≤ k'<VAR>hfk : ¬f ^ k = 0<GOAL>∃ x ∈ 𝒜 ((k' - k) • m + deg z), (algebraMap A (at Submonoid.powers f)) x = (algebraMap A (at Submonoid.powers f)) (f ^ (k' - k) • num z)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : CommMonoid α<VAR>l : List α<GOAL>∏ i : Fin l.length, l[↑i] = l.prod
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ W X Y Z : C<VAR>inst✝¹ : HasBinaryProduct W Y<VAR>inst✝ : HasBinaryProduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>lift (fst ≫ g) (snd ≫ g') = map g g'
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>X✝ Y✝ W X Y Z : C<VAR>inst✝¹ : HasBinaryProduct W Y<VAR>inst✝ : HasBinaryProduct X Z<VAR>g : W ⟶ X<VAR>g' : Y ⟶ Z<GOAL>lift fst snd ≫ map g g' = map g g'
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<GOAL>∃ x ∈ f '' s, ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this : (comap f l ⊓ 𝓟 s).NeBot<GOAL>∃ x ∈ f '' s, ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<GOAL>∃ x ∈ f '' s, ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<GOAL>∃ x ∈ f '' s, ClusterPt x l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<GOAL>ClusterPt (f x) l
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : X → Y<VAR>hs : IsLindelof s<VAR>hf : ContinuousOn f s<VAR>l : Filter Y<VAR>lne : l.NeBot<VAR>inst✝ : CountableInterFilter l<VAR>ls : l ≤ 𝓟 (f '' s)<VAR>this✝¹ : (comap f l ⊓ 𝓟 s).NeBot<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : ClusterPt x (comap f l ⊓ 𝓟 s)<VAR>this✝ : (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)).NeBot<VAR>this : Tendsto f (𝓝 x ⊓ (comap f l ⊓ 𝓟 s)) (𝓝 (f x) ⊓ l)<GOAL>ClusterPt (f x) l
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : Category.{v₂, u₂} D<VAR>L₁ L₂ : C ⥤ D<VAR>R₁ R₂ : D ⥤ C<VAR>adj₁ : L₁ ⊣ R₁<VAR>adj₂ : L₂ ⊣ R₂<VAR>x✝ : D<GOAL>𝟙 (R₁.obj x✝) ≫ (adj₁.unit.app (R₁.obj x✝) ≫ R₁.map (𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝)) ≫ 𝟙 (L₁.obj (R₁.obj x✝))) ≫ R₁.map (adj₁.counit.app x✝)) ≫ 𝟙 (R₁.obj x✝) = 𝟙 (R₁.obj x✝)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConcaveOn 𝕜 s (f • g)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : LinearOrderedCommRing 𝕜<VAR>inst✝⁹ : LinearOrderedCommRing E<VAR>inst✝⁸ : LinearOrderedAddCommGroup F<VAR>inst✝⁷ : Module 𝕜 E<VAR>inst✝⁶ : Module 𝕜 F<VAR>inst✝⁵ : Module E F<VAR>inst✝⁴ : IsScalarTower 𝕜 E F<VAR>inst✝³ : SMulCommClass 𝕜 E F<VAR>inst✝² : OrderedSMul 𝕜 E<VAR>inst✝¹ : OrderedSMul 𝕜 F<VAR>inst✝ : OrderedSMul E F<VAR>s : Set 𝕜<VAR>f : 𝕜 → E<VAR>g : 𝕜 → F<VAR>hf : ConvexOn 𝕜 s f<VAR>hg : ConcaveOn 𝕜 s g<VAR>hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → 0 ≤ f x<VAR>hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0<VAR>hfg : AntivaryOn f g s<GOAL>ConvexOn 𝕜 s (f • -g)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>inst✝³ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝ : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>L M : Ideal R<VAR>hL : L ∣ I<VAR>hM : M ∣ I<GOAL>↑((idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩) ∣ ↑((idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩) ↔ L ∣ M
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>K : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : Field K<VAR>inst✝³ : IsDedekindDomain A<VAR>I : Ideal R<VAR>J : Ideal A<VAR>B : Type u_4<VAR>inst✝² : CommRing B<VAR>inst✝¹ : IsDedekindDomain B<VAR>L✝ : Ideal B<VAR>inst✝ : IsDedekindDomain R<VAR>f : R ⧸ I ≃+* A ⧸ J<VAR>L M : Ideal R<VAR>hL : L ∣ I<VAR>hM : M ∣ I<GOAL>(idealFactorsEquivOfQuotEquiv f) ⟨M, hM⟩ ≤ (idealFactorsEquivOfQuotEquiv f) ⟨L, hL⟩ ↔ ⟨M, hM⟩ ≤ ⟨L, hL⟩
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>n✝ m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ q r p : R[X]<VAR>n d : ℕ<GOAL>(X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>M : Type u_3<VAR>M₁ : Type u_4<VAR>M₂ : Type u_5<VAR>N : Type u_6<VAR>inst✝⁷ : Monoid R<VAR>inst✝⁶ : Monoid S<VAR>σ : R → S<VAR>inst✝⁵ : MulAction R M<VAR>inst✝⁴ : MulAction S N<VAR>inst✝³ : MulAction R M₁<VAR>inst✝² : MulAction R M₂<VAR>F : Type u_7<VAR>h : F<VAR>inst✝¹ : FunLike F M N<VAR>inst✝ : MulActionSemiHomClass F σ M N<VAR>c : R<VAR>s : Set M<VAR>t : Set N<GOAL>⇑h '' (c • s) = σ c • ⇑h '' s
<VAR>θ : Angle<GOAL>θ.toReal = π / 2 ↔ θ = ↑(π / 2)
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n p : R<VAR>k : ℕ<VAR>inst✝ : NoZeroDivisors R<GOAL>¬IsPrimePow 0
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n p : R<VAR>k : ℕ<VAR>inst✝ : NoZeroDivisors R<GOAL>∀ (x : R) (x_1 : ℕ), 0 < x_1 → x ^ x_1 = 0 → ¬Prime x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k : ℕ<VAR>inst✝ : NoZeroDivisors R<VAR>x : R<VAR>n : ℕ<VAR>_hn : 0 < n<VAR>hx : x ^ n = 0<GOAL>¬Prime x
<VAR>R : Type u_1<VAR>inst✝¹ : CommMonoidWithZero R<VAR>n✝ p : R<VAR>k : ℕ<VAR>inst✝ : NoZeroDivisors R<VAR>x : R<VAR>n : ℕ<VAR>_hn : 0 < n<VAR>hx : x ^ n = 0<GOAL>¬Prime 0
<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>inst✝ : IsNoetherian R M<GOAL>IsNilpotent R L M ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
<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>inst✝ : IsNoetherian R M<GOAL>(∀ (x : ↥(toEnd R L M).range), _root_.IsNilpotent ((toEnd R (↥(toEnd R L M).range) M) x)) ↔ ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)
<VAR>G : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : MulAction G β<VAR>a₁ a₂ : α<GOAL>a₁ ∈ orbit G a₂ ↔ a₂ ∈ orbit G a₁
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<GOAL>(limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫ (HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫ (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫ (J.plusMap (limit.π F k)).app (op X) = S.π.app k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<GOAL>limit.lift (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) S ≫ ((HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫ (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫ (J.plusMap (limit.π F k)).app (op X) = (limit.isLimit (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).lift S ≫ (limit.cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))).π.app k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<GOAL>((HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).inv ≫ (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).inv) ≫ (J.plusMap (limit.π F k)).app (op X) = limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<GOAL>(J.plusMap (limit.π F k)).app (op X) = (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ (HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).inv ≫ limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>colimit.ι (J.diagram (limit F) (unop (op X))) j ≫ (J.plusMap (limit.π F k)).app (op X) = colimit.ι (J.diagram (limit F) (unop (op X))) j ≫ (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ (HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).inv ≫ limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>colimit.ι (J.diagram (limit F) X) j ≫ colimMap (J.diagramNatTrans (limit.π F k) X) = colimit.ι (J.diagram (limit F) X) j ≫ (HasColimit.isoOfNatIso ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X)))).hom ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ (HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).inv ≫ limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k
<VAR>C : Type u<VAR>inst✝¹⁰ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>D : Type w<VAR>inst✝⁹ : Category.{max v u, w} D<VAR>inst✝⁸ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)<VAR>inst✝⁷ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D<VAR>inst✝⁶ : ConcreteCategory D<VAR>inst✝⁵ : (X : C) → PreservesColimitsOfShape (J.Cover X)ᵒᵖ (forget D)<VAR>K : Type (max v u)<VAR>inst✝⁴ : SmallCategory K<VAR>inst✝³ : FinCategory K<VAR>inst✝² : HasLimitsOfShape K D<VAR>inst✝¹ : PreservesLimitsOfShape K (forget D)<VAR>inst✝ : ReflectsLimitsOfShape K (forget D)<VAR>F : K ⥤ Cᵒᵖ ⥤ D<VAR>X : C<VAR>S : Cone (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X))<VAR>k : K<VAR>j : (J.Cover (unop (op X)))ᵒᵖ<GOAL>(J.diagramNatTrans (limit.π F k) X).app j ≫ colimit.ι (J.diagram (F.obj k) X) j = ((isLimitOfPreserves (J.diagramFunctor D X) (limit.isLimit F)).conePointUniqueUpToIso (limit.isLimit (F ⋙ J.diagramFunctor D X))).hom.app j ≫ colimit.ι (limit (F ⋙ J.diagramFunctor D X)) j ≫ (colimitLimitIso (F ⋙ J.diagramFunctor D X)).hom ≫ (HasLimit.isoOfNatIso (NatIso.ofComponents (fun k => colimitObjIsoColimitCompEvaluation (F ⋙ J.diagramFunctor D X).flip k) ⋯).symm).inv ≫ limit.π (F ⋙ J.plusFunctor D ⋙ (evaluation Cᵒᵖ D).obj (op X)) k