ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : (i : ι) → β i<VAR>s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<GOAL>i ∈ { toFun := f, support' := Trunc.mk s }.support ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : (i : ι) → β i<VAR>s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<GOAL>i ∈ Finset.filter (fun i => { toFun := f, support' := Trunc.mk s } i ≠ 0) (↑s).toFinset ↔ { toFun := f, support' := Trunc.mk s } i ≠ 0
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : (i : ι) → Zero (β i)<VAR>inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)<VAR>i : ι<VAR>f : (i : ι) → β i<VAR>s : { s // ∀ (i : ι), i ∈ s ∨ f i = 0 }<GOAL>i ∈ ↑s ∧ f i ≠ 0 ↔ f i ≠ 0
<VAR>E : ℕ → Type u_1<VAR>α : Type u_2<VAR>x : ℕ → α<VAR>n : ℕ<VAR>y : ℕ → α<GOAL>(∀ i < n, y i = x i) ↔ res y n = res x n
<VAR>n m l : ℕ<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
<VAR>n m l : ℕ<VAR>hnl : n ≤ l<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
<VAR>n m l : ℕ<VAR>hln : l ≤ n<GOAL>filter (fun x => decide (l ≤ x)) (Ico n m) = Ico (max n l) m
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<GOAL>f ∈ ↑(vanishingIdeal t) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<GOAL>(∀ (i : ProjectiveSpectrum 𝒜), f ∈ (⨅ (_ : i ∈ t), i.asHomogeneousIdeal).toIdeal) ↔ f ∈ {f | ∀ x ∈ t, f ∈ x.asHomogeneousIdeal}
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<VAR>x : ProjectiveSpectrum 𝒜<GOAL>f ∈ (⨅ (_ : x ∈ t), x.asHomogeneousIdeal).toIdeal ↔ x ∈ t → f ∈ x.asHomogeneousIdeal
<VAR>C✝ : Type u<VAR>𝒞 : Category.{v, u} C✝<VAR>inst✝² : MonoidalCategory C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : MonoidalCategory C<VAR>U V W X✝ Y✝ Z✝ X X' Y Y' Z Z' : C<VAR>f : X ⟶ X'<VAR>g : Y ⟶ Y'<VAR>h : Z ⟶ Z'<GOAL>(f ⊗ g) ⊗ h = (α_ X Y Z).hom ≫ (f ⊗ g ⊗ h) ≫ (α_ X' Y' Z').inv
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s t : Set α<VAR>a : α<VAR>h : IsUpperSet sᶜ<GOAL>IsLowerSet s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝¹ : LE α<VAR>inst✝ : LE β<VAR>s t : Set α<VAR>a : α<VAR>h : IsUpperSet sᶜ<GOAL>s = sᶜᶜ
<VAR>K : Type u<VAR>inst✝¹ : CommRing K<VAR>inst✝ : IsDomain K<VAR>p q : K[X]<VAR>hq : q ∈ K[X]⁰<GOAL>RatFunc.mk p q = { toFractionRing := IsLocalization.mk' (FractionRing K[X]) p ⟨q, hq⟩ }
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>s : Set (α × α)<VAR>hs : s ∈ 𝓤 α<VAR>x : α × α<VAR>h : x ∈ Prod.map Sum.inl Sum.inl ⁻¹' (Prod.map Sum.inl Sum.inl '' s ∪ range (Prod.map Sum.inr Sum.inr))<GOAL>x ∈ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>H : Type u_8<VAR>F : Type u_9<VAR>inst✝⁶ : MulOneClass M<VAR>inst✝⁵ : MulOneClass N<VAR>inst✝⁴ : FunLike F M N<VAR>inst✝³ : FunLike F G H<VAR>inst✝² : DivInvMonoid G<VAR>inst✝¹ : DivInvMonoid H<VAR>inst✝ : MonoidHomClass F G H<VAR>f : F<VAR>hf : ∀ (a : G), f a⁻¹ = (f a)⁻¹<VAR>g h : ι → G<VAR>x✝ : ι<GOAL>(⇑f ∘ (g / h)) x✝ = (⇑f ∘ g / ⇑f ∘ h) x✝
<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>as : Array α<VAR>motive : Nat → β → Prop<VAR>init : β<VAR>h0 : motive 0 init<VAR>f : β → α → m β<VAR>hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])<GOAL>SatisfiesM (motive as.size) (foldlM.loop f as as.size ⋯ as.size 0 init)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁸ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_3<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>M : Type u_4<VAR>inst✝¹⁴ : TopologicalSpace M<VAR>inst✝¹³ : ChartedSpace H M<VAR>inst✝¹² : SmoothManifoldWithCorners I M<VAR>E' : Type u_5<VAR>inst✝¹¹ : NormedAddCommGroup E'<VAR>inst✝¹⁰ : NormedSpace 𝕜 E'<VAR>H' : Type u_6<VAR>inst✝⁹ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E' H'<VAR>M' : Type u_7<VAR>inst✝⁸ : TopologicalSpace M'<VAR>inst✝⁷ : ChartedSpace H' M'<VAR>inst✝⁶ : SmoothManifoldWithCorners I' M'<VAR>E'' : Type u_8<VAR>inst✝⁵ : NormedAddCommGroup E''<VAR>inst✝⁴ : NormedSpace 𝕜 E''<VAR>H'' : Type u_9<VAR>inst✝³ : TopologicalSpace H''<VAR>I'' : ModelWithCorners 𝕜 E'' H''<VAR>M'' : Type u_10<VAR>inst✝² : TopologicalSpace M''<VAR>inst✝¹ : ChartedSpace H'' M''<VAR>e : PartialHomeomorph M H<VAR>e' : PartialHomeomorph M' H'<VAR>f f₁ : M → M'<VAR>s s₁ t : Set M<VAR>x : M<VAR>m n : ℕ∞<VAR>c : M'<VAR>inst✝ : One M'<GOAL>Smooth I I' 1
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.148403, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>inst✝³ : Mono S₁.f<VAR>inst✝² : Mono S₂.f<VAR>inst✝¹ : Mono φ.τ₁<VAR>inst✝ : Mono φ.τ₃<GOAL>Mono φ.τ₂
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.148403, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>inst✝³ : Mono S₁.f<VAR>inst✝² : Mono S₂.f<VAR>inst✝¹ : Mono φ.τ₁<VAR>inst✝ : Mono φ.τ₃<GOAL>∀ (P : C) (g : P ⟶ S₁.X₂), g ≫ φ.τ₂ = 0 → g = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.148403, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>inst✝³ : Mono S₁.f<VAR>inst✝² : Mono S₂.f<VAR>inst✝¹ : Mono φ.τ₁<VAR>inst✝ : Mono φ.τ₃<VAR>A : C<VAR>x₂ : A ⟶ S₁.X₂<VAR>hx₂ : x₂ ≫ φ.τ₂ = 0<GOAL>x₂ = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.148403, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>inst✝³ : Mono S₁.f<VAR>inst✝² : Mono S₂.f<VAR>inst✝¹ : Mono φ.τ₁<VAR>inst✝ : Mono φ.τ₃<VAR>A : C<VAR>x₂ : A ⟶ S₁.X₂<VAR>hx₂ : x₂ ≫ φ.τ₂ = 0<VAR>x₁ : A ⟶ S₁.X₁<VAR>hx₁ : x₁ ≫ S₁.f = x₂<GOAL>x₂ = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁸ : Category.{u_3, u_1} C<VAR>inst✝⁷ : Category.{?u.148403, u_2} D<VAR>inst✝⁶ : Preadditive C<VAR>inst✝⁵ : Preadditive D<VAR>S : ShortComplex C<VAR>inst✝⁴ : Balanced C<VAR>S₁ S₂ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h₁ : S₁.Exact<VAR>inst✝³ : Mono S₁.f<VAR>inst✝² : Mono S₂.f<VAR>inst✝¹ : Mono φ.τ₁<VAR>inst✝ : Mono φ.τ₃<VAR>A : C<VAR>x₂ : A ⟶ S₁.X₂<VAR>hx₂ : x₂ ≫ φ.τ₂ = 0<VAR>x₁ : A ⟶ S₁.X₁<VAR>hx₁ : x₁ ≫ S₁.f = x₂<GOAL>x₁ = 0
<VAR>E : Type u_1<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : MeasurableSpace E<VAR>inst✝¹² : BorelSpace E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝¹⁰ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>s : Set E<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ G = n)<VAR>ω : G [⋀^Fin n]→ₗ[ℝ] ℝ<VAR>v : Fin n → G<GOAL>ω.measure (parallelepiped v) = ENNReal.ofReal |ω v|
<VAR>E : Type u_1<VAR>inst✝¹⁵ : NormedAddCommGroup E<VAR>inst✝¹⁴ : NormedSpace ℝ E<VAR>inst✝¹³ : MeasurableSpace E<VAR>inst✝¹² : BorelSpace E<VAR>inst✝¹¹ : FiniteDimensional ℝ E<VAR>μ : Measure E<VAR>inst✝¹⁰ : μ.IsAddHaarMeasure<VAR>F : Type u_2<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace ℝ F<VAR>inst✝⁷ : CompleteSpace F<VAR>s : Set E<VAR>ι : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : Fintype ι<VAR>inst✝⁵ : DecidableEq ι<VAR>inst✝⁴ : NormedAddCommGroup G<VAR>inst✝³ : NormedSpace ℝ G<VAR>inst✝² : MeasurableSpace G<VAR>inst✝¹ : BorelSpace G<VAR>inst✝ : FiniteDimensional ℝ G<VAR>n : ℕ<VAR>_i : Fact (finrank ℝ G = n)<VAR>ω : G [⋀^Fin n]→ₗ[ℝ] ℝ<VAR>v : Fin n → G<GOAL>ω.measure (parallelepiped v) = ENNReal.ofReal |(ω ⇑(finBasisOfFinrankEq ℝ G ⋯) • (finBasisOfFinrankEq ℝ G ⋯).det) v|
<VAR>C✝ : Type u_1<VAR>inst✝⁵ : Category.{?u.2292, u_1} C✝<VAR>inst✝⁴ : MonoidalCategory C✝<VAR>inst✝³ : BraidedCategory C✝<VAR>C : Type u_2<VAR>inst✝² : Category.{u_3, u_2} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X Y W Z : Cᵒᵖ<GOAL>(tensor_μ Cᵒᵖ (X, W) (Y, Z)).unop = tensor_μ C (unop X, unop Y) (unop W, unop Z)
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<VAR>h_two : ENNReal.toReal 2 = 2<GOAL>‖f‖ ^ 2 = RCLike.re ⟪f, f⟫_𝕜
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<VAR>h_two : ENNReal.toReal 2 = 2<GOAL>eLpNorm (↑↑f) 2 μ ^ 2 = ∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝⁴ : RCLike 𝕜<VAR>inst✝³ : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace 𝕜 E<VAR>inst✝ : NormedAddCommGroup F<VAR>f : ↥(Lp E 2 μ)<VAR>h_two : ENNReal.toReal 2 = 2<GOAL>∫⁻ (a : α), ↑‖↑↑f a‖₊ ^ 2 ∂μ ≠ ⊤
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>ofTensorProduct I (ι → R) = ↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piScalarRight R (AdicCompletion I R) (AdicCompletion I R) ι)
<VAR>R : Type u_1<VAR>inst✝⁶ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R M<VAR>N : Type u_3<VAR>inst✝³ : AddCommGroup N<VAR>inst✝² : Module R N<VAR>ι : Type u_4<VAR>inst✝¹ : Fintype ι<VAR>inst✝ : DecidableEq ι<GOAL>ofTensorProduct I (ι → R) = (↑(piEquivOfFintype I fun x => R).symm ∘ₗ ↑(piEquivOfFintype I fun x => R)) ∘ₗ ofTensorProduct I (ι → R)
<VAR>X : Scheme<VAR>𝒰 : X.OpenCover<VAR>x y z : 𝒰.J<GOAL>𝒰.gluedCoverT' x y z ≫ 𝒰.gluedCoverT' y z x ≫ 𝒰.gluedCoverT' z x y ≫ pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z)) = pullback.fst (pullback.fst (𝒰.map x) (𝒰.map y)) (pullback.fst (𝒰.map x) (𝒰.map z))
<VAR>α : Type u<VAR>β : Type v<VAR>l : List α<VAR>x : α<VAR>xs : List α<VAR>n✝ : ℕ<VAR>d : α<VAR>n : ℕ<GOAL>l.getD n d = (l.get? n).getD d
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>𝒢 : Set C<VAR>h𝒢 : IsCoseparating 𝒢<GOAL>IsCoseparating ((proj S T).obj ⁻¹' 𝒢)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>S : D<VAR>T : C ⥤ D<VAR>𝒢 : Set C<VAR>h𝒢 : IsCoseparating 𝒢<VAR>X Y : StructuredArrow S T<VAR>f g : X ⟶ Y<VAR>hfg : ∀ G ∈ (proj S T).obj ⁻¹' 𝒢, ∀ (h : Y ⟶ G), f ≫ h = g ≫ h<VAR>G : C<VAR>hG : G ∈ 𝒢<VAR>h : Y.right ⟶ G<GOAL>f.right ≫ h = g.right ≫ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : NormedRing R<VAR>inst✝ : CompleteSpace R<VAR>x : R<VAR>h : ‖x‖ < 1<GOAL>∑' (i : ℕ), x ^ (i + 1) = ∑' (i : ℕ), x ^ i - 1
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>colimit.ι (F ⋙ evaluation R X) j ≫ colimMap (whiskerLeft F (restriction R (𝟙 X))) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).inv = colimit.ι (F ⋙ evaluation R X) j ≫ (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (colimit (F ⋙ evaluation R X))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>restrictionApp (𝟙 X) (F.obj j) ≫ colimit.ι (F ⋙ evaluation R X ⋙ ModuleCat.restrictScalars (R.map (𝟙 X))) j ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map (𝟙 X))) (F ⋙ evaluation R X)).inv = colimit.ι (F ⋙ evaluation R X) j ≫ (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ (colimit (F ⋙ evaluation R X))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>restrictionApp (𝟙 X) (F.obj j) ≫ (ModuleCat.restrictScalars (R.map (𝟙 X))).map (colimit.ι (F ⋙ evaluation R X) j) = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ ((F.obj j).obj X)).inv ≫ (ModuleCat.restrictScalars (R.map (𝟙 X))).map (colimit.ι (F ⋙ evaluation R X) j)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X : Cᵒᵖ<VAR>j : J<GOAL>(ModuleCat.restrictScalarsId' (R.map (𝟙 X)) ⋯).inv.app ((F.obj j).obj X) ≫ (ModuleCat.restrictScalars (R.map (𝟙 X))).map (colimit.ι (F ⋙ evaluation R X) j) = (ModuleCat.restrictScalarsId'App (R.map (𝟙 X)) ⋯ ((F.obj j).obj X)).inv ≫ (ModuleCat.restrictScalars (R.map (𝟙 X))).map (colimit.ι (F ⋙ evaluation R X) j)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>colimit.ι (F ⋙ evaluation R X) j ≫ colimMap (whiskerLeft F (restriction R (f ≫ g))) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).inv = colimit.ι (F ⋙ evaluation R X) j ≫ (colimMap (whiskerLeft F (restriction R f)) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv) ≫ (ModuleCat.restrictScalars (R.map f)).map (colimMap (whiskerLeft F (restriction R g)) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp (f ≫ g) (F.obj j) ≫ colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map (f ≫ g))) j ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map (f ≫ g))) (F ⋙ evaluation R Z)).inv = (whiskerLeft F (restriction R f)).app j ≫ colimit.ι (F ⋙ evaluation R Y ⋙ ModuleCat.restrictScalars (R.map f)) j ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map f)) (F ⋙ evaluation R Y)).inv ≫ (ModuleCat.restrictScalars (R.map f)).map (colimMap (whiskerLeft F (restriction R g)) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp (f ≫ g) (F.obj j) ≫ (ModuleCat.restrictScalars (R.map (f ≫ g))).map (colimit.ι (F ⋙ evaluation R Z) j) = (whiskerLeft F (restriction R f)).app j ≫ (ModuleCat.restrictScalars (R.map f)).map (colimit.ι (F ⋙ evaluation R Y) j) ≫ (ModuleCat.restrictScalars (R.map f)).map (colimMap (whiskerLeft F (restriction R g)) ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp (f ≫ g) (F.obj j) ≫ (ModuleCat.restrictScalars (R.map (f ≫ g))).map (colimit.ι (F ⋙ evaluation R Z) j) = (whiskerLeft F (restriction R f)).app j ≫ (ModuleCat.restrictScalars (R.map f)).map ((whiskerLeft F (restriction R g)).app j ≫ colimit.ι (F ⋙ evaluation R Z ⋙ ModuleCat.restrictScalars (R.map g)) j ≫ (preservesColimitIso (ModuleCat.restrictScalars (R.map g)) (F ⋙ evaluation R Z)).inv) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp (f ≫ g) (F.obj j) ≫ (ModuleCat.restrictScalars (R.map (f ≫ g))).map (colimit.ι (F ⋙ evaluation R Z) j) = (whiskerLeft F (restriction R f)).app j ≫ (ModuleCat.restrictScalars (R.map f)).map ((whiskerLeft F (restriction R g)).app j ≫ (ModuleCat.restrictScalars (R.map g)).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv ≫ (ModuleCat.restrictScalars (R.map (f ≫ g))).map (colimit.ι (F ⋙ evaluation R Z) j) = restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j) ≫ (ModuleCat.restrictScalars (R.map g)).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>J : Type u₂<VAR>inst✝² : Category.{v₂, u₂} J<VAR>F : J ⥤ PresheafOfModules R<VAR>inst✝¹ : {X Y : Cᵒᵖ} → (f : X ⟶ Y) → PreservesColimit (F ⋙ evaluation R Y) (ModuleCat.restrictScalars (R.map f))<VAR>inst✝ : ∀ (X : Cᵒᵖ), HasColimit (F ⋙ evaluation R X)<VAR>X Y Z : Cᵒᵖ<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>j : J<GOAL>restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ ((F.obj j).obj Z)).inv ≫ (ModuleCat.restrictScalars (R.map (f ≫ g))).map (colimit.ι (F ⋙ evaluation R Z) j) = restrictionApp f (F.obj j) ≫ (ModuleCat.restrictScalars (R.map f)).map (restrictionApp g (F.obj j)) ≫ (ModuleCat.restrictScalars (R.map f)).map ((ModuleCat.restrictScalars (R.map g)).map (colimit.ι (F ⋙ evaluation R Z) j)) ≫ (ModuleCat.restrictScalarsComp'App (R.map f) (R.map g) (R.map (f ≫ g)) ⋯ (colimit (F ⋙ evaluation R Z))).inv
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>this : ∀ (t : Set A), Algebra.adjoin R (star t) ≤ star (Algebra.adjoin R t)<GOAL>star (Algebra.adjoin R s) ≤ Algebra.adjoin R (star s)
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x✝ : (i : ↑↑s) → β ↑i<VAR>i✝ j i : ι<VAR>x : β i<GOAL>erase j (single i x) = if i = j then 0 else single i x
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝ : HasColimit F<VAR>c : Cocone F<VAR>X : C<VAR>f : c.pt ⟶ X<VAR>j✝ : J<GOAL>ι F j✝ ≫ desc F (c.extend f) = ι F j✝ ≫ desc F c ≫ f
<VAR>J : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} J<VAR>K : Type u₂<VAR>inst✝² : Category.{v₂, u₂} K<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>F✝ F : J ⥤ C<VAR>inst✝ : HasColimit F<VAR>c : Cocone F<VAR>X : C<VAR>f : c.pt ⟶ X<VAR>j✝ : J<GOAL>ι F j✝ ≫ desc F (c.extend f) = (ι F j✝ ≫ desc F c) ≫ f
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<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 u_2<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>b : E × F → G<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>m : ℕ<VAR>x✝ : ↑m ≤ n<GOAL>Differentiable 𝕜 (iteratedFDeriv 𝕜 m fun x => 0)