ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Monoid α<VAR>inst✝⁴ : Monoid β<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : MulEquivClass F α β<VAR>f : F<VAR>a b : α<VAR>n : ℕ<GOAL>f a ^ n ∣ f b ↔ a ^ n ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Monoid α<VAR>inst✝⁴ : Monoid β<VAR>inst✝³ : DecidableRel fun x x_1 => x ∣ x_1<VAR>inst✝² : DecidableRel fun x x_1 => x ∣ x_1<VAR>F : Type u_3<VAR>inst✝¹ : EquivLike F α β<VAR>inst✝ : MulEquivClass F α β<VAR>f : F<VAR>a b : α<VAR>n : ℕ<GOAL>f (a ^ n) ∣ f b ↔ a ^ n ∣ b
<VAR>V : Type u_1<VAR>W : Type u_2<VAR>X : Type u_3<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph W<VAR>u v : V<VAR>x✝² : SimpleGraph V<VAR>x✝¹ x✝ : V<GOAL>((Equiv.refl V).simpleGraph x✝²).Adj x✝¹ x✝ ↔ ((Equiv.refl (SimpleGraph V)) x✝²).Adj x✝¹ x✝
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<GOAL>(countP p) (of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<GOAL>(if p x = (true = true) then 1 else 0) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0
<VAR>α : Type u_1<VAR>p : α → Prop<VAR>inst✝ : DecidablePred p<VAR>x : α<GOAL>(if p x then 1 else 0) = if p x then Multiplicative.ofAdd 1 else 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>a : α<VAR>b : β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s₁ ×ˢ t₁ ∩ s₂ ×ˢ t₂ ↔ (x, y) ∈ (s₁ ∩ s₂) ×ˢ (t₁ ∩ t₂)
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>x y z : ℝ<VAR>n : ℕ<VAR>hx : 0 ≤ x<VAR>hn : n ≠ 0<VAR>hn0 : ↑n ≠ 0<GOAL>(x ^ (↑n)⁻¹) ^ n = x
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R N<VAR>P : RootPairing ι R M N<VAR>i j : ι<VAR>inst✝ : CharZero R<VAR>h : P.root i = 0<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>K : Type u_3<VAR>inst✝ : Field K<VAR>a b c : K<VAR>hc : c ≠ 0<GOAL>b - a / c = (b * c - a) / c
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ⇑f '' ↑I = ↑J<GOAL>map f I = J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ⇑f '' ↑I = ↑J<GOAL>map f I ≤ J
<VAR>R : Type u<VAR>L : Type v<VAR>L' : Type w₂<VAR>M : Type w<VAR>M' : Type w₁<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✝³ : AddCommGroup M'<VAR>inst✝² : Module R M'<VAR>inst✝¹ : LieRingModule L M'<VAR>inst✝ : LieModule R L M'<VAR>f : L →ₗ⁅R⁆ L'<VAR>I I₂ : LieIdeal R L<VAR>J : LieIdeal R L'<VAR>h : ⇑f '' ↑I = ↑J<GOAL>J ≤ map f I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : CoheytingAlgebra α<VAR>a✝ b✝ c a b : α<GOAL>￢a \ b = ￢b \ a
<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>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>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>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>s : Set M<VAR>x : M<GOAL>UniqueMDiffWithinAt I s x ↔ UniqueDiffWithinAt 𝕜 (↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target) (↑(extChartAt I x) x)
<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>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>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>f f₀ f₁ : M → M'<VAR>x✝ : M<VAR>s✝ t : Set M<VAR>g : M' → M''<VAR>u : Set M'<VAR>s : Set M<VAR>x : M<GOAL>𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x = 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ (extChartAt I x).target] ↑(extChartAt I x) x
<VAR>α : Type u_1<VAR>inst✝ : GroupWithZero α<VAR>a b : α<VAR>m n : ℕ<VAR>hab : Commute a b<VAR>hmn : m.Coprime n<GOAL>a ^ m = b ^ n ↔ ∃ c, a = c ^ n ∧ b = c ^ m
<VAR>α : Type u_1<VAR>inst✝ : GroupWithZero α<VAR>a b : α<VAR>m n : ℕ<VAR>hab : Commute a b<VAR>hmn : m.Coprime n<VAR>h : a ^ m = b ^ n<GOAL>∃ c, a = c ^ n ∧ b = c ^ m
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ<VAR>inst✝ : IsProbabilityMeasure μ<VAR>hf : Integrable f μ<VAR>hN : μ N = 0<GOAL>∃ x ∉ N, ∫ (a : α), f a ∂μ ≤ f x
<VAR>C : Type u_1<VAR>ι : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>c : ComplexShape ι<VAR>K L : HomologicalComplex C c<VAR>inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)<VAR>i : ι<GOAL>biprod.inr.f i ≫ biprod.fst.f i = 0
<VAR>R : Type u_1<VAR>R' : Type u_2<VAR>𝕜 : Type u_3<VAR>𝕜₂ : Type u_4<VAR>𝕜₃ : Type u_5<VAR>𝕝 : Type u_6<VAR>E : Type u_7<VAR>E₂ : Type u_8<VAR>E₃ : Type u_9<VAR>F : Type u_10<VAR>G : Type u_11<VAR>ι : Type u_12<VAR>inst✝² : SeminormedRing 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : SMul 𝕜 E<VAR>p✝ : Seminorm 𝕜 E<VAR>x y : E<VAR>r✝ : ℝ<VAR>p : ι → Seminorm 𝕜 E<VAR>s : Finset ι<VAR>H : s.Nonempty<VAR>e : E<VAR>r : ℝ<GOAL>(s.sup' H p).ball e r = s.inf' H fun i => (p i).ball e r
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrderedField α<VAR>a : α<VAR>k : Type u_2<VAR>inst✝ : LinearOrderedField k<VAR>x : k<VAR>hx : 0 < x<GOAL>(fun y => x * y) '' Ioi 0 = Ioi 0
<VAR>α : Type u_1<VAR>s : Set α<GOAL>s.Countable ↔ #↑s < aleph 1
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>h' : M ⊆ K<GOAL>ConnectedComponent.map (induceHom Hom.id ⋯) C = ConnectedComponent.map (induceHom Hom.id ⋯) (ConnectedComponent.map (induceHom Hom.id ⋯) C)
<VAR>V : Type u<VAR>G : SimpleGraph V<VAR>K L L' M : Set V<VAR>C : G.ComponentCompl L<VAR>h : K ⊆ L<VAR>h' : M ⊆ K<GOAL>ConnectedComponent.map (induceHom Hom.id ⋯) C = ConnectedComponent.map (induceHom (Hom.id.comp Hom.id) ⋯) C
<VAR>a✝ b c✝ d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>c : ℝ<VAR>a : ℝ≥0∞<VAR>h : 0 ≤ c<GOAL>(ENNReal.ofReal c * a).toReal = c * a.toReal
<VAR>x y : ℂ<GOAL>cos x - sin x * I = cexp (-x * I)
<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>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>x : G<VAR>i : ℕ<GOAL>‖iteratedFDeriv 𝕜 i (f ∘ ⇑g) x‖ = ‖iteratedFDeriv 𝕜 i f (g x)‖
<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>g : G ≃ₗᵢ[𝕜] E<VAR>f : E → F<VAR>x : G<VAR>i : ℕ<GOAL>‖iteratedFDerivWithin 𝕜 i (f ∘ ⇑g) univ x‖ = ‖iteratedFDerivWithin 𝕜 i f univ (g x)‖
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Ring S<VAR>inst✝ : Algebra R S<VAR>M N : Submodule R S<VAR>ι : Type u_1<VAR>n : Basis ι R ↥N<VAR>H : LinearMap.ker (M.mulRightMap ⇑n) = ⊥<VAR>this : AddCommGroup (ι →₀ ↥M) := Finsupp.instAddCommGroup<GOAL>M.LinearDisjoint N
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>D : Type u'<VAR>inst✝² : Category.{v', u'} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>inst✝ : HasImage f<VAR>w : image.ι f = 0<GOAL>f = 0
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>x : M<VAR>hx : x ∈ S<GOAL>x ∈ S.centralizer.centralizer
<VAR>M : Type u_1<VAR>S T : Set M<VAR>inst✝ : Mul M<VAR>x : M<VAR>hx : x ∈ S<GOAL>∀ (m : M), (∀ m_1 ∈ S, m_1 * m = m * m_1) → m * x = x * m
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<GOAL>(LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<GOAL>(LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<GOAL>(LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<VAR>this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance<VAR>f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯<VAR>e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f<GOAL>(LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<VAR>this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance<VAR>f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯<VAR>e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f<VAR>hf : Function.Surjective ⇑f<GOAL>(LinearMap.ker (Finsupp.total { x // x ∈ s } M R Subtype.val)).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<VAR>this : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance<VAR>f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯<VAR>e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f<VAR>hf : Function.Surjective ⇑f<GOAL>(LinearMap.ker π).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<VAR>this✝ : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance<VAR>f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯<VAR>e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f<VAR>hf : Function.Surjective ⇑f<VAR>this : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π)<GOAL>(LinearMap.ker π).FG
<VAR>R : Type u_1<VAR>M : Type u_3<VAR>N : Type u_2<VAR>inst✝⁷ : Ring R<VAR>inst✝⁶ : AddCommGroup M<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : AddCommGroup N<VAR>inst✝³ : Module R N<VAR>ι : Sort ?u.161801<VAR>inst✝² : _root_.Finite ι<VAR>inst✝¹ : FinitePresentation R N<VAR>l : M →ₗ[R] N<VAR>hl : Function.Surjective ⇑l<VAR>inst✝ : FinitePresentation R ↥(LinearMap.ker l)<VAR>s : Finset M<VAR>hs : Submodule.span R ↑s = ⊤<VAR>π : ({ x // x ∈ s } →₀ R) →ₗ[R] M := Finsupp.total { x // x ∈ s } M R Subtype.val<VAR>H : Function.Surjective ⇑π<VAR>inst : Finite R ↥(LinearMap.ker (l ∘ₗ π))<VAR>this✝ : AddCommGroup ↥(LinearMap.ker (l ∘ₗ π)) := inferInstance<VAR>f : ↥(LinearMap.ker (l ∘ₗ π)) →ₗ[R] ↥(LinearMap.ker l) := π.restrict ⋯<VAR>e : π ∘ₗ (LinearMap.ker (l ∘ₗ π)).subtype = (LinearMap.ker l).subtype ∘ₗ f<VAR>hf : Function.Surjective ⇑f<VAR>this : LinearMap.ker π ≤ LinearMap.ker (l ∘ₗ π)<GOAL>(Submodule.map (LinearMap.ker (l ∘ₗ π)).subtype (LinearMap.ker f)).FG
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a n : ℕ<VAR>h : a.AtLeastTwo<GOAL>(OfNat.ofNat a).coeff (n + 1) = 0
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a n : ℕ<VAR>h : a.AtLeastTwo<GOAL>(↑a).coeff (n + 1) = 0
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>R : Type u_3<VAR>A : Type u_4<VAR>inst✝⁵ : Semiring A<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>(homogeneousHull 𝒜 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✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>(homogeneousHull 𝒜 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✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<GOAL>{r | ∃ i x, ↑(((decompose 𝒜) ↑x) i) = r} ⊆ ↑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✝⁴ : DecidableEq ι<VAR>inst✝³ : AddMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>h : IsHomogeneous 𝒜 I<VAR>i : ι<VAR>x : ↥I<GOAL>↑(((decompose 𝒜) ↑x) i) ∈ ↑I
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝¹ : Zero M<VAR>a a' : α<VAR>b : M<VAR>inst✝ : Nonempty α<VAR>f : α →₀ M<GOAL>f.support.card ≤ 1 ↔ ∃ a, f = single a (f a)
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>α : Type u_4<VAR>x✝³ : α → α → Prop<VAR>x✝² : IsWellOrder α x✝³<VAR>β : Type u_4<VAR>x✝¹ : β → β → Prop<VAR>x✝ : IsWellOrder β x✝¹<GOAL>type x✝³ * type x✝¹ = 0 ↔ type x✝³ = 0 ∨ type x✝¹ = 0
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>α : Type u_4<VAR>x✝³ : α → α → Prop<VAR>x✝² : IsWellOrder α x✝³<VAR>β : Type u_4<VAR>x✝¹ : β → β → Prop<VAR>x✝ : IsWellOrder β x✝¹<GOAL>IsEmpty (β × α) ↔ IsEmpty α ∨ IsEmpty β
<VAR>α✝ : Type u_1<VAR>β✝ : Type u_2<VAR>γ : Type u_3<VAR>r : α✝ → α✝ → Prop<VAR>s : β✝ → β✝ → Prop<VAR>t : γ → γ → Prop<VAR>a b : Ordinal.{u_4}<VAR>α : Type u_4<VAR>x✝³ : α → α → Prop<VAR>x✝² : IsWellOrder α x✝³<VAR>β : Type u_4<VAR>x✝¹ : β → β → Prop<VAR>x✝ : IsWellOrder β x✝¹<GOAL>IsEmpty (β × α) ↔ IsEmpty β ∨ IsEmpty α
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι), f.comp (LinearMap.single i).toAffineMap = g.comp (LinearMap.single i).toAffineMap<GOAL>f = g
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁵ : Ring k<VAR>inst✝¹⁴ : AddCommGroup V1<VAR>inst✝¹³ : AffineSpace V1 P1<VAR>inst✝¹² : AddCommGroup V2<VAR>inst✝¹¹ : AffineSpace V2 P2<VAR>inst✝¹⁰ : AddCommGroup V3<VAR>inst✝⁹ : AffineSpace V3 P3<VAR>inst✝⁸ : Module k V1<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁵ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝⁴ : (i : ι) → Module k (φv i)<VAR>inst✝³ : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝² : Finite ι<VAR>inst✝¹ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>inst✝ : Nonempty ι<VAR>h : ∀ (i : ι), f.comp (LinearMap.single i).toAffineMap = g.comp (LinearMap.single i).toAffineMap<VAR>i : ι<VAR>x : φv i<GOAL>f (Pi.single i x) = g (Pi.single i x)
<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>n : ℕ<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>(iteratedFDerivWithin 𝕜 (n + 1) (fun x => c) s x) m = 0 m
<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>n : ℕ<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>((iteratedFDerivWithin 𝕜 n (fun y => fderivWithin 𝕜 (fun x => c) s y) s x) (init m)) (m (last n)) = 0 m
<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>n : ℕ<VAR>c : F<VAR>hs : UniqueDiffOn 𝕜 s<VAR>hx : x ∈ s<VAR>m : Fin (n + 1) → E<GOAL>((iteratedFDerivWithin 𝕜 n (fun y => 0) s x) (init m)) (m (last n)) = 0 m