ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : Module.IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>x y : M<VAR>k : ℕ<VAR>hM' : Module.IsTorsionBy R M (p ^ Submodule.pOrder hM y)<VAR>h : p ^ k • x ∈ Submodule.span R {y}<GOAL>∃ a, p ^ k • x = p ^ k • a • y
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>M : Type v<VAR>AddCommGroup M<VAR>Module R M<VAR>p : R<VAR>hp : Irreducible p<VAR>hM : Module.IsTorsion' M ↥(Submonoid.powers p)<VAR>dec : (x : M) → Decidable (x = 0)<VAR>z : M<VAR>hz : Module.IsTorsionBy R M (p ^ Submodule.pOrder hM z)<VAR>k : ℕ<VAR>f : R ⧸ Submodule.span R {p ^ k} →ₗ[R] M ⧸ Submodule.span R {z}<GOAL>∃ x, p ^ k • x = 0 ∧ Submodule.Quotient.mk x = f 1
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : Type (max u v)<VAR>AddCommGroup N<VAR>Module R N<VAR>p : R<VAR>hp : Irreducible p<VAR>hN : Module.IsTorsion' N ↥(Submonoid.powers p)<VAR>h' : Module.Finite R N<GOAL>∃ d k, Nonempty (N ≃ₗ[R] ⨁ (i : Fin d), R ⧸ Submodule.span R {p ^ k i})
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : Type (max u v)<VAR>AddCommGroup N<VAR>Module R N<VAR>h' : Module.Finite R N<VAR>hN : Module.IsTorsion R N<GOAL>∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] ⨁ (i : ι), R ⧸ Submodule.span R {p i ^ e i})
<VAR>R : Type u<VAR>CommRing R<VAR>IsDomain R<VAR>IsPrincipalIdealRing R<VAR>N : Type (max u v)<VAR>AddCommGroup N<VAR>Module R N<VAR>h' : Module.Finite R N<GOAL>∃ n ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (N ≃ₗ[R] (Fin n →₀ R) × ⨁ (i : ι), R ⧸ Submodule.span R {p i ^ e i})
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ * B₁ = B₁ * A₀
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₁ * B₁ = B₁ * A₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>star B₀ = B₀
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>star A₀ = A₀
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>B₁ ^ 2 = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ * B₀ = B₀ * A₀
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₁ ^ 2 = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ ^ 2 = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>star A₁ = A₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>star B₁ = B₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₁ * B₀ = B₀ * A₁
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>A₀ A₁ B₀ B₁ : R<VAR>self : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>B₀ ^ 2 = 1
<VAR>R : Type u<VAR>CommRing R<VAR>A₀ A₁ B₀ B₁ : R<VAR>A₀_inv : A₀ ^ 2 = 1<VAR>A₁_inv : A₁ ^ 2 = 1<VAR>B₀_inv : B₀ ^ 2 = 1<VAR>B₁_inv : B₁ ^ 2 = 1<GOAL>(2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁) = 4 * (2 - A₀ * B₀ - A₀ * B₁ - A₁ * B₀ + A₁ * B₁)
<VAR>R : Type u<VAR>OrderedCommRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>Algebra ℝ R<VAR>OrderedSMul ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ 2
<GOAL>√2 * √2 ^ 3 = √2 * (2 * (√2)⁻¹ + 4 * ((√2)⁻¹ * 2⁻¹))
<GOAL>(√2)⁻¹ * (√2)⁻¹ = 2⁻¹
<VAR>R : Type u<VAR>OrderedRing R<VAR>StarRing R<VAR>StarOrderedRing R<VAR>Algebra ℝ R<VAR>OrderedSMul ℝ R<VAR>StarModule ℝ R<VAR>A₀ A₁ B₀ B₁ : R<VAR>T : IsCHSHTuple A₀ A₁ B₀ B₁<GOAL>A₀ * B₀ + A₀ * B₁ + A₁ * B₀ - A₁ * B₁ ≤ √2 ^ 3 • 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : R<GOAL>U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : R<VAR>hU : U ∈ unitary R<GOAL>star U * U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : R<VAR>hU : U ∈ unitary R<GOAL>U * star U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : R<VAR>hU : U ∈ unitary R<GOAL>star U ∈ unitary R
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : R<GOAL>star U ∈ unitary R ↔ U ∈ unitary R
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>↑(star U) = star ↑U
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>star ↑U * ↑U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>↑U * ↑(star U) = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>star U * U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>U * star U = 1
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>star U = U⁻¹
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<GOAL>star = Inv.inv
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>x : ↥(unitary R)<GOAL>↑(unitary.toUnits x) = ↑x
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>x : ↥(unitary R)<GOAL>↑(unitary.toUnits x)⁻¹ = ↑x⁻¹
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<GOAL>Function.Injective ⇑unitary.toUnits
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>u : R<VAR>hu : IsUnit u<VAR>h_mul : star u * u = 1<GOAL>u ∈ unitary R
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>u : R<VAR>hu : IsUnit u<VAR>h_mul : u * star u = 1<GOAL>u ∈ unitary R
<VAR>R : Type u_1<VAR>Monoid R<VAR>StarMul R<VAR>u : R<VAR>hu : u ∈ unitary R<GOAL>IsStarNormal u
<VAR>F : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Monoid R<VAR>StarMul R<VAR>Monoid S<VAR>StarMul S<VAR>FunLike F R S<VAR>StarHomClass F R S<VAR>MonoidHomClass F R S<VAR>f : F<VAR>r : R<VAR>hr : r ∈ unitary R<GOAL>f r ∈ unitary S
<VAR>F : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Monoid R<VAR>StarMul R<VAR>Monoid S<VAR>StarMul S<VAR>FunLike F R S<VAR>StarHomClass F R S<VAR>MonoidHomClass F R S<VAR>f : F<GOAL>∀ (a : ↥(unitary R)), (unitary.map f) a = Subtype.map ⇑f ⋯ a
<VAR>F : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>Monoid R<VAR>StarMul R<VAR>Monoid S<VAR>StarMul S<VAR>FunLike F R S<VAR>StarHomClass F R S<VAR>MonoidHomClass F R S<VAR>f : F<GOAL>unitary.toUnits.comp (unitary.map f) = (Units.map ↑f).comp unitary.toUnits
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>StarMul R<VAR>U : R<GOAL>U ∈ unitary R ↔ star U * U = 1
<VAR>R : Type u_1<VAR>CommMonoid R<VAR>StarMul R<VAR>U : R<GOAL>U ∈ unitary R ↔ U * star U = 1
<VAR>R : Type u_1<VAR>GroupWithZero R<VAR>StarMul R<VAR>U : ↥(unitary R)<GOAL>↑U⁻¹ = (↑U)⁻¹
<VAR>R : Type u_1<VAR>GroupWithZero R<VAR>StarMul R<VAR>U₁ U₂ : ↥(unitary R)<GOAL>↑(U₁ / U₂) = ↑U₁ / ↑U₂
<VAR>R : Type u_1<VAR>GroupWithZero R<VAR>StarMul R<VAR>U : ↥(unitary R)<VAR>z : ℤ<GOAL>↑(U ^ z) = ↑U ^ z
<VAR>R : Type u_1<VAR>Ring R<VAR>StarRing R<VAR>U : ↥(unitary R)<GOAL>↑(-U) = -↑U
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>StarMul A<VAR>a : A<VAR>u : ↥(unitary A)<GOAL>spectrum R (↑u * a * star ↑u) = spectrum R a
<VAR>R : Type u_2<VAR>A : Type u_3<VAR>CommSemiring R<VAR>Ring A<VAR>Algebra R A<VAR>StarMul A<VAR>a : A<VAR>u : ↥(unitary A)<GOAL>spectrum R (star ↑u * a * ↑u) = spectrum R a
<VAR>R : Type u<VAR>Semiring R<VAR>r : R → R → Prop<VAR>StarRing R<VAR>hr : ∀ (a b : R), r a b → r (star a) (star b)<VAR>a b : R<VAR>h : RingQuot.Rel r a b<GOAL>RingQuot.Rel r (star a) (star b)
<VAR>R : Type u_1<VAR>Semiring R<VAR>r : R → R → Prop<VAR>StarRing R<VAR>hr : ∀ (a b : R), r a b → r (star a) (star b)<GOAL>∀ (x : RingQuot r), RingQuot.star' r hr x = match x with | { toQuot := a } => { toQuot := Quot.map star ⋯ a }
<VAR>R : Type u<VAR>Semiring R<VAR>r : R → R → Prop<VAR>StarRing R<VAR>hr : ∀ (a b : R), r a b → r (star a) (star b)<VAR>a : R<GOAL>RingQuot.star' r hr { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (star a) }
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p : MvPolynomial σ R<GOAL>p.degrees = p.support.sup fun s => Finsupp.toMultiset s
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>a : R<GOAL>((MvPolynomial.monomial s) a).degrees ≤ Finsupp.toMultiset s
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>a : R<VAR>ha : a ≠ 0<GOAL>((MvPolynomial.monomial s) a).degrees = Finsupp.toMultiset s
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>(MvPolynomial.C a).degrees = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<GOAL>(MvPolynomial.X n).degrees ≤ {n}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>n : σ<GOAL>(MvPolynomial.X n).degrees = {n}
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.degrees 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.degrees 1 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<GOAL>(p + q).degrees ≤ p.degrees ⊔ q.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>DecidableEq σ<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(∑ i ∈ s, f i).degrees ≤ s.sup fun i => (f i).degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<GOAL>(p * q).degrees ≤ p.degrees + q.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(∏ i ∈ s, f i).degrees ≤ ∑ i ∈ s, (f i).degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>(p ^ n).degrees ≤ n • p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>i : σ<GOAL>i ∈ p.degrees ↔ ∃ d, MvPolynomial.coeff d p ≠ 0 ∧ i ∈ d.support
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>h : p.degrees.Disjoint q.degrees<GOAL>p.degrees ≤ (p + q).degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>p q : MvPolynomial σ R<VAR>h : p.degrees.Disjoint q.degrees<GOAL>(p + q).degrees = p.degrees ∪ q.degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<GOAL>((MvPolynomial.map f) p).degrees ⊆ p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>f : σ → τ<VAR>φ : MvPolynomial σ R<GOAL>((MvPolynomial.rename f) φ).degrees ⊆ Multiset.map f φ.degrees
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>p : MvPolynomial σ R<VAR>f : R →+* S<VAR>hf : Function.Injective ⇑f<GOAL>((MvPolynomial.map f) p).degrees = p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>f : σ → τ<VAR>h : Function.Injective f<GOAL>((MvPolynomial.rename f) p).degrees = Multiset.map f p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>n : σ<VAR>p : MvPolynomial σ R<GOAL>MvPolynomial.degreeOf n p = Multiset.count n p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<VAR>f : MvPolynomial σ R<GOAL>MvPolynomial.degreeOf n f = f.support.sup fun m => m n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<VAR>f : MvPolynomial σ R<VAR>d : ℕ<VAR>h : 0 < d<GOAL>MvPolynomial.degreeOf n f < d ↔ ∀ m ∈ f.support, m n < d
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<VAR>f : MvPolynomial σ R<VAR>d : ℕ<GOAL>MvPolynomial.degreeOf n f ≤ d ↔ ∀ m ∈ f.support, m n ≤ d
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<GOAL>MvPolynomial.degreeOf n 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : R<VAR>x : σ<GOAL>MvPolynomial.degreeOf x (MvPolynomial.C a) = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>DecidableEq σ<VAR>i j : σ<VAR>Nontrivial R<GOAL>MvPolynomial.degreeOf i (MvPolynomial.X j) = if i = j then 1 else 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>n : σ<VAR>f g : MvPolynomial σ R<GOAL>MvPolynomial.degreeOf n (f + g) ≤ max (MvPolynomial.degreeOf n f) (MvPolynomial.degreeOf n g)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<VAR>f : MvPolynomial σ R<VAR>m : σ →₀ ℕ<VAR>h_m : m ∈ f.support<GOAL>m i ≤ MvPolynomial.degreeOf i f
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i : σ<VAR>f g : MvPolynomial σ R<GOAL>MvPolynomial.degreeOf i (f * g) ≤ MvPolynomial.degreeOf i f + MvPolynomial.degreeOf i g
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>i j : σ<VAR>f : MvPolynomial σ R<VAR>h : i ≠ j<GOAL>MvPolynomial.degreeOf i (f * MvPolynomial.X j) = MvPolynomial.degreeOf i f
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>j : σ<VAR>f : MvPolynomial σ R<GOAL>MvPolynomial.degreeOf j (f * MvPolynomial.X j) ≤ MvPolynomial.degreeOf j f + 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>MvPolynomial.degreeOf i (MvPolynomial.C c * p) ≤ MvPolynomial.degreeOf i p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>i : σ<VAR>c : R<GOAL>MvPolynomial.degreeOf i (p * MvPolynomial.C c) ≤ MvPolynomial.degreeOf i p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>f : σ → τ<VAR>h : Function.Injective f<VAR>i : σ<GOAL>MvPolynomial.degreeOf (f i) ((MvPolynomial.rename f) p) = MvPolynomial.degreeOf i p
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree = p.support.sup fun m => Multiset.card (Finsupp.toMultiset m)
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<VAR>s : σ →₀ ℕ<VAR>h : s ∈ p.support<GOAL>(s.sum fun x e => e) ≤ p.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p : MvPolynomial σ R<GOAL>p.totalDegree ≤ Multiset.card p.degrees
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>h : p.support ⊆ q.support<GOAL>p.totalDegree ≤ q.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : R<GOAL>(MvPolynomial.C a).totalDegree = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.totalDegree 0 = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<GOAL>MvPolynomial.totalDegree 1 = 0
<VAR>σ : Type u_1<VAR>R : Type u_3<VAR>CommSemiring R<VAR>Nontrivial R<VAR>s : σ<GOAL>(MvPolynomial.X s).totalDegree = 1
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a b : MvPolynomial σ R<GOAL>(a + b).totalDegree ≤ max a.totalDegree b.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>h : q.totalDegree < p.totalDegree<GOAL>(p + q).totalDegree = p.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>p q : MvPolynomial σ R<VAR>h : q.totalDegree < p.totalDegree<GOAL>(q + p).totalDegree = p.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a b : MvPolynomial σ R<GOAL>(a * b).totalDegree ≤ a.totalDegree + b.totalDegree
<VAR>R : Type u<VAR>S : Type v<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>CommSemiring S<VAR>DistribMulAction R S<VAR>a : R<VAR>f : MvPolynomial σ S<GOAL>(a • f).totalDegree ≤ f.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>a : MvPolynomial σ R<VAR>n : ℕ<GOAL>(a ^ n).totalDegree ≤ n * a.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>c : R<VAR>hc : c ≠ 0<GOAL>((MvPolynomial.monomial s) c).totalDegree = s.sum fun x e => e
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : σ →₀ ℕ<VAR>c : R<GOAL>((MvPolynomial.monomial s) c).totalDegree ≤ s.sum fun x => id
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Nontrivial R<VAR>s : σ<VAR>n : ℕ<GOAL>(MvPolynomial.X s ^ n).totalDegree = n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : List (MvPolynomial σ R)<GOAL>s.prod.totalDegree ≤ (List.map MvPolynomial.totalDegree s).sum
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>s : Multiset (MvPolynomial σ R)<GOAL>s.prod.totalDegree ≤ (Multiset.map MvPolynomial.totalDegree s).sum
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<GOAL>(s.sum f).totalDegree ≤ s.sup fun i => (f i).totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>ι : Type u_3<VAR>s : Finset ι<VAR>f : ι → MvPolynomial σ R<VAR>d : ℕ<VAR>hf : ∀ i ∈ s, (f i).totalDegree ≤ d<GOAL>(s.sum f).totalDegree ≤ d
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : MvPolynomial σ R<VAR>i : σ<GOAL>MvPolynomial.degreeOf i f ≤ f.totalDegree
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>Fintype σ<VAR>f : MvPolynomial σ R<VAR>n : ℕ<VAR>h : f.totalDegree < n * Fintype.card σ<VAR>d : σ →₀ ℕ<VAR>hd : d ∈ f.support<GOAL>∃ i, d i < n
<VAR>R : Type u<VAR>σ : Type u_1<VAR>CommSemiring R<VAR>f : MvPolynomial σ R<VAR>d : σ →₀ ℕ<VAR>h : f.totalDegree < ∑ i ∈ d.support, d i<GOAL>MvPolynomial.coeff d f = 0
<VAR>R : Type u<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>CommSemiring R<VAR>f : σ → τ<VAR>p : MvPolynomial σ R<GOAL>((MvPolynomial.rename f) p).totalDegree ≤ p.totalDegree
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>self : A →⋆ₙ+* B<VAR>a : A<GOAL>self.toFun (star a) = star (self.toFun a)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>F : Type u_5<VAR>FunLike F A B<VAR>NonUnitalRingHomClass F A B<VAR>NonUnitalStarRingHomClass F A B<VAR>f : F<GOAL>⇑↑f = ⇑f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<GOAL>⇑f.toNonUnitalRingHom = ⇑f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f g : A →⋆ₙ+* B<VAR>h : ∀ (x : A), f x = g x<GOAL>f = g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>⇑(f.copy f' h) = f'
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<VAR>f' : A → B<VAR>h : f' = ⇑f<GOAL>f.copy f' h = f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →ₙ+* B<VAR>h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)<GOAL>⇑{ toNonUnitalRingHom := f, map_star' := h } = ⇑f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<VAR>h₁ : ∀ (x y : A), f (x * y) = f x * f y<VAR>h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0<VAR>h₃ : ∀ (x y : A), { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) = { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y<VAR>h₄ : ∀ (a : A), { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) = star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)<GOAL>{ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f
<VAR>A : Type u_1<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<GOAL>⇑(NonUnitalStarRingHom.id A) = id
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Star C<VAR>f : B →⋆ₙ+* C<VAR>g : A →⋆ₙ+* B<GOAL>⇑(f.comp g) = ⇑f ∘ ⇑g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Star C<VAR>f : B →⋆ₙ+* C<VAR>g : A →⋆ₙ+* B<VAR>a : A<GOAL>(f.comp g) a = f (g a)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>C : Type u_3<VAR>D : Type u_4<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>NonUnitalNonAssocSemiring C<VAR>Star C<VAR>NonUnitalNonAssocSemiring D<VAR>Star D<VAR>f : C →⋆ₙ+* D<VAR>g : B →⋆ₙ+* C<VAR>h : A →⋆ₙ+* B<GOAL>(f.comp g).comp h = f.comp (g.comp h)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<GOAL>(NonUnitalStarRingHom.id B).comp f = f
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>NonUnitalNonAssocSemiring B<VAR>Star B<VAR>f : A →⋆ₙ+* B<GOAL>f.comp (NonUnitalStarRingHom.id A) = f
<VAR>A : Type u_1<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<GOAL>⇑1 = id
<VAR>A : Type u_1<VAR>NonUnitalNonAssocSemiring A<VAR>Star A<VAR>a : A<GOAL>1 a = a
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>StarAddMonoid B<GOAL>⇑0 = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>NonUnitalNonAssocSemiring A<VAR>StarAddMonoid A<VAR>NonUnitalNonAssocSemiring B<VAR>StarAddMonoid B<VAR>a : A<GOAL>0 a = 0
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>self : A ≃⋆+* B<VAR>a : A<GOAL>self.toFun (star a) = star (self.toFun a)
<VAR>F : Type u_1<VAR>A : outParam (Type u_2)<VAR>B : outParam (Type u_3)<VAR>Add A<VAR>Mul A<VAR>Star A<VAR>Add B<VAR>Mul B<VAR>Star B<VAR>EquivLike F A B<VAR>self : StarRingEquivClass F A B<VAR>f : F<VAR>a : A<GOAL>f (star a) = star (f a)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<GOAL>e.toRingEquiv = ↑e
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>f g : A ≃⋆+* B<VAR>h : ∀ (a : A), f a = g a<GOAL>f = g
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>f g : A ≃⋆+* B<GOAL>f = g ↔ ∀ (a : A), f a = g a
<VAR>A : Type u_1<VAR>Add A<VAR>Mul A<VAR>Star A<GOAL>⇑StarRingEquiv.refl = id
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<GOAL>EquivLike.inv e = ⇑e.symm
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<GOAL>e.symm.symm = e
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<GOAL>Function.Bijective StarRingEquiv.symm
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃+* B<VAR>h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)<GOAL>⇑{ toRingEquiv := e, map_star' := h₁ } = ⇑e
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>Add A<VAR>Add B<VAR>Mul A<VAR>Mul B<VAR>Star A<VAR>Star B<VAR>e : A ≃⋆+* B<VAR>e' : B → A<VAR>h₁ : Function.LeftInverse e' ⇑e<VAR>h₂ : Function.RightInverse e' ⇑e<VAR>h₃ : ∀ (x y : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₄ : ∀ (x y : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y<VAR>h₅ : ∀ (a : A), { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun (star a) = star ({ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.toFun a)<GOAL>{ toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄, map_star' := h₅ } = e