ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>h : ∀ (u : ℕ → ι), Tendsto u atTop l → TendstoUniformlyOn (fun n => F (u n)) f atTop s<VAR>u : ℕ → ι × α<VAR>hu : Tendsto (fun n => (u n).1) atTop l ∧ Tendsto (fun n => (u n).2) atTop (𝓟 s)<GOAL>Tendsto ((fun q => (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
<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>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>u : ℕ → ι × α<VAR>hu : Tendsto (fun n => (u n).1) atTop l ∧ Tendsto (fun n => (u n).2) atTop (𝓟 s)<VAR>h : TendstoUniformlyOn (fun n => F (u n).1) f atTop s<GOAL>Tendsto ((fun q => (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
<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>l : Filter ι<VAR>inst✝ : l.IsCountablyGenerated<VAR>u : ℕ → ι × α<VAR>hu : Tendsto (fun n => (u n).1) atTop l ∧ Tendsto (fun n => (u n).2) atTop (𝓟 s)<VAR>h : Tendsto (fun q => (f q.2, F (u q.1).1 q.2)) (atTop ×ˢ 𝓟 s) (𝓤 β)<GOAL>Tendsto ((fun q => (f q.2, F q.1 q.2)) ∘ u) atTop (𝓤 β)
<VAR>a b m n✝ p✝ n p : ℕ<GOAL>n.factorization p = 0 ↔ ¬Prime p ∨ ¬p ∣ n ∨ n = 0
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<GOAL>connectedComponent x = ⋂ s, ↑s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<GOAL>⋂ Z, ↑Z ⊆ connectedComponent x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<GOAL>IsPreconnected (⋂ Z, ↑Z)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<VAR>hs : IsClosed (⋂ s, ↑s)<GOAL>IsPreconnected (⋂ Z, ↑Z)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<VAR>hs : IsClosed (⋂ s, ↑s)<GOAL>∀ (u v : Set X), IsClosed u → IsClosed v → ⋂ s, ↑s ⊆ u ∪ v → Disjoint u v → ⋂ s, ↑s ⊆ u ∨ ⋂ s, ↑s ⊆ v
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<VAR>hs : IsClosed (⋂ s, ↑s)<VAR>a b : Set X<VAR>ha : IsClosed a<VAR>hb : IsClosed b<VAR>hab : ⋂ s, ↑s ⊆ a ∪ b<VAR>ab_disj : Disjoint a b<GOAL>⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : T2Space X<VAR>inst✝ : CompactSpace X<VAR>x : X<VAR>hs : IsClosed (⋂ s, ↑s)<VAR>a b : Set X<VAR>ha : IsClosed a<VAR>hb : IsClosed b<VAR>hab : ⋂ s, ↑s ⊆ a ∪ b<VAR>ab_disj : Disjoint a b<VAR>u v : Set X<VAR>hu : IsOpen u<VAR>hv : IsOpen v<VAR>hau : a ⊆ u<VAR>hbv : b ⊆ v<VAR>huv : Disjoint u v<GOAL>⋂ s, ↑s ⊆ a ∨ ⋂ s, ↑s ⊆ b
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>R : Type x<VAR>inst✝² : Add α<VAR>inst✝¹ : MulOneClass α<VAR>inst✝ : RightDistribClass α<VAR>a b : α<GOAL>(1 + a) * b = b + a * b
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<GOAL>y ∈ closure {x} ↔ ∃ n, x ^ n = y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<VAR>hy : y ∈ closure {x}<GOAL>∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<VAR>hy : y ∈ closure {x}<GOAL>∃ n, x ^ n = 1
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<VAR>hy : y ∈ closure {x}<GOAL>∀ (x_1 y : G), (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<VAR>hy : y ∈ closure {x}<GOAL>∀ (x_1 : G), (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'<VAR>inst✝¹ : Group G''<VAR>A : Type u_4<VAR>inst✝ : AddGroup A<VAR>H K : Subgroup G<VAR>k : Set G<VAR>x y : G<VAR>hy : y ∈ closure {x}<VAR>n : ℤ<GOAL>∃ n_1, x ^ n_1 = (x ^ n)⁻¹
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : LinearOrder α<VAR>l : List α<VAR>a m : α<GOAL>↑a ≤ l.maximum ↔ ∃ b, b ∈ l ∧ a ≤ b
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>R : Type u_3<VAR>R₂ : Type u_4<VAR>K : Type u_5<VAR>M : Type u_6<VAR>M' : Type u_7<VAR>M'' : Type u_8<VAR>V : Type u<VAR>V' : Type u_9<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : Module R M'<VAR>S : Type u_10<VAR>inst✝³ : Semiring S<VAR>inst✝² : Module S M'<VAR>inst✝¹ : SMulCommClass R S M'<VAR>inst✝ : Fintype ι<VAR>P : Submodule R M<VAR>b : Basis ι R ↥P<VAR>x : M<VAR>c : ι → R<GOAL>(x = (Finsupp.equivFunOnFinite.symm c).sum fun i x => x • ↑(b i)) ↔ x = ∑ i : ι, c i • ↑(b i)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝ : p.IsHomLift f φ<GOAL>p.obj a = R
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsHomLift (p.map φ) φ<GOAL>p.obj a✝ = p.obj a✝
<VAR>α : Type u_1<VAR>s t : Finset α<VAR>a : α<VAR>inst✝ : DecidableEq α<VAR>h : s ⋖ t<GOAL>∃ a ∈ t, t.erase a = s
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³¹ : Semiring R₁<VAR>inst✝³⁰ : Semiring R₂<VAR>inst✝²⁹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>inst✝²⁸ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁷ : RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>inst✝²⁶ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝²⁵ : RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>inst✝²⁴ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝²³ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝²² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝²¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M₁<VAR>inst✝¹⁹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁸ : TopologicalSpace M'₁<VAR>inst✝¹⁷ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace M₂<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁴ : TopologicalSpace M₃<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹² : TopologicalSpace M₄<VAR>inst✝¹¹ : AddCommMonoid M₄<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>inst✝⁹ : Module R₁ M'₁<VAR>inst✝⁸ : Module R₂ M₂<VAR>inst✝⁷ : Module R₃ M₃<VAR>R₄ : Type u_9<VAR>inst✝⁶ : Semiring R₄<VAR>inst✝⁵ : Module R₄ M₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝³ : RingHomInvPair σ₄₃ σ₃₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>e₁₂ : M₁ ≃SL[σ₁₂] M₂<VAR>e₄₃ : M₄ ≃SL[σ₄₃] M₃<VAR>f : M₁ →SL[σ₁₄] M₄<VAR>x : M₁<GOAL>((fun f => (↑e₄₃.symm).comp (f.comp ↑e₁₂)) ((fun f => (↑e₄₃).comp (f.comp ↑e₁₂.symm)) f)) x = f x
<VAR>R₁ : Type u_1<VAR>R₂ : Type u_2<VAR>R₃ : Type u_3<VAR>inst✝³¹ : Semiring R₁<VAR>inst✝³⁰ : Semiring R₂<VAR>inst✝²⁹ : Semiring R₃<VAR>σ₁₂ : R₁ →+* R₂<VAR>σ₂₁ : R₂ →+* R₁<VAR>inst✝²⁸ : RingHomInvPair σ₁₂ σ₂₁<VAR>inst✝²⁷ : RingHomInvPair σ₂₁ σ₁₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₃₂ : R₃ →+* R₂<VAR>inst✝²⁶ : RingHomInvPair σ₂₃ σ₃₂<VAR>inst✝²⁵ : RingHomInvPair σ₃₂ σ₂₃<VAR>σ₁₃ : R₁ →+* R₃<VAR>σ₃₁ : R₃ →+* R₁<VAR>inst✝²⁴ : RingHomInvPair σ₁₃ σ₃₁<VAR>inst✝²³ : RingHomInvPair σ₃₁ σ₁₃<VAR>inst✝²² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝²¹ : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁<VAR>M₁ : Type u_4<VAR>inst✝²⁰ : TopologicalSpace M₁<VAR>inst✝¹⁹ : AddCommMonoid M₁<VAR>M'₁ : Type u_5<VAR>inst✝¹⁸ : TopologicalSpace M'₁<VAR>inst✝¹⁷ : AddCommMonoid M'₁<VAR>M₂ : Type u_6<VAR>inst✝¹⁶ : TopologicalSpace M₂<VAR>inst✝¹⁵ : AddCommMonoid M₂<VAR>M₃ : Type u_7<VAR>inst✝¹⁴ : TopologicalSpace M₃<VAR>inst✝¹³ : AddCommMonoid M₃<VAR>M₄ : Type u_8<VAR>inst✝¹² : TopologicalSpace M₄<VAR>inst✝¹¹ : AddCommMonoid M₄<VAR>inst✝¹⁰ : Module R₁ M₁<VAR>inst✝⁹ : Module R₁ M'₁<VAR>inst✝⁸ : Module R₂ M₂<VAR>inst✝⁷ : Module R₃ M₃<VAR>R₄ : Type u_9<VAR>inst✝⁶ : Semiring R₄<VAR>inst✝⁵ : Module R₄ M₄<VAR>σ₃₄ : R₃ →+* R₄<VAR>σ₄₃ : R₄ →+* R₃<VAR>inst✝⁴ : RingHomInvPair σ₃₄ σ₄₃<VAR>inst✝³ : RingHomInvPair σ₄₃ σ₃₄<VAR>σ₂₄ : R₂ →+* R₄<VAR>σ₁₄ : R₁ →+* R₄<VAR>inst✝² : RingHomCompTriple σ₂₁ σ₁₄ σ₂₄<VAR>inst✝¹ : RingHomCompTriple σ₂₄ σ₄₃ σ₂₃<VAR>inst✝ : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄<VAR>e₁₂ : M₁ ≃SL[σ₁₂] M₂<VAR>e₄₃ : M₄ ≃SL[σ₄₃] M₃<VAR>f : M₂ →SL[σ₂₃] M₃<VAR>x : M₂<GOAL>((fun f => (↑e₄₃).comp (f.comp ↑e₁₂.symm)) ((fun f => (↑e₄₃.symm).comp (f.comp ↑e₁₂)) f)) x = f x
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<GOAL>∃ b ⊆ t, span K b = span K t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>b : Set V<VAR>hb₁ : b ⊆ t<VAR>hb₂ : t ⊆ ↑(span K b)<VAR>hb₃ : LinearIndependent (ι := { x // x ∈ b }) K Subtype.val<GOAL>∃ b ⊆ t, span K b = span K t ∧ LinearIndependent (ι := { x // x ∈ b }) K Subtype.val
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>aleph' o = ⨆ a, aleph' ↑a
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>aleph' o ≤ ⨆ a, aleph' ↑a
<VAR>o : Ordinal.{u_1}<VAR>ho : o.IsLimit<GOAL>∀ o' < o, aleph' o' ≤ ⨆ a, aleph' ↑a
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<GOAL>⟪x, x⟫_ℝ = ‖x‖ * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>h : re ⟪x, x⟫_ℝ = ‖x‖ * ‖x‖<GOAL>⟪x, x⟫_ℝ = ‖x‖ * ‖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✝⁹ : Group G<VAR>inst✝⁸ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝⁷ : μ.IsHaarMeasure<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>H : Type u_4<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : MeasurableSpace H<VAR>inst✝¹ : BorelSpace H<VAR>inst✝ : TopologicalGroup H<VAR>e : G ≃* H<VAR>he : Continuous ⇑e<VAR>hesymm : Continuous ⇑e.symm<VAR>K : Set H<VAR>hK : IsCompact K<VAR>F : G ≃ₜ H := let __src := e.toEquiv; { toEquiv := __src, continuous_toFun := he, continuous_invFun := hesymm }<GOAL>(map (⇑F.toMeasurableEquiv) μ) K < ⊤
<VAR>𝕜 : Type u_1<VAR>G : Type u_2<VAR>H✝ : Type u_3<VAR>inst✝¹¹ : MeasurableSpace G<VAR>inst✝¹⁰ : MeasurableSpace H✝<VAR>inst✝⁹ : Group G<VAR>inst✝⁸ : TopologicalSpace G<VAR>μ : Measure G<VAR>inst✝⁷ : μ.IsHaarMeasure<VAR>inst✝⁶ : BorelSpace G<VAR>inst✝⁵ : TopologicalGroup G<VAR>H : Type u_4<VAR>inst✝⁴ : Group H<VAR>inst✝³ : TopologicalSpace H<VAR>inst✝² : MeasurableSpace H<VAR>inst✝¹ : BorelSpace H<VAR>inst✝ : TopologicalGroup H<VAR>e : G ≃* H<VAR>he : Continuous ⇑e<VAR>hesymm : Continuous ⇑e.symm<VAR>K : Set H<VAR>hK : IsCompact K<VAR>F : G ≃ₜ H := let __src := e.toEquiv; { toEquiv := __src, continuous_toFun := he, continuous_invFun := hesymm }<GOAL>μ (⇑F.toMeasurableEquiv ⁻¹' K) < ⊤
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i j : A<GOAL>(shiftFunctorComm C i j).inv = (shiftFunctorComm C j i).hom
<VAR>C : Type u<VAR>A : Type u_1<VAR>inst✝² : Category.{v, u} C<VAR>inst✝¹ : AddCommMonoid A<VAR>inst✝ : HasShift C A<VAR>i j : A<GOAL>((shiftFunctorAdd' C i j (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C j i (i + j) ⋯).inv = ((shiftFunctorAdd' C j i (i + j) ⋯).symm ≪≫ shiftFunctorAdd' C i j (i + j) ⋯).hom
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : CommGroup α<VAR>inst✝ : CommGroup β<VAR>s : Set α<VAR>t u : Finset α<VAR>d : ℕ<VAR>a : α<VAR>e : β ≃* α<GOAL>MulDissociated (⇑e ⁻¹' s) ↔ MulDissociated s
<VAR>𝕜 : Type u<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type uX<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>m n : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<GOAL>(∀ (m : ℕ), ↑m ≤ ⊤ → ContDiffWithinAt 𝕜 (↑m) f s x) ↔ ∀ (n : ℕ), ContDiffWithinAt 𝕜 (↑n) f s x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s t : Set α<VAR>a b : α<VAR>h : a ∈ s<GOAL>(s \ {a}).encard + 1 = s.encard
<VAR>R : Type u<VAR>inst✝ : Semiring R<GOAL>#R[X] ≤ max #R ℵ₀
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>h✝ : Subsingleton R<GOAL>#R[X] ≤ max #R ℵ₀
<VAR>R : Type u<VAR>inst✝ : Semiring R<VAR>h✝ : Nontrivial R<GOAL>#R[X] ≤ max #R ℵ₀
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Opens α<GOAL>IsCoatom s ↔ ∃ x, s = (Closeds.singleton x).compl
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Opens α<GOAL>IsAtom (toDual s.compl.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : T1Space α<VAR>s : Opens α<GOAL>IsAtom ((Closeds.complOrderIso α) s.compl) ↔ ∃ x, s.compl.compl = (Closeds.singleton x).compl
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<VAR>hm : (node size✝ l✝ x✝ r✝).Sized<GOAL>(if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size = l.size + size✝ + 1
<VAR>α : Type u_1<VAR>l : Ordnode α<VAR>x : α<VAR>size✝ : ℕ<VAR>l✝ : Ordnode α<VAR>x✝ : α<VAR>r✝ : Ordnode α<VAR>hm : (node size✝ l✝ x✝ r✝).Sized<GOAL>(if l✝.size < ratio * r✝.size then l.node3L x l✝ x✝ r✝ else l.node4L x l✝ x✝ r✝).size = l.size + (l✝.size + r✝.size + 1) + 1
<VAR>q : ℚ<VAR>a : ℤ<VAR>b : ℕ<GOAL>(mkRat a b)⁻¹ = ↑b /. a
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>S S' S'' : D<VAR>Y Y' Y'' : C<VAR>T T' : C ⥤ D<VAR>A : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} A<VAR>B : Type u₄<VAR>inst✝ : Category.{v₄, u₄} B<VAR>f g : StructuredArrow S T<VAR>h : f.IsUniversal<VAR>c : C<VAR>η η' : f.right ⟶ c<VAR>w : f.hom ≫ T.map η = f.hom ≫ T.map η'<GOAL>η = η'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<GOAL>∃ δ, 0 < δ ∧ ∀ ⦃x : E⦄, ‖x‖ ≤ 1 → ∀ ⦃y : E⦄, ‖y‖ ≤ 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : ‖x‖ ≤ 1 - δ'<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : ‖y‖ ≤ 1 - δ'<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : 1 - δ' < ‖y‖<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : 1 - δ' < ‖y‖<VAR>hδ' : 0 < 1 - δ'<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : 1 - δ' < ‖y‖<VAR>hδ' : 0 < 1 - δ'<VAR>h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : 1 - δ' < ‖y‖<VAR>hδ' : 0 < 1 - δ'<VAR>h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1<VAR>h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>E : Type u_1<VAR>inst✝² : SeminormedAddCommGroup E<VAR>inst✝¹ : UniformConvexSpace E<VAR>ε : ℝ<VAR>inst✝ : NormedSpace ℝ E<VAR>hε : 0 < ε<VAR>hε' : 0 < ε / 3<VAR>δ : ℝ<VAR>hδ : 0 < δ<VAR>h : ∀ ⦃x : E⦄, ‖x‖ = 1 → ∀ ⦃y : E⦄, ‖y‖ = 1 → ε / 3 ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ<VAR>δ' : ℝ := min (1 / 2) (min (ε / 3) (δ / 3))<VAR>x : E<VAR>hx : ‖x‖ ≤ 1<VAR>y : E<VAR>hy : ‖y‖ ≤ 1<VAR>hxy : ε ≤ ‖x - y‖<VAR>hx' : 1 - δ' < ‖x‖<VAR>hy' : 1 - δ' < ‖y‖<VAR>hδ' : 0 < 1 - δ'<VAR>h₁ : ∀ (z : E), 1 - δ' < ‖z‖ → ‖‖z‖⁻¹ • z‖ = 1<VAR>h₂ : ∀ (z : E), ‖z‖ ≤ 1 → 1 - δ' ≤ ‖z‖ → ‖‖z‖⁻¹ • z - z‖ ≤ δ'<VAR>x' : E := ‖x‖⁻¹ • x<VAR>y' : E := ‖y‖⁻¹ • y<VAR>hxy' : ε / 3 ≤ ‖x' - y'‖<GOAL>‖x + y‖ ≤ 2 - δ'
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<GOAL>(ker f).IsMaximal
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<GOAL>1 ∈ J
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<VAR>y : R<VAR>hy : f y = (f x)⁻¹<GOAL>1 ∈ J
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<VAR>y : R<VAR>hy : f y = (f x)⁻¹<VAR>H : 1 = y * x - (y * x - 1)<GOAL>1 ∈ J
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<VAR>y : R<VAR>hy : f y = (f x)⁻¹<VAR>H : 1 = y * x - (y * x - 1)<GOAL>y * x - (y * x - 1) ∈ J
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<VAR>y : R<VAR>hy : f y = (f x)⁻¹<VAR>H : 1 = y * x - (y * x - 1)<GOAL>y * x - 1 ∈ ker f
<VAR>R✝ : Type u<VAR>S : Type v<VAR>T : Type w<VAR>R : Type u_1<VAR>K : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : Ring R<VAR>inst✝² : Field K<VAR>inst✝¹ : FunLike F R K<VAR>inst✝ : RingHomClass F R K<VAR>f : F<VAR>hf : Function.Surjective ⇑f<VAR>J : Ideal R<VAR>x : R<VAR>hJ : ker f ≤ J<VAR>hxf : x ∉ ker f<VAR>hxJ : x ∈ J<VAR>y : R<VAR>hy : f y = (f x)⁻¹<VAR>H : 1 = y * x - (y * x - 1)<GOAL>f (y * x - 1) = 0