ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>g : G<GOAL>Measure.map ((fun x => f g * x) ∘ ⇑f) μ = Measure.map (⇑f ∘ fun x => g * x) μ
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝⁷ : MeasurableSpace G<VAR>inst✝⁶ : MeasurableSpace H✝<VAR>inst✝⁵ : Mul G<VAR>μ : Measure G<VAR>inst✝⁴ : MeasurableMul G<VAR>H : Type u_4<VAR>inst✝³ : MeasurableSpace H<VAR>inst✝² : Mul H<VAR>inst✝¹ : MeasurableMul H<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>f : G →ₙ* H<VAR>hf : Measurable ⇑f<VAR>h_surj : Surjective ⇑f<VAR>g y : G<GOAL>((fun x => f g * x) ∘ ⇑f) y = (⇑f ∘ fun x => g * x) y
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>p : α → Prop<VAR>f g : Filter α<GOAL>(∃ᶠ (x : α) in f ⊔ g, p x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in g, p x
<VAR>G : Type u_1<VAR>inst✝ : DivInvMonoid G<VAR>a✝ b a : G<GOAL>a ^ 2 = a * a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁴ : AddMonoidWithOne α<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : ZeroLEOneClass α<VAR>inst✝ : CharZero α<VAR>m n : ℕ<GOAL>1 ≤ ↑n ↔ 1 ≤ n
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : W.IsCompatibleWithShift M<VAR>X✝ Y✝ : C<VAR>L : C ⥤ D<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L.CommShift M<VAR>X Y : C<GOAL>(∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔ ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : W.IsCompatibleWithShift M<VAR>X✝ Y✝ : C<VAR>L : C ⥤ D<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L.CommShift M<VAR>X Y : C<VAR>eq : ∀ (a b : M), Small.{w, v₂} ((shiftFunctor C a ⋙ L).obj X ⟶ (shiftFunctor C b ⋙ L).obj Y) ↔ Small.{w, v₂} ((L ⋙ shiftFunctor D a).obj X ⟶ (L ⋙ shiftFunctor D b).obj Y)<GOAL>(∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔ ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
<VAR>C : Type u₁<VAR>inst✝⁷ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v₂, u₂} D<VAR>W : MorphismProperty C<VAR>M : Type w'<VAR>inst✝⁵ : AddMonoid M<VAR>inst✝⁴ : HasShift C M<VAR>inst✝³ : HasShift D M<VAR>inst✝² : W.IsCompatibleWithShift M<VAR>X✝ Y✝ : C<VAR>L : C ⥤ D<VAR>inst✝¹ : L.IsLocalization W<VAR>inst✝ : L.CommShift M<VAR>X Y : C<VAR>eq : ∀ (a b : M), Small.{w, v₂} (L.obj ((shiftFunctor C a).obj X) ⟶ L.obj ((shiftFunctor C b).obj Y)) ↔ Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))<GOAL>(∀ (a b : M), HasSmallLocalizedHom W ((shiftFunctor C a).obj X) ((shiftFunctor C b).obj Y)) ↔ ∀ (a b : M), Small.{w, v₂} ((shiftFunctor D a).obj (L.obj X) ⟶ (shiftFunctor D b).obj (L.obj Y))
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a b : α<VAR>l₁ l₂ : List α<VAR>h : b :: l₁ <+ l₂<GOAL>(l₂.erase a).diff ((b :: l₁).erase a) <+ l₂.diff (b :: l₁)
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CommMonoid M<VAR>f : α → M<VAR>a✝ b : α<VAR>inst✝ : LocallyFiniteOrderTop α<VAR>a : α<GOAL>(∏ x ∈ Ioi a, f x) * f a = ∏ x ∈ Ici a, f x
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : IsEmpty ι<VAR>x : G<GOAL>‖constOfIsEmpty 𝕜 E x‖ = ‖x‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : IsEmpty ι<VAR>x : G<GOAL>‖constOfIsEmpty 𝕜 E x‖ ≤ ‖x‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹⁶ : Fintype ι<VAR>inst✝¹⁵ : Fintype ι'<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>inst✝¹³ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝¹² : (i : ι) → NormedSpace 𝕜 (E i)<VAR>inst✝¹¹ : (i : ι) → SeminormedAddCommGroup (E₁ i)<VAR>inst✝¹⁰ : (i : ι) → NormedSpace 𝕜 (E₁ i)<VAR>inst✝⁹ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁸ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝⁷ : SeminormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>inst✝⁵ : SeminormedAddCommGroup G'<VAR>inst✝⁴ : NormedSpace 𝕜 G'<VAR>c : 𝕜<VAR>f g : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<VAR>𝕜' : Type u_1<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedSpace 𝕜' G<VAR>inst✝¹ : SMulCommClass 𝕜 𝕜' G<VAR>inst✝ : IsEmpty ι<VAR>x : G<GOAL>‖x‖ ≤ ‖constOfIsEmpty 𝕜 E x‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.Regular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<GOAL>(x • μ).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.Regular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>this : (x • μ).OuterRegular<GOAL>(x • μ).Regular
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace α<VAR>μ : Measure α<VAR>inst✝ : μ.Regular<VAR>x : ℝ≥0∞<VAR>hx : x ≠ ⊤<VAR>this✝ : (x • μ).OuterRegular<VAR>this : IsFiniteMeasureOnCompacts (x • μ)<GOAL>(x • μ).Regular
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l : Filter α<VAR>s : Set α<VAR>f : α → Filter β<GOAL>(map f (𝓟 s)).join = ⨆ x ∈ s, f x
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>inst✝ : Group G<VAR>x y : G<VAR>i✝ : ℤ<VAR>hx : IsOfFinOrder x<VAR>x✝ : y ∈ zpowers x<VAR>i : ℤ<VAR>hi : (fun x_1 => x ^ x_1) i = y<GOAL>x ^ (i % ↑(orderOf x)).natAbs = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>hs : Convex 𝕜 s<VAR>x✝ x : E<VAR>hx : x ∈ s<GOAL>1 • x ∈ s
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>I : Submodule R A<VAR>hI : I ≤ 1<GOAL>I ≤ I * (1 / I)
<VAR>ι : Sort uι<VAR>R : Type u<VAR>inst✝² : CommSemiring R<VAR>A : Type v<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>M N : Submodule R A<VAR>m n : A<VAR>I : Submodule R A<VAR>hI : I ≤ 1<GOAL>I * 1 ≤ I * (1 / I)
<VAR>r s : ℤ<VAR>h : IsCoprime r s<GOAL>IsCoprime (r ^ 2 + s ^ 2) (r * s)
<VAR>r s : ℤ<VAR>h : IsCoprime r s<GOAL>IsCoprime (r ^ 2 + s ^ 2) s
<VAR>r s : ℤ<VAR>h : IsCoprime r s<GOAL>IsCoprime (s ^ 2 + r ^ 2) s
<VAR>R : Type u<VAR>inst✝² : Semiring R<VAR>ι : Type v<VAR>dec_ι : DecidableEq ι<VAR>M : Type u_1<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : Module R M<VAR>A✝ A : ι → Submodule R M<VAR>i j : ι<VAR>hij : i ≠ j<VAR>h : Set.univ = {i, j}<VAR>hi : IsInternal A<GOAL>iSup A = A i ⊔ A j
<VAR>o a : Ordinal.{u_1}<VAR>h : a < o * ω<GOAL>∃ i, a < o * ↑i + o
<VAR>o a : Ordinal.{u_1}<VAR>h : a < o * ω<VAR>i : Ordinal.{u_1}<VAR>hi : i < ω<VAR>h' : a < o * i<GOAL>∃ i, a < o * ↑i + o
<VAR>o a : Ordinal.{u_1}<VAR>h : a < o * ω<VAR>i : ℕ<VAR>hi : ↑i < ω<VAR>h' : a < o * ↑i<GOAL>∃ i, a < o * ↑i + o
<VAR>x : SimplexCategory<VAR>e : x ≅ x<GOAL>e = Iso.refl x
<VAR>x : SimplexCategory<VAR>e : x ≅ x<VAR>h : Finset.univ.card = x.len + 1<GOAL>e = Iso.refl x
<VAR>x : SimplexCategory<VAR>e : x ≅ x<VAR>h : Finset.univ.card = x.len + 1<VAR>eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h<GOAL>e = Iso.refl x
<VAR>x : SimplexCategory<VAR>e : x ≅ x<VAR>h : Finset.univ.card = x.len + 1<VAR>eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h<VAR>eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h<GOAL>e = Iso.refl x
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>m n : ZNum<GOAL>↑m = ↑n ↔ m = n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>f₁ =O[l] g₁ ↔ f₂ =O[l] g₂
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>f₁ f₂ : α → E<VAR>g₁ g₂ : α → F<VAR>hf : f₁ =ᶠ[l] f₂<VAR>hg : g₁ =ᶠ[l] g₂<GOAL>(∃ c, IsBigOWith c l f₁ g₁) ↔ ∃ c, IsBigOWith c l f₂ g₂
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type w<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Semiring S<VAR>I J : Ideal R<VAR>x : R<GOAL>(Quotient.mk I) x ∈ map (Quotient.mk I) J ↔ x ∈ J ⊔ I
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedField α<VAR>a b c d : α<VAR>n : ℤ<VAR>hc : c < 0<GOAL>b / c ≤ a ↔ c * a ≤ b
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : Add R<VAR>inst✝⁴ : Mul R<VAR>inst✝³ : Neg R<VAR>inst✝² : One R<VAR>inst✝¹ : Zero R<VAR>inst✝ : CompatibleRing R<VAR>v : α → R<GOAL>Term.realize v 1 = 1
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>eval₂ f g (p ^ 0) = eval₂ f g p ^ 0
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<GOAL>eval₂ f g 1 = 1
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s : σ →₀ ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S₁<VAR>p✝ q : MvPolynomial σ R<VAR>f : R →+* S₁<VAR>g : σ → S₁<VAR>p : MvPolynomial σ R<VAR>n : ℕ<GOAL>eval₂ f g (p ^ (n + 1)) = eval₂ f g p ^ (n + 1)
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>L : Type v<VAR>M : Type w<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>I : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>⁅I, N⁆ = ((toModuleHom R L M).comp (mapIncl I N)).range
<VAR>R : Type u<VAR>inst✝⁶ : CommRing R<VAR>L : Type v<VAR>M : Type w<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>I : LieIdeal R L<VAR>N : LieSubmodule R L M<GOAL>Submodule.span R {m | ∃ x n, ⁅↑x, ↑n⁆ = m} = Submodule.span R (⇑↑(toModuleHom R L M) '' {t | ∃ m n, ↑(incl I) m ⊗ₜ[R] ↑N.incl n = t})
<VAR>m n✝ : ℤ<VAR>n : ℕ<GOAL>Odd ↑n ↔ Odd n
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<VAR>ζ : ℝ<VAR>z0 : ζ > 0<VAR>U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<VAR>ζ : ℝ<VAR>z0 : ζ > 0<VAR>U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}<VAR>xm : ℝ<VAR>hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm<GOAL>∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<VAR>ζ : ℝ<VAR>z0 : ζ > 0<VAR>U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}<VAR>xm : ℝ<VAR>hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm<GOAL>∀ (a : ℕ), 1 ≤ (↑a + 1) ^ f.natDegree
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<VAR>ζ : ℝ<VAR>z0 : ζ > 0<VAR>U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}<VAR>xm : ℝ<VAR>hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm<VAR>y : ℝ<VAR>hy : y ∈ closedBall α ζ<GOAL>dist ((fun y => eval y fR) α) ((fun y => eval y fR) y) ≤ dist α y * |eval xm (derivative fR)|
<VAR>α : ℝ<VAR>ha : Irrational α<VAR>f : ℤ[X]<VAR>f0 : f ≠ 0<VAR>fR : ℝ[X] := map (algebraMap ℤ ℝ) f<VAR>fa : eval α fR = 0<VAR>fR0 : fR ≠ 0<VAR>ar : α ∈ ↑fR.roots.toFinset<VAR>ζ : ℝ<VAR>z0 : ζ > 0<VAR>U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}<VAR>xm : ℝ<VAR>hM : IsMaxOn (fun x => |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm<VAR>z : ℤ<VAR>a : ℕ<VAR>hq : ↑z / (↑a + 1) ∈ closedBall α ζ<GOAL>1 ≤ (↑a + 1) ^ f.natDegree * dist ((fun y => eval y fR) α) ((fun y => eval y fR) (↑z / (↑a + 1)))
<VAR>α : Type u_1<VAR>inst✝ : CommRing α<VAR>n1 n2 k e1 e2 t1 t2 : α<VAR>h1 : n1 * e1 = t1<VAR>h2 : n2 * e2 = t2<VAR>h3 : n1 * n2 = k<GOAL>k * (e1 * e2) = t1 * t2
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).inv = (ρ_ X).hom ≫ (λ_ X).inv
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>(β_ (𝟙_ C) X).hom ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>inst✝¹ : MonoidalCategory C<VAR>inst✝ : BraidedCategory C<VAR>X : C<GOAL>((λ_ X).hom ≫ (ρ_ X).inv) ≫ (ρ_ X).hom ≫ (λ_ X).inv = 𝟙 (𝟙_ C ⊗ X)
<VAR>R : Type u_1<VAR>inst✝¹² : CommSemiring R<VAR>S : Submonoid R<VAR>M : Type u_2<VAR>M' : Type u_3<VAR>M'' : Type u_4<VAR>inst✝¹¹ : AddCommMonoid M<VAR>inst✝¹⁰ : AddCommMonoid M'<VAR>inst✝⁹ : AddCommMonoid M''<VAR>A : Type u_5<VAR>inst✝⁸ : CommSemiring A<VAR>inst✝⁷ : Algebra R A<VAR>inst✝⁶ : Module A M'<VAR>inst✝⁵ : IsLocalization S A<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R M'<VAR>inst✝² : Module R M''<VAR>inst✝¹ : IsScalarTower R A M'<VAR>f : M →ₗ[R] M'<VAR>g : M →ₗ[R] M''<VAR>inst✝ : IsLocalizedModule S f<VAR>m₁ m₂ : M<VAR>s₁ s₂ : ↥S<GOAL>(fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) + (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) = (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>h2L₁ : K₁.carrier * L₁ ⊆ U₁<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>h2L₁ : K₁.carrier * L₁ ⊆ U₁<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>h2L₂ : K₂.carrier * L₂ ⊆ U₂<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>h2L₂ : K₂.carrier * L₂ ⊆ U₂<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂
<VAR>G : Type u_1<VAR>inst✝² : Group G<VAR>inst✝¹ : TopologicalSpace G<VAR>inst✝ : TopologicalGroup G<VAR>K₀ : PositiveCompacts G<VAR>K₁ K₂ : Compacts G<VAR>h : Disjoint K₁.carrier K₂.carrier<VAR>h₂ : IsClosed K₂.carrier<VAR>U₁ U₂ : Set G<VAR>h1U₁ : IsOpen U₁<VAR>h1U₂ : IsOpen U₂<VAR>h2U₁ : K₁.carrier ⊆ U₁<VAR>h2U₂ : K₂.carrier ⊆ U₂<VAR>hU : Disjoint U₁ U₂<VAR>L₁ : Set G<VAR>h1L₁ : L₁ ∈ 𝓝 1<VAR>V₁ : Set G<VAR>h1V₁ : V₁ ⊆ L₁<VAR>h2V₁ : IsOpen V₁<VAR>h3V₁ : 1 ∈ V₁<VAR>h2L₁ : K₁.carrier * V₁ ⊆ U₁<VAR>L₂ : Set G<VAR>h1L₂ : L₂ ∈ 𝓝 1<VAR>V₂ : Set G<VAR>h1V₂ : V₂ ⊆ L₂<VAR>h2V₂ : IsOpen V₂<VAR>h3V₂ : 1 ∈ V₂<VAR>h2L₂ : K₂.carrier * V₂ ⊆ U₂<VAR>eval : (Compacts G → ℝ) → ℝ := fun f => f K₁ + f K₂ - f (K₁ ⊔ K₂)<VAR>this : Continuous eval<GOAL>chaar K₀ (K₁ ⊔ K₂) = chaar K₀ K₁ + chaar K₀ K₂