ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>hai : AffineIndependent k p<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>h : IsEmpty ι<GOAL>AffineIndependent k (⇑f ∘ p)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>hai : AffineIndependent k p<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>h : Nonempty ι<GOAL>AffineIndependent k (⇑f ∘ p)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>hai : AffineIndependent k p<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>i : ι<GOAL>AffineIndependent k (⇑f ∘ p)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>i : ι<VAR>hai : LinearIndependent k fun i_1 => p ↑i_1 -ᵥ p i<GOAL>AffineIndependent k (⇑f ∘ p)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>i : ι<VAR>hai : LinearIndependent k fun i_1 => p ↑i_1 -ᵥ p i<GOAL>LinearIndependent k fun i_1 => f.linear (p ↑i_1 -ᵥ p i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝⁶ : Ring k<VAR>inst✝⁵ : AddCommGroup V<VAR>inst✝⁴ : Module k V<VAR>inst✝³ : AffineSpace V P<VAR>ι : Type u_4<VAR>V₂ : Type u_5<VAR>P₂ : Type u_6<VAR>inst✝² : AddCommGroup V₂<VAR>inst✝¹ : Module k V₂<VAR>inst✝ : AffineSpace V₂ P₂<VAR>p : ι → P<VAR>f : P →ᵃ[k] P₂<VAR>hf : Injective ⇑f<VAR>i : ι<VAR>hai : LinearIndependent k fun i_1 => p ↑i_1 -ᵥ p i<VAR>hf' : LinearMap.ker f.linear = ⊥<GOAL>LinearIndependent k fun i_1 => f.linear (p ↑i_1 -ᵥ p i)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>Convex 𝕜 (convexJoin 𝕜 s t)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<GOAL>∀ ⦃x : E⦄, (∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), x ∈ [i-[𝕜]i_1]) → ∀ ⦃y : E⦄, (∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), y ∈ [i-[𝕜]i_1]) → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → ∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), a • x + b • y ∈ [i-[𝕜]i_1]
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x y : E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ s<VAR>y₁ : E<VAR>hy₁ : y₁ ∈ t<VAR>a₁ b₁ : 𝕜<VAR>ha₁ : 0 ≤ a₁<VAR>hb₁ : 0 ≤ b₁<VAR>hab₁ : a₁ + b₁ = 1<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ s<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ t<VAR>a₂ b₂ : 𝕜<VAR>ha₂ : 0 ≤ a₂<VAR>hb₂ : 0 ≤ b₂<VAR>hab₂ : a₂ + b₂ = 1<VAR>p q : 𝕜<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<VAR>hpq : p + q = 1<GOAL>∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i-[𝕜]i_1]
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x✝ y : E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ s<VAR>y₁ : E<VAR>hy₁ : y₁ ∈ t<VAR>a₁ b₁ : 𝕜<VAR>ha₁ : 0 ≤ a₁<VAR>hb₁ : 0 ≤ b₁<VAR>hab₁ : a₁ + b₁ = 1<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ s<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ t<VAR>a₂ b₂ : 𝕜<VAR>ha₂ : 0 ≤ a₂<VAR>hb₂ : 0 ≤ b₂<VAR>hab₂ : a₂ + b₂ = 1<VAR>p q : 𝕜<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<VAR>hpq : p + q = 1<VAR>x : E<VAR>hxs : x ∈ s<VAR>hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂<GOAL>∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i-[𝕜]i_1]
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s t u : Set E<VAR>x✝ y✝ : E<VAR>hs : Convex 𝕜 s<VAR>ht : Convex 𝕜 t<VAR>x₁ : E<VAR>hx₁ : x₁ ∈ s<VAR>y₁ : E<VAR>hy₁ : y₁ ∈ t<VAR>a₁ b₁ : 𝕜<VAR>ha₁ : 0 ≤ a₁<VAR>hb₁ : 0 ≤ b₁<VAR>hab₁ : a₁ + b₁ = 1<VAR>x₂ : E<VAR>hx₂ : x₂ ∈ s<VAR>y₂ : E<VAR>hy₂ : y₂ ∈ t<VAR>a₂ b₂ : 𝕜<VAR>ha₂ : 0 ≤ a₂<VAR>hb₂ : 0 ≤ b₂<VAR>hab₂ : a₂ + b₂ = 1<VAR>p q : 𝕜<VAR>hp : 0 ≤ p<VAR>hq : 0 ≤ q<VAR>hpq : p + q = 1<VAR>x : E<VAR>hxs : x ∈ s<VAR>hx : (p * a₁ + q * a₂) • x = (p * a₁) • x₁ + (q * a₂) • x₂<VAR>y : E<VAR>hyt : y ∈ t<VAR>hy : (p * b₁ + q * b₂) • y = (p * b₁) • y₁ + (q * b₂) • y₂<GOAL>∃ i, ∃ (_ : i ∈ s), ∃ i_1, ∃ (_ : i_1 ∈ t), p • (a₁ • x₁ + b₁ • y₁) + q • (a₂ • x₂ + b₂ • y₂) ∈ [i-[𝕜]i_1]
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c d : ℝ<VAR>f : ℝ → E<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<GOAL>‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>ha' : SpectrumRestricts a ⇑Complex.reCLM<GOAL>‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a
<VAR>A : Type u_1<VAR>inst✝⁸ : NormedRing A<VAR>inst✝⁷ : StarRing A<VAR>inst✝⁶ : CstarRing A<VAR>inst✝⁵ : CompleteSpace A<VAR>inst✝⁴ : NormedAlgebra ℂ A<VAR>inst✝³ : StarModule ℂ A<VAR>inst✝² : PartialOrder A<VAR>inst✝¹ : StarOrderedRing A<VAR>inst✝ : Nontrivial A<VAR>a : A<VAR>ha : autoParam (IsSelfAdjoint a) _auto✝<VAR>ha' : SpectrumRestricts a ⇑Complex.reCLM<GOAL>(spectralRadius ℝ a).toReal ∈ spectrum ℝ a ∨ -(spectralRadius ℝ a).toReal ∈ spectrum ℝ a
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>(homogeneousCore 𝒜 I).toIdeal = I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>I ≤ homogeneousCore' 𝒜 I
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : SetLike σ A<VAR>inst✝³ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : AddMonoid ι<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<VAR>x : A<VAR>hx : x ∈ I<GOAL>x ∈ homogeneousCore' 𝒜 I
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w✝ : V<VAR>h : M.IsMatching<VAR>v✝ : V<VAR>hv : v✝ ∈ M.verts<VAR>w : V<VAR>hvw : M.Adj v✝ w<VAR>hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w<GOAL>∃! w, (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w
<VAR>V : Type u_1<VAR>G G' : SimpleGraph V<VAR>M M' : G.Subgraph<VAR>v w✝ : V<VAR>h : M.IsMatching<VAR>v✝ : V<VAR>hv : v✝ ∈ M.verts<VAR>w : V<VAR>hvw : M.Adj v✝ w<VAR>hw : ∀ (y : V), (fun w => M.Adj v✝ w) y → y = w<GOAL>(fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) w ∧ ∀ (y : V), (fun w => (M.induce (M.verts ∩ (G.connectedComponentMk v✝).supp)).Adj v✝ w) y → y = w
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X✝ Y✝ : C × C<VAR>f : X✝ ⟶ Y✝<VAR>Z : C × C<GOAL>__src✝.map f ▷ __src✝.obj Z ≫ tensor_μ C Y✝ Z = tensor_μ C X✝ Z ≫ __src✝.map (f ▷ Z)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X✝ Y✝ Z : C × C<VAR>f : X✝ ⟶ Y✝<GOAL>__src✝.obj Z ◁ __src✝.map f ≫ tensor_μ C Z Y✝ = tensor_μ C Z X✝ ≫ __src✝.map (Z ◁ f)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X Y Z : C × C<GOAL>tensor_μ C X Y ▷ __src✝.obj Z ≫ tensor_μ C (X ⊗ Y) Z ≫ __src✝.map (α_ X Y Z).hom = (α_ (__src✝.obj X) (__src✝.obj Y) (__src✝.obj Z)).hom ≫ __src✝.obj X ◁ tensor_μ C Y Z ≫ tensor_μ C X (Y ⊗ Z)
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>x✝ : C × C<VAR>X₁ X₂ : C<GOAL>(λ_ (__src✝.obj (X₁, X₂))).hom = (λ_ (𝟙_ C)).inv ▷ __src✝.obj (X₁, X₂) ≫ tensor_μ C (𝟙_ (C × C)) (X₁, X₂) ≫ __src✝.map (λ_ (X₁, X₂)).hom
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>x✝ : C × C<VAR>X₁ X₂ : C<GOAL>(ρ_ (__src✝.obj (X₁, X₂))).hom = __src✝.obj (X₁, X₂) ◁ (λ_ (𝟙_ C)).inv ≫ tensor_μ C (X₁, X₂) (𝟙_ (C × C)) ≫ __src✝.map (ρ_ (X₁, X₂)).hom
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>ha : 0 ≤ a<VAR>hb : 1 ≤ b<GOAL>a / b ≤ a
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesLimit F G<VAR>inst✝³ : HasLimit F<VAR>inst✝² : PreservesLimitsOfShape J G<VAR>inst✝¹ : HasLimitsOfShape J D<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<GOAL>(lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom = ((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesLimit F G<VAR>inst✝³ : HasLimit F<VAR>inst✝² : PreservesLimitsOfShape J G<VAR>inst✝¹ : HasLimitsOfShape J D<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<GOAL>∀ (j : J), ((lim ⋙ G).map f ≫ ((fun F => preservesLimitIso G F) Y✝).hom) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j = (((fun F => preservesLimitIso G F) X✝).hom ≫ ((whiskeringRight J C D).obj G ⋙ lim).map f) ≫ limit.π (((whiskeringRight J C D).obj G).obj Y✝) j
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>G : C ⥤ D<VAR>J : Type w<VAR>inst✝⁵ : Category.{w', w} J<VAR>F : J ⥤ C<VAR>inst✝⁴ : PreservesLimit F G<VAR>inst✝³ : HasLimit F<VAR>inst✝² : PreservesLimitsOfShape J G<VAR>inst✝¹ : HasLimitsOfShape J D<VAR>inst✝ : HasLimitsOfShape J C<VAR>X✝ Y✝ : J ⥤ C<VAR>f : X✝ ⟶ Y✝<VAR>j : J<GOAL>(G.map (limMap f) ≫ (preservesLimitIso G Y✝).hom) ≫ limit.π (Y✝ ⋙ G) j = ((preservesLimitIso G X✝).hom ≫ limMap (whiskerRight f G)) ≫ limit.π (Y✝ ⋙ G) j
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : CommSemiring P<VAR>inst✝⁴ : CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<GOAL>IsLocalizedModule M (toKerIsLocalization S Q g ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : CommSemiring P<VAR>inst✝⁴ : CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<VAR>e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) := LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯<GOAL>IsLocalizedModule M (toKerIsLocalization S Q g ⋯)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>P : Type u_3<VAR>Q : Type u_4<VAR>inst✝⁷ : CommSemiring R<VAR>inst✝⁶ : CommSemiring S<VAR>inst✝⁵ : CommSemiring P<VAR>inst✝⁴ : CommSemiring Q<VAR>M : Submonoid R<VAR>T : Submonoid P<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra P Q<VAR>inst✝¹ : IsLocalization M S<VAR>inst✝ : IsLocalization T Q<VAR>g : R →+* P<VAR>hT : Submonoid.map g M = T<VAR>e : ↥(Ideal.map (algebraMap R S) (ker g)) ≃ₛₗ[id S] ↥(ker (IsLocalization.map Q g ⋯)) := LinearEquiv.ofEq (Ideal.map (algebraMap R S) (ker g)) (ker (IsLocalization.map Q g ⋯)) ⋯<GOAL>IsLocalizedModule M (↑(LinearEquiv.restrictScalars R e) ∘ₗ Algebra.idealMap S (ker g))
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<VAR>x' : S<VAR>hx' : x' ∈ ↑A.toSubsemiring<VAR>hx'' : ↑g x' = ↑y ^ n • (algebraMap S S') x<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<VAR>x' : S<VAR>hx' : x' ∈ ↑A.toSubsemiring<VAR>hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<VAR>x' : S<VAR>hx' : x' ∈ ↑A.toSubsemiring<VAR>hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)<VAR>a : ↥M<VAR>ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)<GOAL>∃ m, m • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<VAR>x' : S<VAR>hx' : x' ∈ ↑A.toSubsemiring<VAR>hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)<VAR>a : ↥M<VAR>ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)<GOAL>(a * y ^ n) • x ∈ A
<VAR>R S : Type u<VAR>inst✝⁹ : CommRing R<VAR>inst✝⁸ : CommRing S<VAR>M✝ : Submonoid R<VAR>N : Submonoid S<VAR>R' S' : Type u<VAR>inst✝⁷ : CommRing R'<VAR>inst✝⁶ : CommRing S'<VAR>f : R →+* S<VAR>inst✝⁵ : Algebra R R'<VAR>inst✝⁴ : Algebra S S'<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R S'<VAR>inst✝¹ : IsScalarTower R S S'<VAR>M : Submonoid S<VAR>inst✝ : IsLocalization M S'<VAR>x : S<VAR>s : Finset S'<VAR>A : Subalgebra R S<VAR>hA₁ : ↑(finsetIntegerMultiple M s) ⊆ ↑A<VAR>hA₂ : M ≤ A.toSubmonoid<VAR>hx : (algebraMap S S') x ∈ Algebra.adjoin R ↑s<VAR>g : S →ₐ[R] S' := IsScalarTower.toAlgHom R S S'<VAR>y : ↥M := commonDenomOfFinset M s<VAR>hx₁ : ↑y • ↑s = ⇑g '' ↑(finsetIntegerMultiple M s)<VAR>n : ℕ<VAR>hn : ∀ n_1 ≥ n, ↑y ^ n_1 • (algebraMap S S') x ∈ Subalgebra.map g A<VAR>x' : S<VAR>hx' : x' ∈ ↑A.toSubsemiring<VAR>hx'' : ↑g x' = (algebraMap S S') (↑y ^ n * x)<VAR>a : ↥M<VAR>ha₂ : ↑a * x' = ↑a * (↑y ^ n * x)<GOAL>(a * y ^ n) • x = x' * ↑a
<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 L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>h : ∀ (x : L), _root_.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>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>h : ∀ (x : L), _root_.IsNilpotent ((toEnd R L M) x)<GOAL>LieModule.IsNilpotent R (↥(toEnd R L M).range) 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>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<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>inst✝ : IsNoetherian R L<VAR>M : Type u_1<VAR>_i1 : AddCommGroup M<VAR>_i2 : Module R M<VAR>_i3 : LieRingModule L M<VAR>_i4 : LieModule R L M<VAR>L' : LieSubalgebra R (Module.End R M) := (toEnd R L M).range<VAR>h : ∀ (y : ↥L'), _root_.IsNilpotent ↑y<VAR>s : Set (LieSubalgebra R ↥L') := {K | IsEngelian R ↥K}<VAR>hs : s.Nonempty<GOAL>LieModule.IsNilpotent R (↥L') M