ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>y : R<VAR>hy : y ∈ ↑N<GOAL>(algebraMap S T) ↑⟨(algebraMap R S) y, ⋯⟩ = (algebraMap R T) ↑⟨y, hy⟩
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>y : T<GOAL>∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>y : T<VAR>x : R<VAR>s : ↥N<VAR>e : y * (algebraMap R T) ↑(x, s).2 = (algebraMap R T) (x, s).1<GOAL>∃ x, y * (algebraMap S T) ↑x.2 = (algebraMap S T) x.1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>y : T<VAR>x : R<VAR>s : ↥N<VAR>e : y * (algebraMap R T) ↑(x, s).2 = (algebraMap R T) (x, s).1<GOAL>y * (algebraMap S T) ↑((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).2 = (algebraMap S T) ((algebraMap R S) x, ⟨(algebraMap R S) ↑s, ⋯⟩).1
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<GOAL>(algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ c, ↑c * x₁ = ↑c * x₂
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑(y₁, s₁).2 = (algebraMap R S) (y₁, s₁).1<GOAL>(algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ c, ↑c * x₁ = ↑c * x₂
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑(y₁, s₁).2 = (algebraMap R S) (y₁, s₁).1<VAR>y₂ : R<VAR>s₂ : ↥M<VAR>e₂ : x₂ * (algebraMap R S) ↑(y₂, s₂).2 = (algebraMap R S) (y₂, s₂).1<GOAL>(algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ c, ↑c * x₁ = ↑c * x₂
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑(y₁, s₁).2 = (algebraMap R S) (y₁, s₁).1<VAR>y₂ : R<VAR>s₂ : ↥M<VAR>e₂ : x₂ * (algebraMap R S) ↑(y₂, s₂).2 = (algebraMap R S) (y₂, s₂).1<GOAL>(algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁<VAR>y₂ : R<VAR>s₂ : ↥M<VAR>e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂<GOAL>(algebraMap S T) x₁ = (algebraMap S T) x₂ → ∃ a, (algebraMap R S) ↑a * x₁ = (algebraMap R S) ↑a * x₂
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁<VAR>y₂ : R<VAR>s₂ : ↥M<VAR>e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂<GOAL>(algebraMap R T) (y₁ * ↑s₂) = (algebraMap R T) (y₂ * ↑s₁) → ∃ a, (algebraMap R S) (↑a * (y₁ * ↑s₂)) = (algebraMap R S) (↑a * (y₂ * ↑s₁))
<VAR>R : Type u_1<VAR>inst✝⁹ : CommSemiring R<VAR>M✝ : Submonoid R<VAR>S : Type u_2<VAR>inst✝⁸ : CommSemiring S<VAR>inst✝⁷ : Algebra R S<VAR>P : Type u_3<VAR>inst✝⁶ : CommSemiring P<VAR>N✝ : Submonoid S<VAR>T : Type u_4<VAR>inst✝⁵ : CommSemiring T<VAR>inst✝⁴ : Algebra R T<VAR>M N : Submonoid R<VAR>h : M ≤ N<VAR>inst✝³ : IsLocalization M S<VAR>inst✝² : IsLocalization N T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>x₁ x₂ : S<VAR>y₁ : R<VAR>s₁ : ↥M<VAR>e₁ : x₁ * (algebraMap R S) ↑s₁ = (algebraMap R S) y₁<VAR>y₂ : R<VAR>s₂ : ↥M<VAR>e₂ : x₂ * (algebraMap R S) ↑s₂ = (algebraMap R S) y₂<GOAL>(∃ c, ↑c * (y₁ * ↑s₂) = ↑c * (y₂ * ↑s₁)) → ∃ a c, ↑c * (↑a * (y₁ * ↑s₂)) = ↑c * (↑a * (y₂ * ↑s₁))
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : x ∈ closure s<VAR>w : F<VAR>c : ℕ → 𝕜<VAR>d : ℕ → F<VAR>hd : ∀ᶠ (n : ℕ) in atTop, y + d n ∈ t<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<GOAL>(LinearMap.inr 𝕜 E F) w ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<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>x y✝ : E<VAR>s t✝ : Set E<VAR>t : Set F<VAR>y : F<VAR>hs : x ∈ closure s<VAR>w : F<VAR>c : ℕ → 𝕜<VAR>d : ℕ → F<VAR>hd : ∀ᶠ (n : ℕ) in atTop, y + d n ∈ t<VAR>hc : Tendsto (fun n => ‖c n‖) atTop atTop<VAR>hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)<VAR>this : ∀ (n : ℕ), ∃ d', x + d' ∈ s ∧ ‖c n • d'‖ < (1 / 2) ^ n<GOAL>(LinearMap.inr 𝕜 E F) w ∈ tangentConeAt 𝕜 (s ×ˢ t) (x, y)
<VAR>α : Type u_1<VAR>inst✝¹ : BEq α<VAR>inst✝ : LawfulBEq α<VAR>a : α<VAR>l₂ : List α<VAR>h : ¬a ∈ l₂<VAR>l₁ : List α<GOAL>(a :: l₁).diff l₂ = a :: l₁.diff l₂
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y z : E<VAR>hf : ConcaveOn 𝕜 [x-[𝕜]y] f<VAR>hz : z ∈ [x-[𝕜]y]<GOAL>min (f x) (f y) ≤ f z
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>ι : Type u_5<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : AddCommGroup E<VAR>inst✝³ : LinearOrderedAddCommGroup β<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>s : Set E<VAR>f : E → β<VAR>t : Finset ι<VAR>w : ι → 𝕜<VAR>p : ι → E<VAR>x y z : E<VAR>hf : ConcaveOn 𝕜 ((convexHull 𝕜) {x, y}) f<VAR>hz : z ∈ (convexHull 𝕜) {x, y}<GOAL>min (f x) (f y) ≤ f z
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hζ' : ζ ∈ primitiveRoots n K<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • α = σ α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>hα : α ^ n = (algebraMap K L) a<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hζ'✝ : ζ ∈ primitiveRoots n K<VAR>hζ' : IsPrimitiveRoot ζ n<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • α = σ α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hα : α ∈ Multiset.map (fun x => (algebraMap K L) ζ ^ x * rootOfSplitsXPowSubC hn a L) (Multiset.range n)<VAR>hζ'✝ : ζ ∈ primitiveRoots n K<VAR>hζ' : IsPrimitiveRoot ζ n<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • α = σ α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>α : L<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hζ'✝ : ζ ∈ primitiveRoots n K<VAR>hζ' : IsPrimitiveRoot ζ n<VAR>hα : ∃ a_1 < n, (algebraMap K L) ζ ^ a_1 * rootOfSplitsXPowSubC hn a L = α<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • α = σ α
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hζ'✝ : ζ ∈ primitiveRoots n K<VAR>hζ' : IsPrimitiveRoot ζ n<VAR>i : ℕ<VAR>left✝ : i < n<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC hn a L) = σ ((algebraMap K L) ζ ^ i * rootOfSplitsXPowSubC hn a L)
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>n : ℕ<VAR>hζ : (primitiveRoots n K).Nonempty<VAR>hn : 0 < n<VAR>a : K<VAR>H : Irreducible (X ^ n - C a)<VAR>L : Type u_1<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsSplittingField K L (X ^ n - C a)<VAR>σ : L ≃ₐ[K] L<VAR>ζ : K<VAR>hζ'✝ : ζ ∈ primitiveRoots n K<VAR>hζ' : IsPrimitiveRoot ζ n<VAR>i : ℕ<VAR>left✝ : i < n<GOAL>(autEquivRootsOfUnity ⋯ hn H L) σ • ζ ^ i • rootOfSplitsXPowSubC hn a L = ζ ^ i • (autEquivRootsOfUnity hζ hn H L) σ • rootOfSplitsXPowSubC hn a L
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>as : AssocList α β<GOAL>as.toList = as.toListTR
<VAR>α : Type u_2<VAR>β : Type u_1<VAR>as : AssocList α β<GOAL>as.toList = (List.foldl (fun d x => d.push (x.fst, x.snd)) #[] as.toList).data
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a b : R[X]<VAR>e : a * p + b * q = 1<VAR>s : R := ↑hr.unit⁻¹<GOAL>IsCoprime (p.scaleRoots r) (q.scaleRoots r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a b : R[X]<VAR>e : a * p + b * q = 1<VAR>s : R := ↑hr.unit⁻¹<VAR>this : (a * p).natDegree = (b * q).natDegree<GOAL>IsCoprime (p.scaleRoots r) (q.scaleRoots r)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a b : R[X]<VAR>e : a * p + b * q = 1<VAR>s : R := ↑hr.unit⁻¹<VAR>this : (a * p).natDegree = (b * q).natDegree<GOAL>∃ b, s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r + b * q.scaleRoots r = 1
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>A : Type u_3<VAR>K : Type u_4<VAR>inst✝³ : Semiring S<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Field K<VAR>p q : R[X]<VAR>r : R<VAR>hr : IsUnit r<VAR>a b : R[X]<VAR>e : a * p + b * q = 1<VAR>s : R := ↑hr.unit⁻¹<VAR>this : (a * p).natDegree = (b * q).natDegree<GOAL>s ^ (a * p).natDegree • s ^ (a.natDegree + p.natDegree - (a * p).natDegree) • a.scaleRoots r * p.scaleRoots r + s ^ (a * p).natDegree • s ^ (b.natDegree + q.natDegree - (b * q).natDegree) • b.scaleRoots r * q.scaleRoots r = 1
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>u : Aˣ<GOAL>spectrum R (↑u * a * ↑u⁻¹) = spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a : A<VAR>u : Aˣ<GOAL>∀ (b : A) (v : Aˣ), spectrum R (↑v * b * ↑v⁻¹) ⊆ spectrum R b
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a✝ : A<VAR>u✝ : Aˣ<VAR>a : A<VAR>u : Aˣ<VAR>μ : R<VAR>hμ : μ ∈ spectrum R (↑u * a * ↑u⁻¹)<GOAL>μ ∈ spectrum R a
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a✝ : A<VAR>u✝ : Aˣ<VAR>a : A<VAR>u : Aˣ<VAR>μ : R<VAR>hμ : ¬IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)<GOAL>¬IsUnit ((algebraMap R A) μ - a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : Ring A<VAR>inst✝ : Algebra R A<VAR>a✝ : A<VAR>u✝ : Aˣ<VAR>a : A<VAR>u : Aˣ<VAR>μ : R<VAR>hμ : IsUnit ((algebraMap R A) μ - a)<GOAL>IsUnit ((algebraMap R A) μ - ↑u * a * ↑u⁻¹)
<VAR>n : ℕ<VAR>inst✝ : Fintype (ZMod n)<GOAL>Fintype.card (ZMod n) = n
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>Disjoint (x \ z) y ↔ Disjoint x (y \ z)
<VAR>ι : Type w<VAR>R : Type u<VAR>M : Type v₁<VAR>N : Type v₂<VAR>P : Type v₃<VAR>Q : Type v₄<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : AddCommMonoid M<VAR>inst✝⁸ : AddCommMonoid N<VAR>inst✝⁷ : AddCommMonoid P<VAR>inst✝⁶ : AddCommMonoid Q<VAR>inst✝⁵ : Module R M<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : Module R P<VAR>inst✝² : Module R Q<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Fintype ι<VAR>b : Basis ι R M<VAR>g : Dual R N<VAR>q : Q<GOAL>prodMap 0 ((dualTensorHom R N Q) (g ⊗ₜ[R] q)) = (dualTensorHom R (M × N) (P × Q)) ((g ∘ₗ snd R M N) ⊗ₜ[R] (inr R P Q) q)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>p : X → Prop<GOAL>IsOpen {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>p : X → Prop<VAR>a : X<VAR>ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}<GOAL>{x | ∀ᶠ (y : X) in 𝓝[≠] x, p y} ∈ 𝓝 a
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>p : X → Prop<VAR>a : X<VAR>ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}<VAR>b : X<VAR>hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x<GOAL>∀ᶠ (y : X) in 𝓝[≠] b, p y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>p : X → Prop<VAR>a : X<VAR>ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}<VAR>hb : ∀ᶠ (x : X) in 𝓝[≠] a, p x<GOAL>∀ᶠ (y : X) in 𝓝[≠] a, p y
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T1Space X<VAR>p : X → Prop<VAR>a : X<VAR>ha : a ∈ {x | ∀ᶠ (y : X) in 𝓝[≠] x, p y}<VAR>b : X<VAR>hb : ∀ᶠ (x : X) in 𝓝[{a}ᶜ] b, p x<VAR>h : a ≠ b<GOAL>∀ᶠ (y : X) in 𝓝[≠] b, p y
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>‖f_nat k a t n‖ ≤ g_nat k a t n
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>(↑n + a) ^ k * rexp (-π * (↑n + a) ^ 2 * t) ≤ g_nat k a t n
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>rexp (-π * (↑n + a) ^ 2 * t) ≤ rexp (-π * (↑n + a ^ 2) * t)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<GOAL>0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<VAR>u : ↑n ≤ ↑n ^ 2<GOAL>0 ≤ (↑n + a) ^ 2 - (↑n + a ^ 2)
<VAR>k : ℕ<VAR>a t : ℝ<VAR>ha : 0 ≤ a<VAR>ht : 0 < t<VAR>n : ℕ<VAR>u : ↑n ≤ ↑n ^ 2<GOAL>(↑n + a) ^ 2 - (↑n + a ^ 2) = ↑n ^ 2 - ↑n + 2 * ↑n * a
<VAR>𝕜✝ : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type v<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace 𝕜✝ E✝<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜✝ F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜✝ F'<VAR>inst✝⁴ : CompleteSpace 𝕜✝<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : LocallyCompactSpace E<GOAL>ProperSpace E
<VAR>𝕜✝ : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type v<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace 𝕜✝ E✝<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜✝ F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜✝ F'<VAR>inst✝⁴ : CompleteSpace 𝕜✝<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : LocallyCompactSpace E<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>hr : IsCompact (closedBall 0 r)<GOAL>ProperSpace E
<VAR>𝕜✝ : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type v<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace 𝕜✝ E✝<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜✝ F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜✝ F'<VAR>inst✝⁴ : CompleteSpace 𝕜✝<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : LocallyCompactSpace E<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>hr : IsCompact (closedBall 0 r)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<GOAL>ProperSpace E
<VAR>𝕜✝ : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type v<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace 𝕜✝ E✝<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜✝ F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜✝ F'<VAR>inst✝⁴ : CompleteSpace 𝕜✝<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : LocallyCompactSpace E<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>hr : IsCompact (closedBall 0 r)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))<GOAL>ProperSpace E
<VAR>𝕜✝ : Type u<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜✝<VAR>E✝ : Type v<VAR>inst✝¹³ : NormedAddCommGroup E✝<VAR>inst✝¹² : NormedSpace 𝕜✝ E✝<VAR>F : Type w<VAR>inst✝¹¹ : NormedAddCommGroup F<VAR>inst✝¹⁰ : NormedSpace 𝕜✝ F<VAR>F' : Type x<VAR>inst✝⁹ : AddCommGroup F'<VAR>inst✝⁸ : Module 𝕜✝ F'<VAR>inst✝⁷ : TopologicalSpace F'<VAR>inst✝⁶ : TopologicalAddGroup F'<VAR>inst✝⁵ : ContinuousSMul 𝕜✝ F'<VAR>inst✝⁴ : CompleteSpace 𝕜✝<VAR>𝕜 : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : NormedSpace 𝕜 E<VAR>inst✝ : LocallyCompactSpace E<VAR>r : ℝ<VAR>rpos : 0 < r<VAR>hr : IsCompact (closedBall 0 r)<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>hC : ∀ (n : ℕ), IsCompact (closedBall 0 (‖c‖ ^ n * r))<VAR>hTop : Tendsto (fun n => ‖c‖ ^ n * r) atTop atTop<GOAL>ProperSpace E
<VAR>S : Finset Λ'<VAR>k : Cont'<VAR>H₁ : contSupp k ⊆ S<GOAL>TM2.SupportsStmt S (tr (Λ'.ret k))
<VAR>S : Finset Λ'<VAR>k : Cont'<VAR>H₁ : contSupp k ⊆ S<VAR>W : ∀ {q : Λ'}, q ∈ trStmts₁ q<GOAL>TM2.SupportsStmt S (tr (Λ'.ret k))
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>x y : E<VAR>h : SameRay ℝ x y<GOAL>‖x - y‖ = |‖x‖ - ‖y‖|
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>u : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>h : SameRay ℝ (a • u) (b • u)<GOAL>‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>u : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>h : SameRay ℝ (a • u) (b • u)<VAR>hab : b ≤ a<GOAL>‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
<VAR>E : Type u_1<VAR>inst✝³ : SeminormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>u : E<VAR>a b : ℝ<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>h : SameRay ℝ (a • u) (b • u)<VAR>hab : 0 ≤ a - b<GOAL>‖a • u - b • u‖ = |‖a • u‖ - ‖b • u‖|
<VAR>n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits<GOAL>digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (bit b n).bits
<VAR>n✝ : ℕ<VAR>b : Bool<VAR>n : ℕ<VAR>h : n ≠ 0<VAR>ih : digits 2 n = List.map (fun b => bif b then 1 else 0) n.bits<GOAL>digits 2 (bit b n) = List.map (fun b => bif b then 1 else 0) (b :: n.bits)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p q r✝ : R[X]<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>r : R<GOAL>map f (r • p) = f r • map f p
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty<VAR>y : α<VAR>hy : y ∈ Icc a b<GOAL>y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁶ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁵ : TopologicalSpace α<VAR>inst✝⁴ : OrderTopology α<VAR>inst✝³ : ConditionallyCompleteLinearOrder β<VAR>inst✝² : TopologicalSpace β<VAR>inst✝¹ : OrderTopology β<VAR>inst✝ : Nonempty γ<VAR>a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty<VAR>y : α<VAR>hy : y ∈ Icc a b<VAR>this : IsClosed (s ∩ Icc a y)<GOAL>y ∈ s