ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>x : ℝ<VAR>A : 0 < ↑⌊‖x‖⌋₊ + 1<VAR>B : ‖x‖ / (↑⌊‖x‖⌋₊ + 1) < 1<VAR>n : ℕ<VAR>hn : n ≥ ⌊‖x‖⌋₊<GOAL>‖x ^ (n + 1) / ↑(n + 1)!‖ ≤ ‖x‖ / (↑⌊‖x‖⌋₊ + 1) * ‖x ^ n / ↑n !‖
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<GOAL>toJordanDecomposition 0 = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<GOAL>(toJordanDecomposition 0).toSignedMeasure = toSignedMeasure 0
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>h : IsCyclic α<GOAL>∃ g, orderOf g = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>h : IsCyclic α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<GOAL>∃ g, orderOf g = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>h : IsCyclic α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<GOAL>orderOf g = Nat.card α
<VAR>α : Type u<VAR>a : α<VAR>inst✝ : Group α<VAR>h : IsCyclic α<VAR>g : α<VAR>hg : ∀ (x : α), x ∈ zpowers g<GOAL>Nat.card ↥⊤ = Nat.card α
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x y z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<GOAL>z ⊓ x ⊓ y ⊔ x \ y = x \ y ⊔ x ⊓ z
<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>StrictConvexOn ℝ (Ici 0) fun x => x ^ p
<VAR>p : ℝ<VAR>hp : 1 < p<GOAL>∀ {x y z : ℝ}, x ∈ Ici 0 → z ∈ Ici 0 → x < y → y < z → (y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
<VAR>p : ℝ<VAR>hp : 1 < p<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hz : 0 ≤ z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hy : 0 < y<GOAL>(y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
<VAR>p : ℝ<VAR>hp : 1 < p<VAR>x y z : ℝ<VAR>hx : 0 ≤ x<VAR>hz : 0 ≤ z<VAR>hxy : x < y<VAR>hyz : y < z<VAR>hy : 0 < y<VAR>hy' : 0 < y ^ p<GOAL>(y ^ p - x ^ p) / (y - x) < (z ^ p - y ^ p) / (z - y)
<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✝³ : OrderedAddCommGroup β<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>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)<GOAL>∀ ⦃j : ι⦄, j ∈ t → ∀ ⦃k : ι⦄, k ∈ t → p j = p k
<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✝³ : OrderedAddCommGroup β<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>v : 𝕜<VAR>q : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>h₀ : ∀ i ∈ t, 0 < w i<VAR>h₁ : ∑ i ∈ t, w i = 1<VAR>hmem : ∀ i ∈ t, p i ∈ s<VAR>h_eq : ∑ i ∈ t, w i • f (p i) ≤ f (∑ i ∈ t, w i • p i)<VAR>this : ∃ j ∈ t, ∃ k ∈ t, p j ≠ p k<GOAL>False
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a b c : α<VAR>n : ℤ<VAR>hp' : Fact (0 < p)<VAR>x₁ x₂ x₃ : α<GOAL>btw ↑x₁ ↑x₂ ↑x₃ ↔ toIcoMod ⋯ x₁ x₂ ≤ toIocMod ⋯ x₁ x₃
<VAR>J : Type w<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>D : Type uD<VAR>inst✝² : Category.{uD', uD} D<VAR>inst✝¹ : HasZeroMorphisms D<VAR>P Q X Y : C<VAR>inst✝ : HasBinaryBiproduct X Y<GOAL>(isoProd X Y).inv = lift prod.fst prod.snd
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>e : PartialEquiv α β<VAR>e'✝ : PartialEquiv β γ<VAR>s : Set α<VAR>t : Set β<VAR>x : α<VAR>y : β<VAR>e' : PartialEquiv α β<VAR>h : e.IsImage s t<VAR>h' : e'.IsImage s t<VAR>hs : e.source ∩ s = e'.source ∩ s<VAR>heq : EqOn (↑e) (↑e') (e.source ∩ s)<GOAL>e.target ∩ t = e'.target ∩ t
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Group α<VAR>inst✝ : ContinuousConstSMul α α<VAR>s t : Set α<VAR>a : α<VAR>h : s ∈ 𝓝 1<GOAL>{a} * s ∈ 𝓝 a
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v₁, u₁} C<VAR>inst✝⁷ : MonoidalCategory C<VAR>inst✝⁶ : BraidedCategory C<VAR>D : Type u₂<VAR>inst✝⁵ : Category.{v₂, u₂} D<VAR>inst✝⁴ : MonoidalCategory D<VAR>inst✝³ : BraidedCategory D<VAR>E : Type u₃<VAR>inst✝² : Category.{v₃, u₃} E<VAR>inst✝¹ : MonoidalCategory E<VAR>inst✝ : BraidedCategory E<VAR>X₁ X₂ Y₁ Y₂ : C<VAR>f₁ : X₁ ⟶ Y₁<VAR>f₂ : X₂ ⟶ Y₂<VAR>Z₁ Z₂ : C<GOAL>(f₁ ⊗ f₂) ▷ (Z₁ ⊗ Z₂) ≫ tensor_μ C (Y₁, Y₂) (Z₁, Z₂) = tensor_μ C (X₁, X₂) (Z₁, Z₂) ≫ (f₁ ▷ Z₁ ⊗ f₂ ▷ Z₂)
<VAR>V : Type u<VAR>V' : Type v<VAR>V'' : Type w<VAR>G : SimpleGraph V<VAR>G' : SimpleGraph V'<VAR>G'' : SimpleGraph V''<VAR>u v : V<VAR>p : G.Path v u<VAR>h : G.Adj u v<VAR>he : s(u, v) ∉ (↑p).edges<GOAL>(Walk.cons h ↑p).IsCycle
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>s / ball 1 δ = thickening δ s
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>G : Type u_7<VAR>inst✝² : Monoid M<VAR>inst✝¹ : Monoid N<VAR>inst✝ : Monoid P<VAR>l✝ l₁ l₂ : List M<VAR>a✝ a : M<VAR>l : List M<GOAL>(a :: l).prod = foldr (fun x x_1 => x * x_1) 1 (a :: l)
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<GOAL>Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<GOAL>Real.sin (angle x (x - y)) * ‖x - y‖ = ‖y‖
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>map (fun x => x.1 * x.2) ((dirac 1).prod μ) = μ
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>map ((fun x => x.1 * x.2) ∘ Prod.mk 1) μ = μ
<VAR>M : Type u_1<VAR>inst✝³ : Monoid M<VAR>inst✝² : MeasurableSpace M<VAR>inst✝¹ : MeasurableMul₂ M<VAR>μ : Measure M<VAR>inst✝ : SFinite μ<GOAL>Measurable (Prod.mk 1)
<VAR>b n : ℕ<GOAL>log b (n / b) = log b n - 1
<VAR>b n : ℕ<VAR>hb : b ≤ 1<GOAL>log b (n / b) = log b n - 1
<VAR>b n : ℕ<VAR>hb : 1 < b<GOAL>log b (n / b) = log b n - 1
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>h : n < b<GOAL>log b (n / b) = log b n - 1
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>h : b ≤ n<GOAL>log b (n / b) = log b n - 1
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>i : ℕ<VAR>a : R<VAR>x : E<VAR>hf : ContDiff 𝕜 (↑i) f<GOAL>iteratedFDeriv 𝕜 i (a • f) x = a • iteratedFDeriv 𝕜 i f x
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁴ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝¹³ : NormedAddCommGroup D<VAR>inst✝¹² : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝¹¹ : NormedAddCommGroup E<VAR>inst✝¹⁰ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝⁷ : NormedAddCommGroup G<VAR>inst✝⁶ : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup X<VAR>inst✝⁴ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>R : Type u_3<VAR>inst✝³ : Semiring R<VAR>inst✝² : Module R F<VAR>inst✝¹ : SMulCommClass 𝕜 R F<VAR>inst✝ : ContinuousConstSMul R F<VAR>i : ℕ<VAR>a : R<VAR>x : E<VAR>hf : ContDiffOn 𝕜 (↑i) f univ<GOAL>iteratedFDerivWithin 𝕜 i (a • f) univ x = a • iteratedFDerivWithin 𝕜 i f univ x
<VAR>ι : Sort u<VAR>α : Type v<VAR>β : Type w<VAR>inst✝¹ : LinearOrder α<VAR>s : Set α<VAR>a : α<VAR>f✝ : ι → α<VAR>R : Type u_1<VAR>inst✝ : CompleteLinearOrder R<VAR>f : ι → R<VAR>no_least_elem : ⨅ i, f i ∉ range f<GOAL>⋃ i, Ici (f i) = Ioi (⨅ i, f i)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x)
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<GOAL>TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, ∀ u ∈ 𝓤 β, ∃ pa, (∀ᶠ (x : ι) in p, pa x) ∧ ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>n : Type u_4<VAR>ι : Type u_5<VAR>ι' : Type u_6<VAR>ιM : Type u_7<VAR>inst✝¹² : CommRing R<VAR>inst✝¹¹ : AddCommGroup L<VAR>inst✝¹⁰ : Module R L<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>φ : L →ₗ[R] Module.End R M<VAR>inst✝⁷ : Fintype ι<VAR>inst✝⁶ : Fintype ι'<VAR>inst✝⁵ : Fintype ιM<VAR>inst✝⁴ : DecidableEq ι<VAR>inst✝³ : DecidableEq ι'<VAR>inst✝² : Module.Free R M<VAR>inst✝¹ : Module.Finite R M<VAR>b : Basis ι R L<VAR>inst✝ : Nontrivial R<GOAL>(φ.polyCharpoly b).natDegree = finrank R M
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<GOAL>SeparatedNhds s t
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : NormalSpace Y<VAR>f : X → Y<VAR>hf : ClosedEmbedding f<VAR>s t : Set X<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hst : Disjoint s t<VAR>H : SeparatedNhds (f '' s) (f '' t)<GOAL>SeparatedNhds s t
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>R : Type u_4<VAR>inst✝¹ : Semiring α<VAR>inst✝ : Semiring β<VAR>a b : α<VAR>m n : ℕ<GOAL>Odd (a + (1 + a))
<VAR>x y : ℝ<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℝ<VAR>hf : ∀ x ∈ s, f x ≠ 0<GOAL>log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)
<VAR>x y : ℝ<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>hf : ∀ x ∈ ∅, f x ≠ 0<GOAL>log (∏ i ∈ ∅, f i) = ∑ i ∈ ∅, log (f i)
<VAR>x y : ℝ<VAR>α : Type u_1<VAR>f : α → ℝ<VAR>a : α<VAR>s : Finset α<VAR>ha : a ∉ s<VAR>ih : (∀ x ∈ s, f x ≠ 0) → log (∏ i ∈ s, f i) = ∑ i ∈ s, log (f i)<VAR>hf : ∀ x ∈ Finset.cons a s ha, f x ≠ 0<GOAL>log (∏ i ∈ Finset.cons a s ha, f i) = ∑ i ∈ Finset.cons a s ha, log (f i)
<VAR>C : Type u<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>Z : C<VAR>P : ProjectiveResolution Z<GOAL>P.complex.d 1 0 ≫ P.π.f 0 = 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<GOAL>⨆ k, LieSubmodule.ucs k ⊥ = weightSpace M 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>k : ℕ<VAR>hk : weightSpace M 0 ≤ LieSubmodule.ucs k ⊥<GOAL>⨆ k, LieSubmodule.ucs k ⊥ = weightSpace M 0
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>k : ℕ<VAR>hk : weightSpace M 0 ≤ LieSubmodule.ucs k ⊥<GOAL>LieSubmodule.ucs k ⊥ ≤ ⨆ k, LieSubmodule.ucs k ⊥
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<GOAL>φ = ψ
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>∀ (x : A) (h : x ∈ {a}), φ ((StarSubalgebra.inclusion ⋯) ⟨x, ⋯⟩) = ψ ((StarSubalgebra.inclusion ⋯) ⟨x, ⋯⟩)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>∀ (r : R), φ ((StarSubalgebra.inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r)) = ψ ((StarSubalgebra.inclusion ⋯) ((algebraMap R ↥(adjoin R {a})) r))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>∀ (x y : ↥(adjoin R {a})), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x) → φ ((StarSubalgebra.inclusion ⋯) y) = ψ ((StarSubalgebra.inclusion ⋯) y) → φ ((StarSubalgebra.inclusion ⋯) (x + y)) = ψ ((StarSubalgebra.inclusion ⋯) (x + y))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>∀ (x y : ↥(adjoin R {a})), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x) → φ ((StarSubalgebra.inclusion ⋯) y) = ψ ((StarSubalgebra.inclusion ⋯) y) → φ ((StarSubalgebra.inclusion ⋯) (x * y)) = ψ ((StarSubalgebra.inclusion ⋯) (x * y))
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : TopologicalSpace A<VAR>inst✝¹³ : Semiring A<VAR>inst✝¹² : StarRing A<VAR>inst✝¹¹ : TopologicalSemiring A<VAR>inst✝¹⁰ : ContinuousStar A<VAR>inst✝⁹ : Algebra R A<VAR>inst✝⁸ : StarModule R A<VAR>inst✝⁷ : TopologicalSpace B<VAR>inst✝⁶ : Semiring B<VAR>inst✝⁵ : StarRing B<VAR>inst✝⁴ : Algebra R B<VAR>inst✝³ : T2Space B<VAR>F : Type u_4<VAR>a : A<VAR>inst✝² : FunLike F (↥(elementalStarAlgebra R a)) B<VAR>inst✝¹ : AlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>inst✝ : StarAlgHomClass F R (↥(elementalStarAlgebra R a)) B<VAR>φ ψ : F<VAR>hφ : Continuous ⇑φ<VAR>hψ : Continuous ⇑ψ<VAR>h : φ ⟨a, ⋯⟩ = ψ ⟨a, ⋯⟩<VAR>this : StarAlgHomClass F R (↥(adjoin R {a}).topologicalClosure) B<VAR>x : ↥(adjoin R {a})<GOAL>∀ (x : ↥(adjoin R {a})), φ ((StarSubalgebra.inclusion ⋯) x) = ψ ((StarSubalgebra.inclusion ⋯) x) → φ ((StarSubalgebra.inclusion ⋯) (star x)) = ψ ((StarSubalgebra.inclusion ⋯) (star x))
<VAR>α : Type u_1<VAR>inst✝¹ : CancelCommMonoidWithZero α<VAR>inst✝ : NormalizationMonoid α<VAR>a : α<VAR>b : Associates α<GOAL>∀ (a_1 : α), a ∣ Associates.out ⟦a_1⟧ ↔ Associates.mk a ≤ ⟦a_1⟧
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>hf : IsUnit f<GOAL>X.basicOpen f = U
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>hf : IsUnit f<GOAL>X.basicOpen f ≤ U
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>hf : IsUnit f<GOAL>U ≤ X.basicOpen f
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>hf : IsUnit f<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ↑U<GOAL>x ∈ ↑(X.basicOpen f)
<VAR>X : RingedSpace<VAR>U : Opens ↑↑X.toPresheafedSpace<VAR>f : ↑(X.presheaf.obj (op U))<VAR>hf : IsUnit f<VAR>x : ↑↑X.toPresheafedSpace<VAR>hx : x ∈ ↑U<GOAL>IsUnit ((X.presheaf.germ ⟨x, hx⟩) f)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>H : IsTotallySeparated s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>ht : IsPreconnected t<VAR>x : α<VAR>x_in : x ∈ t<VAR>y : α<VAR>y_in : y ∈ t<GOAL>x = y
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u v s : Set α<VAR>H : IsTotallySeparated s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>ht : IsPreconnected t<VAR>x : α<VAR>x_in : x ∈ t<VAR>y : α<VAR>y_in : y ∈ t<VAR>h : ¬x = y<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s✝ t✝ u✝ v✝ s : Set α<VAR>H : IsTotallySeparated s<VAR>t : Set α<VAR>hts : t ⊆ s<VAR>ht : IsPreconnected t<VAR>x : α<VAR>x_in : x ∈ t<VAR>y : α<VAR>y_in : y ∈ t<VAR>h : ¬x = y<VAR>u v : Set α<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>hxu : x ∈ u<VAR>hyv : y ∈ v<VAR>hs : s ⊆ u ∪ v<VAR>huv : Disjoint u v<GOAL>t ∩ (u ∩ v) = ∅
<VAR>α : Type u_1<VAR>inst✝¹ : MeasurableSpace α<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace β<VAR>μ : FiniteMeasure α<VAR>ν : FiniteMeasure β<GOAL>prod 0 ν = 0
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : G<GOAL>(A.leftRegularHomEquiv.symm x).hom (Finsupp.single g 1) = (A.ρ g) x
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>inst✝ : Monoid G<VAR>X Y : Action (Type u) (MonCat.of G)<VAR>f : X ⟶ Y<VAR>A : Rep k G<VAR>x : CoeSort.coe A<VAR>g : G<GOAL>0 • (A.ρ g) x = 0
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<GOAL>∃ y, i y.2 = x ^ p ^ y.1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁷ : CommSemiring K<VAR>inst✝⁶ : CommSemiring L<VAR>inst✝⁵ : CommSemiring M<VAR>i : K →+* L<VAR>j : K →+* M<VAR>f : L →+* M<VAR>p : ℕ<VAR>inst✝⁴ : ExpChar K p<VAR>inst✝³ : ExpChar L p<VAR>inst✝² : ExpChar M p<VAR>inst✝¹ : PerfectRing M p<VAR>inst✝ : IsPRadical i p<VAR>x : L<VAR>n : ℕ<VAR>y : K<VAR>h : i y = x ^ p ^ n<GOAL>∃ y, i y.2 = x ^ p ^ y.1
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : ¬c = 0<GOAL>a / c + b / c ≤ (a + b) / c
<VAR>m n a✝ b✝ c✝ d a b c : ℕ<VAR>hc0 : ¬c = 0<GOAL>a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>IsBounded ∅
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>x✝ : Bornology α<VAR>s t : Set α<VAR>x : α<GOAL>univ ∈ cobounded α
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝⁴ : MulOneClass α<VAR>inst✝³ : Zero α<VAR>inst✝² : Preorder α<VAR>inst✝¹ : PosMulStrictMono α<VAR>inst✝ : PosMulReflectLT α<VAR>a0 : 0 < a<GOAL>a * b < a ↔ a * b < a * 1
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<VAR>H✝ : IsCoprime x y<VAR>a b : R<VAR>H : a * x + b * y = 1<GOAL>b * y + a * x = 1
<VAR>α : Type u_1<VAR>γ : Type u_2<VAR>mα : MeasurableSpace α<VAR>mγ : MeasurableSpace γ<VAR>κ✝ η✝ : Kernel α γ<VAR>hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ<VAR>κ η : Kernel α γ<VAR>x✝¹ : α<VAR>x✝ : γ<GOAL>κ.rnDeriv η x✝¹ x✝ = ENNReal.ofReal (κ.rnDerivAux (κ + η) x✝¹ x✝) / ENNReal.ofReal (1 - κ.rnDerivAux (κ + η) x✝¹ x✝)
<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<GOAL>a / b = ⊤ ↔ a ≠ 0 ∧ b = 0 ∨ a = ⊤ ∧ b ≠ ⊤
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : Finite β<GOAL>closure {σ | σ.IsCycle} = ⊤
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Sort x<VAR>a b : α<VAR>s s₁ s₂ t t₁ t₂ u : Set α<VAR>h : a ∈ s<GOAL>s ∩ insert a t = insert a (s ∩ t)
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>x : α<GOAL>x ∈ {x | (p * q) x ≠ x} → x ∈ {x | p x ≠ x} ∪ {x | q x ≠ x}
<VAR>α : Type u_1<VAR>p q : Perm α<VAR>x : α<GOAL>¬p (q x) = x → ¬p x = x ∨ ¬q x = x