ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : Preadditive C<VAR>G : C<VAR>hG : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = 0) → f = 0<VAR>X Y : C<VAR>f g : X ⟶ Y<VAR>hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h<GOAL>∀ (h : Y ⟶ G), (f - g) ≫ h = 0
<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>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f : M →ₗ[R] N<VAR>a : AdicCauchySequence I M<VAR>m n : ℕ<VAR>hmn : m ≤ n<GOAL>(fun n => f (↑a n)) m ≡ (fun n => f (↑a n)) n [SMOD I ^ m • ⊤]
<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>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f : M →ₗ[R] N<VAR>a : AdicCauchySequence I M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hm : Submodule.map f (I ^ m • ⊤) ≤ I ^ m • ⊤<GOAL>(fun n => f (↑a n)) m ≡ (fun n => f (↑a n)) n [SMOD I ^ m • ⊤]
<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>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f : M →ₗ[R] N<VAR>a : AdicCauchySequence I M<VAR>m n : ℕ<VAR>hmn : m ≤ n<VAR>hm : Submodule.map f (I ^ m • ⊤) ≤ I ^ m • ⊤<GOAL>(fun n => f (↑a n)) m ≡ (fun n => f (↑a n)) n [SMOD Submodule.map f (I ^ m • ⊤)]
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α✝<VAR>p : α✝ → Prop<VAR>inst✝³ : DecidablePred p<VAR>α : Type u_3<VAR>s : Set α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<GOAL>s.Finite ↔ BddBelow s ∧ BddAbove s
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α✝<VAR>p : α✝ → Prop<VAR>inst✝³ : DecidablePred p<VAR>α : Type u_3<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<GOAL>∅.Finite ↔ BddBelow ∅ ∧ BddAbove ∅
<VAR>α✝ : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : Preorder α✝<VAR>p : α✝ → Prop<VAR>inst✝³ : DecidablePred p<VAR>α : Type u_3<VAR>s : Set α<VAR>inst✝² : Nonempty α<VAR>inst✝¹ : Lattice α<VAR>inst✝ : LocallyFiniteOrder α<VAR>hs : s.Nonempty<GOAL>s.Finite ↔ BddBelow s ∧ BddAbove s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : DivisionMonoid α<VAR>a b c d : α<VAR>h : b * a = 1<GOAL>b = 1 / a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>inst✝² : CommRing A<VAR>inst✝¹ : CommRing B<VAR>inst✝ : CommRing C<VAR>f : A →+* B<VAR>g : B →+* C<VAR>hf : f.FiniteType<VAR>hg : Surjective ⇑g<VAR>x✝¹ : Algebra A B := f.toAlgebra<VAR>x✝ : Algebra A C := (g.comp f).toAlgebra<GOAL>(g.comp f).FiniteType
<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>G H : C<VAR>inst✝ : HasBinaryCoproduct G H<GOAL>IsSeparator (G ⨿ H) ↔ IsSeparating {G, H}
<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>G H : C<VAR>inst✝ : HasBinaryCoproduct G H<VAR>h : IsSeparator (G ⨿ H)<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ G_1 ∈ {G, H}, ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v<GOAL>u = v
<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>G H : C<VAR>inst✝ : HasBinaryCoproduct G H<VAR>h : IsSeparating {G, H}<VAR>X Y : C<VAR>u v : X ⟶ Y<VAR>huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v<VAR>Z : C<VAR>hZ : Z ∈ {G, H}<VAR>g : Z ⟶ X<GOAL>g ≫ u = g ≫ v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>↑‖⟪x, x⟫_𝕜‖ = ⟪x, x⟫_𝕜
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : E<GOAL>↑(re ⟪x, x⟫_𝕜) = ⟪x, x⟫_𝕜
<VAR>d x y : ℤ<GOAL>IsPell { re := x, im := y } ↔ { re := x, im := y } ∈ unitary (ℤ√d)
<VAR>f : ℕ → ℂ<VAR>m : ℝ<VAR>h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>LSeriesSummable f s
<VAR>f : ℕ → ℂ<VAR>m : ℝ<VAR>h : ∀ (n : ℕ), n ≠ 0 → Complex.abs (f n) ≤ m<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>‖f n‖ ≤ m * ↑n ^ (1 - 1)
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<GOAL>∀ᶠ (z : E) in 𝓝[s \ {x}] x, f z ≠ f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<GOAL>∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<VAR>A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)<GOAL>∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
<VAR>𝕜 : Type u_1<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<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>G : Type u_4<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>inst✝¹ : NormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f f₀ f₁ g : E → F<VAR>f' f₀' f₁' g' e : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>L L₁ L₂ : Filter E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hf' : ∃ C, ∀ (z : E), ‖z‖ ≤ C * ‖f' z‖<VAR>A : (fun z => z - x) =O[𝓝[s] x] fun z => f' (z - x)<VAR>this : (fun z => f z - f x) ~[𝓝[s] x] fun z => f' (z - x)<GOAL>∀ᶠ (x_1 : E) in 𝓝 x ⊓ 𝓟 s, x_1 ∈ {x}ᶜ → f x_1 ≠ f x
<VAR>l : Type u_1<VAR>m : Type u_2<VAR>n : Type u_3<VAR>o : Type u_4<VAR>m' : o → Type u_5<VAR>n' : o → Type u_6<VAR>R : Type u_7<VAR>S : Type u_8<VAR>α : Type v<VAR>β : Type w<VAR>γ : Type u_9<VAR>inst✝⁵ : AddCommMonoid α<VAR>inst✝⁴ : Mul α<VAR>inst✝³ : Fintype n<VAR>inst✝² : Monoid R<VAR>inst✝¹ : DistribMulAction R α<VAR>inst✝ : SMulCommClass R α α<VAR>M : Matrix m n α<VAR>a : R<VAR>N : Matrix n l α<VAR>i✝ : m<VAR>j✝ : l<GOAL>(M * a • N) i✝ j✝ = (a • (M * N)) i✝ j✝
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : Semiring R<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Zero N<VAR>inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)<VAR>f : (i : ι) × η i →₀ N<VAR>a✝ : ι<GOAL>a✝ ∈ (sigmaFinsuppEquivDFinsupp f).support ↔ a✝ ∈ f.splitSupport
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝³ : Semiring R<VAR>inst✝² : DecidableEq ι<VAR>inst✝¹ : Zero N<VAR>inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)<VAR>f : (i : ι) × η i →₀ N<VAR>a✝ : ι<GOAL>(sigmaFinsuppEquivDFinsupp f) a✝ ≠ 0 ↔ a✝ ∈ f.splitSupport
<VAR>R : Type u<VAR>a✝ b : R<VAR>m n : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>a : R<VAR>ha : a ≠ 0<VAR>i j : ℕ<GOAL>(monomial i) a = (monomial j) a ↔ i = j
<VAR>C : Type u_4<VAR>D : Type u_2<VAR>inst✝⁵ : Category.{u_5, u_4} C<VAR>inst✝⁴ : Category.{u_1, u_2} D<VAR>F : C ⥤ D<VAR>A : Type u_3<VAR>inst✝³ : AddMonoid A<VAR>inst✝² : HasShift C A<VAR>s : A → D ⥤ D<VAR>i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F<VAR>inst✝¹ : ((whiskeringLeft C D D).obj F).Full<VAR>inst✝ : ((whiskeringLeft C D D).obj F).Faithful<VAR>X : C<VAR>this : HasShift D A := HasShift.induced F A s i<GOAL>(shiftFunctorZero D A).hom.app (F.obj X) = (i 0).hom.app X ≫ F.map ((shiftFunctorZero C A).hom.app X)
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>eval x (basisDivisor x y) = 1
<VAR>F : Type u_1<VAR>inst✝ : Field F<VAR>x y : F<VAR>hxy : x ≠ y<GOAL>(x - y)⁻¹ * (x - y) = 1
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<VAR>hx : ¬x = 0<GOAL>(x + y).intDegree ≤ max x.intDegree y.intDegree
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hy : y ≠ 0<VAR>hxy : x + y ≠ 0<VAR>hx : ¬x = 0<GOAL>(x.num * y.denom + x.denom * y.num).natDegree ≤ max (x.num * y.denom).natDegree (x.denom * y.num).natDegree
<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>n : ℕ<VAR>hf : DifferentiableOn 𝕜 f s<VAR>h : ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s<VAR>x : E<VAR>hx : x ∈ s<GOAL>ContDiffWithinAt 𝕜 (↑(n + 1)) f s x
<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>n : ℕ<VAR>hf : DifferentiableOn 𝕜 f s<VAR>h : ContDiffOn 𝕜 (↑n) (fun y => fderivWithin 𝕜 f s y) s<VAR>x : E<VAR>hx : x ∈ s<GOAL>∃ u ∈ 𝓝[s] x, ∃ f', (∀ x ∈ u, HasFDerivWithinAt f (f' x) u x) ∧ ContDiffWithinAt 𝕜 (↑n) f' u x
<VAR>q : ℍ<GOAL>‖exp ℝ q‖ = ‖exp ℝ q.re‖
<VAR>a n : ℕ<VAR>a0 : a ≠ 0<GOAL>addOrderOf ↑a = n / n.gcd a
<VAR>α : Type u_1<VAR>inst✝ : BEq α<VAR>l : List α<GOAL>[] ∪ l = l
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>p : ι → Prop<VAR>s : ι → Set α<VAR>𝓕 : Filter ι<VAR>a : α<GOAL>a ∈ limsup s 𝓕 ↔ ∃ᶠ (i : ι) in 𝓕, a ∈ s i
<VAR>o : Ordinal.{u_1}<VAR>H : ∀ (n : ℕ), ↑n ≤ o<VAR>a : Ordinal.{u_1}<VAR>h : a < ω<GOAL>a < o
<VAR>o : Ordinal.{u_1}<VAR>H : ∀ (n : ℕ), ↑n ≤ o<VAR>a : Ordinal.{u_1}<VAR>h : a < ω<VAR>n : ℕ<VAR>e : a = ↑n<GOAL>a < o
<VAR>o : Ordinal.{u_1}<VAR>H : ∀ (n : ℕ), ↑n ≤ o<VAR>a : Ordinal.{u_1}<VAR>h : a < ω<VAR>n : ℕ<VAR>e : a = ↑n<GOAL>succ ↑n ≤ o
<VAR>R : Type u<VAR>S✝ : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<GOAL>ϕ p = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p
<VAR>R : Type u<VAR>S✝ : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<VAR>val✝ : Fintype σ<GOAL>ϕ p = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p
<VAR>R : Type u<VAR>S✝ : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<VAR>val✝ : Fintype σ<GOAL>ϕ (∑ v ∈ p.support, (monomial v) (coeff v p)) = eval₂ (ϕ.comp C) (fun s => ϕ (X s)) p
<VAR>R : Type u<VAR>S✝ : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<VAR>val✝ : Fintype σ<GOAL>∑ x ∈ p.support, ϕ ((monomial x) (coeff x p)) = ∑ d ∈ p.support, (ϕ.comp C) (coeff d p) * ∏ i : σ, ϕ (X i) ^ d i
<VAR>R : Type u<VAR>S✝ : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : CommRing S✝<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>S : Type u_2<VAR>inst✝¹ : CommRing S<VAR>inst✝ : Finite σ<VAR>ϕ : MvPolynomial σ R →+* S<VAR>p : MvPolynomial σ R<VAR>val✝ : Fintype σ<VAR>x✝ : σ →₀ ℕ<GOAL>ϕ ((monomial x✝) (coeff x✝ p)) = (ϕ.comp C) (coeff x✝ p) * ∏ i : σ, ϕ (X i) ^ x✝ i
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>inst✝ : HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<VAR>g : X ⟶ widePullback B objs arrows<VAR>h1 : ∀ (j : J), g ≫ π arrows j = fs j<VAR>h2 : g ≫ base arrows = f<GOAL>g = lift f fs w
<VAR>J : Type w<VAR>C✝ : Type u<VAR>inst✝² : Category.{v, u} C✝<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>B : C<VAR>objs : J → C<VAR>arrows : (j : J) → objs j ⟶ B<VAR>inst✝ : HasWidePullback B objs arrows<VAR>X : C<VAR>f : X ⟶ B<VAR>fs : (j : J) → X ⟶ objs j<VAR>w : ∀ (j : J), fs j ≫ arrows j = f<VAR>g : X ⟶ widePullback B objs arrows<VAR>h1 : ∀ (j : J), g ≫ π arrows j = fs j<VAR>h2 : g ≫ base arrows = f<GOAL>∀ (j : WidePullbackShape J), g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app j = (WidePullbackShape.mkCone f fs w).π.app j
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hr : G.Reachable u v<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>u v w : V<VAR>hr : G.Reachable u v<VAR>p : G.Walk u v<VAR>h : p.length = G.dist u v<GOAL>∃ p, p.IsPath ∧ p.length = G.dist u v
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelMonoidWithZero M<VAR>inst✝⁴ : Finite M<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : GCDMonoid R<VAR>inst✝ : Unique Rˣ<VAR>a b c : R<VAR>n : ℕ<VAR>cp : IsCoprime a b<VAR>h : a * b = c ^ n<GOAL>∃ d, a = d ^ n
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelMonoidWithZero M<VAR>inst✝⁴ : Finite M<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : GCDMonoid R<VAR>inst✝ : Unique Rˣ<VAR>a b c : R<VAR>n : ℕ<VAR>cp : IsCoprime a b<VAR>h : a * b = c ^ n<GOAL>GCDMonoid.gcd a b ∣ 1
<VAR>M : Type u_1<VAR>inst✝⁵ : CancelMonoidWithZero M<VAR>inst✝⁴ : Finite M<VAR>R : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : IsDomain R<VAR>inst✝¹ : GCDMonoid R<VAR>inst✝ : Unique Rˣ<VAR>a b c : R<VAR>n : ℕ<VAR>h : a * b = c ^ n<VAR>x y : R<VAR>hxy : x * a + y * b = 1<GOAL>GCDMonoid.gcd a b ∣ x * a + y * b
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>a b : α<GOAL>some '' Icc a b = Icc ↑a ↑b
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>Disjoint t (⋃₀ ↑(hC.diffFinset hs ht))
<VAR>α : Type u_1<VAR>C : Set (Set α)<VAR>s t : Set α<VAR>hC : IsSetSemiring C<VAR>hs : s ∈ C<VAR>ht : t ∈ C<GOAL>Disjoint t (s \ t)
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>π : ι → Type u_4<VAR>inst✝ : GeneralizedHeytingAlgebra α<VAR>a b c d : α<GOAL>⊤ ⇔ a = a
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<GOAL>C x hx
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<GOAL>∃ (x_1 : x ∈ ⨆ i, p i), C x x_1
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝¹ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x✝ : M<VAR>hx✝ : x✝ ∈ ⨆ i, p i<VAR>i : ι<VAR>x : M<VAR>hx : x ∈ p i<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x : M<VAR>hx : x ∈ ⨆ i, p i<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) 0
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝¹ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>p : ι → Submodule R M<VAR>C : (x : M) → x ∈ ⨆ i, p i → Prop<VAR>mem : ∀ (i : ι) (x : M) (hx : x ∈ p i), C x ⋯<VAR>zero : C 0 ⋯<VAR>add : ∀ (x y : M) (hx : x ∈ ⨆ i, p i) (hy : y ∈ ⨆ i, p i), C x hx → C y hy → C (x + y) ⋯<VAR>x✝ : M<VAR>hx : x✝ ∈ ⨆ i, p i<VAR>x y : M<GOAL>(fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) x → (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) y → (fun x => ∃ (hx : x ∈ ⨆ i, p i), C x hx) (x + y)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>f : α → β<VAR>s t : Set α<VAR>a✝ : α<VAR>Hf : MonotoneOn f t<VAR>Hst : s ⊆ t<VAR>a : α<VAR>ha : a ∈ upperBounds s ∩ t<GOAL>f a ∈ upperBounds (f '' s)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Ring B<VAR>inst✝¹ : TopologicalRing B<VAR>inst✝ : Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>comap f s.topologicalClosure = (comap f s).topologicalClosure
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Ring B<VAR>inst✝¹ : TopologicalRing B<VAR>inst✝ : Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>↑(comap f s.topologicalClosure) = ↑(comap f s).topologicalClosure
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Ring B<VAR>inst✝¹ : TopologicalRing B<VAR>inst✝ : Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>↑(comap f s.topologicalClosure) = closure ↑(comap f s)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Ring B<VAR>inst✝¹ : TopologicalRing B<VAR>inst✝ : Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>⇑f ⁻¹' ↑s.topologicalClosure = closure (⇑f ⁻¹' ↑s)
<VAR>R : Type u_1<VAR>inst✝⁸ : CommSemiring R<VAR>A : Type u<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : TopologicalSemiring A<VAR>s : Subalgebra R A<VAR>B : Type u_2<VAR>inst✝³ : TopologicalSpace B<VAR>inst✝² : Ring B<VAR>inst✝¹ : TopologicalRing B<VAR>inst✝ : Algebra R B<VAR>f : B →ₐ[R] A<VAR>f' : B ≃ₜ A<VAR>w : ⇑f = ⇑f'<GOAL>⇑f' ⁻¹' ↑s.topologicalClosure = closure (⇑f' ⁻¹' ↑s)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>v : α →₀ M<VAR>c : R<VAR>h : α → M →ₗ[R] M₂<GOAL>((c • v).sum fun a => ⇑(h a)) = c • v.sum fun a => ⇑(h a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>v : α →₀ M<VAR>c : R<VAR>h : α → M →ₗ[R] M₂<GOAL>(v.sum fun i c_1 => (h i) (c • c_1)) = v.sum fun a b => c • (h a) b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>inst✝⁴ : Semiring R<VAR>inst✝³ : AddCommMonoid M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R M₂<VAR>v : α →₀ M<VAR>c : R<VAR>h : α → M →ₗ[R] M₂<GOAL>∀ (i : α), (h i) 0 = 0
<VAR>p n : ℕ+<VAR>A : Type w<VAR>B : Type z<VAR>K : Type u<VAR>L : Type v<VAR>C : Type w<VAR>inst✝⁵ : CommRing A<VAR>inst✝⁴ : CommRing B<VAR>inst✝³ : Algebra A B<VAR>inst✝² : IsCyclotomicExtension {n} A B<VAR>inst✝¹ : IsDomain B<VAR>inst✝ : NeZero ↑↑n<GOAL>(cyclotomic (↑n) B).IsRoot (zeta n A B)