ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Field K<VAR>L : Type u_7<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsFractionRing A K<VAR>g : A →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : R<VAR>y : ↥(nonZeroDivisors R)<GOAL>mk' K x y = 0 ↔ x = 0
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Field K<VAR>L : Type u_7<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsFractionRing A K<VAR>g : A →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : R<VAR>y : ↥(nonZeroDivisors R)<VAR>hxy : mk' K x y = 0<GOAL>x = 0
<VAR>R : Type u_1<VAR>inst✝¹³ : CommRing R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝¹² : CommRing S<VAR>inst✝¹¹ : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹⁰ : CommRing P<VAR>A : Type u_4<VAR>inst✝⁹ : CommRing A<VAR>inst✝⁸ : IsDomain A<VAR>K : Type u_5<VAR>B : Type u_6<VAR>inst✝⁷ : CommRing B<VAR>inst✝⁶ : IsDomain B<VAR>inst✝⁵ : Field K<VAR>L : Type u_7<VAR>inst✝⁴ : Field L<VAR>inst✝³ : Algebra A K<VAR>inst✝² : IsFractionRing A K<VAR>g : A →+* L<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>x : R<VAR>y : ↥(nonZeroDivisors R)<VAR>hxy : ∃ m, x = 0<GOAL>x = 0
<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>hc : 0 < c<GOAL>a ≤ b / c ↔ c * a ≤ b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>X : Type u_4<VAR>Y : Type u_5<VAR>inst✝ : TopologicalSpace X<VAR>x : X<GOAL>𝓝 (𝓝 x) = ⨅ s, ⨅ (_ : IsOpen s), ⨅ (_ : x ∈ s), 𝓟 (Iic (𝓟 s))
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁵ : NontriviallyNormedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : Module 𝕜 E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>x : E<VAR>hx : x ∈ s<GOAL>#↑s = #E
<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>inst✝ : MeasurableSpace α<VAR>f : α → Prop<VAR>h : MeasurableSet (f ⁻¹' {True})<GOAL>Measurable f
<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>inst✝ : MeasurableSpace α<VAR>f : α → Prop<VAR>h : MeasurableSet (f ⁻¹' {True})<VAR>x : Prop<GOAL>MeasurableSet (f ⁻¹' {x})
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<GOAL>IsGLB (↑s) i ↔ IsLeast (↑s) i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>his : IsGLB (↑s) i<GOAL>IsLeast (↑s) i
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>his : IsGLB (↑s) i<GOAL>i = s.min' hs
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>inst✝ : LinearOrder α<VAR>i : α<VAR>s : Finset α<VAR>hs : s.Nonempty<VAR>his : (∀ x ∈ ↑s, i ≤ x) ∧ ∀ x ∈ lowerBounds ↑s, x ≤ i<GOAL>i = s.min' hs
<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>f : (i : ι) → β i<VAR>s : Multiset ι<VAR>h : ∀ (i : ι), i ∈ s ∨ f i = 0<VAR>i : ι<VAR>H : i ∈ { toFun := f, support' := Trunc.mk ⟨s, h⟩ }.support<GOAL>i ∈ s.toFinset.val.toFinset
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<VAR>x : CliffordAlgebra Q<GOAL>(contractRight ((contractRight x) d)) d = 0
<VAR>R : Type u_1<VAR>inst✝² : CommSemiring R<VAR>k : Type u_2<VAR>l : Type u_3<VAR>m : Type u_4<VAR>n : Type u_5<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>i✝ x✝ : n<GOAL>(mulVecLin 1 ∘ₗ single i✝) 1 x✝ = (LinearMap.id ∘ₗ single i✝) 1 x✝
<VAR>α : Type u_1<VAR>inst✝ : Ring α<VAR>n e1 e2 t1 t2 : α<VAR>h1 : n * e1 = t1<VAR>h2 : n * e2 = t2<GOAL>n * (e1 + e2) = t1 + t2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : ConditionallyCompleteLattice α<VAR>inst✝ : InfConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>hbdd : BddBelow (range f)<GOAL>Tendsto f atTop (𝓝 (⨅ i, f i))
<VAR>R : Type u_1<VAR>n : ℕ<VAR>inst✝² : CommRing R<VAR>a b x y : R<VAR>p : ℕ<VAR>inst✝¹ : IsDomain R<VAR>inst✝ : DecidableRel fun x x_1 => x ∣ x_1<VAR>hp : Prime ↑p<VAR>hp1 : Odd p<VAR>hxy : ↑p ∣ x - y<VAR>hx : ¬↑p ∣ x<GOAL>multiplicity (↑p) (x ^ p - y ^ p) = multiplicity (↑p) (x - y) + 1
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>z : E<VAR>m : Fin 2 → E<GOAL>(iteratedFDeriv 𝕜 2 f z) m = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f✝ f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m✝ n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f : E → F<VAR>z : E<VAR>m : Fin 2 → E<GOAL>(((iteratedFDeriv 𝕜 0 (fun y => fderiv 𝕜 (fun y => fderiv 𝕜 f y) y) z) (init (init m))) (init m (last 0))) (m (last 1)) = ((fderiv 𝕜 (fderiv 𝕜 f) z) (m 0)) (m 1)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<VAR>hts : t ⊆ ↑s<VAR>hst : ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t<GOAL>lowerClosure t ⊔ s.sdiff t = s
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<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>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>⇑(chainTop α β) = ↑(chainTopCoeff α β) • α + ⇑β
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : LieRing L<VAR>inst✝⁸ : LieAlgebra R L<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>inst✝³ : LieAlgebra.IsNilpotent R L<VAR>inst✝² : NoZeroSMulDivisors ℤ R<VAR>inst✝¹ : NoZeroSMulDivisors R M<VAR>inst✝ : IsNoetherian R M<VAR>α : L → R<VAR>β : Weight R L M<VAR>hα : α ≠ 0<GOAL>⇑(chainTop α β) = chainTopCoeff α β • α + ⇑β
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<GOAL>adjoin K ((X ^ ↑n - 1).rootSet L) = ⊤
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<GOAL>adjoin K ((X ^ ↑n - 1).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<GOAL>(X ^ ↑n - 1).rootSet L = {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>x : L<GOAL>x ∈ (X ^ ↑n - 1).rootSet L ↔ x ∈ {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>x : L<GOAL>x ∈ (X ^ ↑n - 1).rootSet L ↔ x ^ ↑n = 1
<VAR>n : ℕ+<VAR>S T : Set ℕ+<VAR>A : Type u<VAR>B : Type v<VAR>K : Type w<VAR>L : Type z<VAR>inst✝⁶ : CommRing A<VAR>inst✝⁵ : CommRing B<VAR>inst✝⁴ : Algebra A B<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {n} K L<VAR>x : L<GOAL>x ^ ↑n = 1 → X ^ ↑n - 1 ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f✝ g : α → β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<GOAL>AEStronglyMeasurable' m (-f) μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f✝ g : α → β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<VAR>x : α<VAR>hx : f x = f' x<GOAL>(-f) x = (-f') x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>𝕜 : Type u_3<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝² : TopologicalSpace β<VAR>f✝ g : α → β<VAR>inst✝¹ : AddGroup β<VAR>inst✝ : TopologicalAddGroup β<VAR>f f' : α → β<VAR>hf'_meas : StronglyMeasurable f'<VAR>hf_ae : f =ᶠ[ae μ] f'<VAR>x : α<VAR>hx : f x = f' x<GOAL>-f x = -f' x
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<GOAL>c = f.cycleOf a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<GOAL>f.cycleOf a = c.cycleOf a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<VAR>hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)<GOAL>f.cycleOf a = c.cycleOf a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<VAR>hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)<VAR>hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc<GOAL>f.cycleOf a = c.cycleOf a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<VAR>hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)<VAR>hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc<GOAL>f.cycleOf a = (c * (f * c⁻¹)).cycleOf a
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : Fintype α<VAR>f✝ f c : Perm α<VAR>a : α<VAR>ha : a ∈ c.support<VAR>hc : c ∈ f.cycleFactorsFinset<VAR>hfc : c.Disjoint (f * c⁻¹) := Disjoint.symm (disjoint_mul_inv_of_mem_cycleFactorsFinset hc)<VAR>hfc2 : Commute c (f * c⁻¹) := Disjoint.commute hfc<GOAL>(f * c⁻¹) a = a
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>S : Set (Submodule R M)<VAR>m : M<GOAL>m ∈ sSup S ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>S : Set (Submodule R M)<VAR>m : M<GOAL>(∃ s, m ∈ ⨆ i ∈ s, ↑i) ↔ ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>S : Set (Submodule R M)<VAR>m : M<VAR>x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i<VAR>s : Finset { a // a ∈ S }<VAR>hs : m ∈ ⨆ i ∈ s, ↑i<GOAL>↑(Finset.map (Function.Embedding.subtype S) s) ⊆ S
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>S : Set (Submodule R M)<VAR>m : M<VAR>x✝ : ∃ s, m ∈ ⨆ i ∈ s, ↑i<VAR>s : Finset { a // a ∈ S }<VAR>hs : m ∈ ⨆ i ∈ s, ↑i<GOAL>m ∈ ⨆ i ∈ Finset.map (Function.Embedding.subtype S) s, i
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid N<VAR>inst✝ : Module R N<VAR>S : Set (Submodule R M)<VAR>m : M<VAR>x✝ : ∃ s, ↑s ⊆ S ∧ m ∈ ⨆ i ∈ s, i<VAR>s : Finset (Submodule R M)<VAR>hsS : ↑s ⊆ S<VAR>hs : m ∈ ⨆ i ∈ s, i<GOAL>m ∈ ⨆ i ∈ s.preimage Subtype.val ⋯, ↑i
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<GOAL>IsAffine X
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<GOAL>IsAffine X
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<GOAL>IsAffine X
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<GOAL>IsIso (ΓSpec.adjunction.unit.app X)
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<VAR>i : ↑s<GOAL>PrimeSpectrum.basicOpen ↑i ∈ ((Scheme.Γ.rightOp ⋙ Scheme.Spec).obj X).affineOpens
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<GOAL>⨆ i, ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i) = ⊤
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<VAR>i : ↑s<GOAL>IsAffine ↑(ΓSpec.adjunction.unit.app X ⁻¹ᵁ ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i))
<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>s : Set ↑Γ(X, ⊤)<VAR>hs : Ideal.span s = ⊤<VAR>hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)<VAR>this✝ : QuasiSeparatedSpace ↑↑X.toPresheafedSpace<VAR>this : CompactSpace ↑↑X.toPresheafedSpace<VAR>i : ↑s<GOAL>IsIso (Scheme.Hom.app (ΓSpec.adjunction.unit.app X ∣_ ↑((fun i => ⟨PrimeSpectrum.basicOpen ↑i, ⋯⟩) i)) ⊤)
<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>f : α → F<VAR>hμν : ν ≪ μ<GOAL>essSup (fun x => ↑‖f x‖₊) ν ≤ essSup (fun x => ↑‖f x‖₊) μ
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>t : Set E<VAR>hst : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>hp : HasFTaylorSeriesUpToOn (↑1) f p t<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>t : Set E<VAR>hst : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>hp : HasFTaylorSeriesUpToOn (↑1) f p t<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : Metric.ball x ε ∩ insert x s ⊆ t<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>t : Set E<VAR>hst : t ∈ 𝓝[insert x s] x<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hε : Metric.ball x ε ∩ insert x s ⊆ t<VAR>hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hp : HasFTaylorSeriesUpToOn 1 f p (Metric.ball x ε ∩ insert x s)<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))<VAR>K : ℝ≥0<VAR>t : Set E<VAR>hst : t ∈ 𝓝[Metric.ball x ε ∩ s] x<VAR>hft : LipschitzOnWith K f t<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>n : ℕ∞<VAR>𝕂 : Type u_1<VAR>inst✝⁸ : RCLike 𝕂<VAR>E' : Type u_2<VAR>inst✝⁷ : NormedAddCommGroup E'<VAR>inst✝⁶ : NormedSpace 𝕂 E'<VAR>F' : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup F'<VAR>inst✝⁴ : NormedSpace 𝕂 F'<VAR>E : Type u_4<VAR>F : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>hf : ContDiffWithinAt ℝ 1 f s x<VAR>hs : Convex ℝ s<VAR>p : E → FormalMultilinearSeries ℝ E F<VAR>ε : ℝ<VAR>ε0 : ε > 0<VAR>hp : HasFTaylorSeriesUpToOn 1 f p (insert x (Metric.ball x ε ∩ s))<VAR>K : ℝ≥0<VAR>t : Set E<VAR>hst : t ∈ 𝓝[s] x<VAR>hft : LipschitzOnWith K f t<GOAL>∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<GOAL>((f fun x_1 => x) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((sᶜ.orderEmbOfFin hl) i)) = (f fun x_1 => x) fun x => y
<VAR>R : Type uR<VAR>S : Type uS<VAR>ι : Type uι<VAR>n✝ : ℕ<VAR>M : Fin n✝.succ → Type v<VAR>M₁ : ι → Type v₁<VAR>M₂ : Type v₂<VAR>M₃ : Type v₃<VAR>M' : Type v'<VAR>inst✝⁶ : CommSemiring R<VAR>inst✝⁵ : (i : Fin n✝.succ) → AddCommMonoid (M i)<VAR>inst✝⁴ : AddCommMonoid M'<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : (i : Fin n✝.succ) → Module R (M i)<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M₂<VAR>ι' : Type u_1<VAR>k l n : ℕ<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>hl : sᶜ.card = l<VAR>f : MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)<VAR>x y : M'<VAR>this : ((curryFinFinset R M₂ M' hk hl).symm f) (s.piecewise (fun x_1 => x) fun x => y) = (f fun x_1 => x) fun x => y<GOAL>((f fun x_1 => x) fun i => s.piecewise (fun x_1 => x) (fun x => y) ((sᶜ.orderEmbOfFin hl) i)) = (f fun x_1 => x) fun x => y