ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<VAR>hne : ∀ z ∈ sphere c R, z ≠ w<VAR>hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)<VAR>hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)<GOAL>CircleIntegrable (fun z => (z - w)⁻¹ • f z) c R
<VAR>E : Type u<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>R : ℝ<VAR>c w : ℂ<VAR>f : ℂ → E<VAR>s : Set ℂ<VAR>hs : s.Countable<VAR>hw : w ∈ ball c R \ s<VAR>hc : ContinuousOn f (closedBall c R)<VAR>hd : ∀ x ∈ ball c R \ s, DifferentiableAt ℂ f x<VAR>hR : 0 < R<VAR>F : ℂ → E := dslope f w<VAR>hws : (insert w s).Countable<VAR>hcF : ContinuousOn F (closedBall c R)<VAR>hdF : ∀ z ∈ ball c R \ insert w s, DifferentiableAt ℂ F z<VAR>HI : (∮ (z : ℂ) in C(c, R), F z) = 0<VAR>hne : ∀ z ∈ sphere c R, z ≠ w<VAR>hFeq : EqOn F (fun z => (z - w)⁻¹ • f z - (z - w)⁻¹ • f w) (sphere c R)<VAR>hc' : ContinuousOn (fun z => (z - w)⁻¹) (sphere c R)<GOAL>CircleIntegrable (fun z => (z - w)⁻¹ • f w) c R
<VAR>R : Type u<VAR>S : Type u_1<VAR>A : Type v<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : CommRing S<VAR>inst✝⁶ : Ring A<VAR>inst✝⁵ : Algebra R A<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra S A<VAR>inst✝² : IsScalarTower R S A<VAR>B : Type u_2<VAR>inst✝¹ : Ring B<VAR>inst✝ : Algebra R B<VAR>f : A →ₐ[R] B<VAR>hf : Function.Injective ⇑f<VAR>a : A<VAR>x✝ : IsAlgebraic R (f a)<VAR>p : R[X]<VAR>hp0 : p ≠ 0<VAR>hp : (aeval (f a)) p = 0<GOAL>f ((aeval a) p) = f 0
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℤ → G<GOAL>Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-(↑n + 1))
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℤ → G<VAR>p : Multipliable f<GOAL>Injective Nat.cast
<VAR>M : Type u_1<VAR>inst✝⁵ : CommMonoid M<VAR>inst✝⁴ : TopologicalSpace M<VAR>m m' : M<VAR>G : Type u_2<VAR>inst✝³ : CommGroup G<VAR>g g' : G<VAR>inst✝² : UniformSpace G<VAR>inst✝¹ : UniformGroup G<VAR>inst✝ : CompleteSpace G<VAR>f : ℤ → G<VAR>p : Multipliable f<GOAL>Injective fun n => -(↑n + 1)
<VAR>z : ℂ<GOAL>z.re = -abs z ↔ z ≤ 0
<VAR>e : ℂ → ℂ<VAR>e' : ℂ<VAR>z : ℝ<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℝ<VAR>u : ℝ<VAR>hf : HasDerivAt f u z<GOAL>HasDerivAt (fun y => ↑(f y)) (↑u) z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝ : MeasurableSpace α<VAR>j : JordanDecomposition α<VAR>r : ℝ<VAR>hr : 0 ≤ r<GOAL>(r • j).negPart = r.toNNReal • j.negPart
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : CommGroup G<VAR>a b c d : G<VAR>h : c * a = b<GOAL>a = b / c
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : NonPreadditiveAbelian C<VAR>X Y Z : C<VAR>f g : X ⟶ Y<VAR>h : Y ⟶ Z<GOAL>(f - g) ≫ h = f ≫ h - g ≫ h
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>hg' : g univ = ⊤<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>hg' : g univ = ⊤<VAR>h✝ : IsEmpty ι<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>f✝ f₁ f₂ : Filter α<VAR>g✝ g₁ g₂ : Set α → Filter β<VAR>f : ι → Filter α<VAR>g : Set α → Filter β<VAR>hg : ∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t<VAR>hg' : g univ = ⊤<VAR>h✝ : Nonempty ι<GOAL>(iInf f).lift g = ⨅ i, (f i).lift g
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.36631, u_1} C<VAR>inst✝⁸ : Category.{?u.36635, u_2} C₁<VAR>inst✝⁷ : Category.{?u.36639, u_3} C₂<VAR>inst✝⁶ : Category.{?u.36643, u_4} C₃<VAR>inst✝⁵ : Category.{?u.36647, u_5} D₁<VAR>inst✝⁴ : Category.{?u.36651, u_6} D₂<VAR>inst✝³ : Category.{?u.36655, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>(LocalizerMorphism.id W).homMap L₂ L₁ ((LocalizerMorphism.id W).homMap L₁ L₂ f) = f
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.36631, u_1} C<VAR>inst✝⁸ : Category.{?u.36635, u_2} C₁<VAR>inst✝⁷ : Category.{?u.36639, u_3} C₂<VAR>inst✝⁶ : Category.{?u.36643, u_4} C₃<VAR>inst✝⁵ : Category.{?u.36647, u_5} D₁<VAR>inst✝⁴ : Category.{?u.36651, u_6} D₂<VAR>inst✝³ : Category.{?u.36655, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>f : L₁.obj X ⟶ L₁.obj Y<GOAL>((LocalizerMorphism.id W).comp (LocalizerMorphism.id W)).homMap L₁ L₁ f = f
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.36631, u_1} C<VAR>inst✝⁸ : Category.{?u.36635, u_2} C₁<VAR>inst✝⁷ : Category.{?u.36639, u_3} C₂<VAR>inst✝⁶ : Category.{?u.36643, u_4} C₃<VAR>inst✝⁵ : Category.{?u.36647, u_5} D₁<VAR>inst✝⁴ : Category.{?u.36651, u_6} D₂<VAR>inst✝³ : Category.{?u.36655, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>g : L₂.obj X ⟶ L₂.obj Y<GOAL>(LocalizerMorphism.id W).homMap L₁ L₂ ((LocalizerMorphism.id W).homMap L₂ L₁ g) = g
<VAR>C : Type u_1<VAR>C₁ : Type u_2<VAR>C₂ : Type u_3<VAR>C₃ : Type u_4<VAR>D₁ : Type u_5<VAR>D₂ : Type u_6<VAR>D₃ : Type u_7<VAR>inst✝⁹ : Category.{?u.36631, u_1} C<VAR>inst✝⁸ : Category.{?u.36635, u_2} C₁<VAR>inst✝⁷ : Category.{?u.36639, u_3} C₂<VAR>inst✝⁶ : Category.{?u.36643, u_4} C₃<VAR>inst✝⁵ : Category.{?u.36647, u_5} D₁<VAR>inst✝⁴ : Category.{?u.36651, u_6} D₂<VAR>inst✝³ : Category.{?u.36655, u_7} D₃<VAR>W : MorphismProperty C<VAR>L₁ : C ⥤ D₁<VAR>inst✝² : L₁.IsLocalization W<VAR>L₂ : C ⥤ D₂<VAR>inst✝¹ : L₂.IsLocalization W<VAR>L₃ : C ⥤ D₃<VAR>inst✝ : L₃.IsLocalization W<VAR>X Y Z : C<VAR>g : L₂.obj X ⟶ L₂.obj Y<GOAL>((LocalizerMorphism.id W).comp (LocalizerMorphism.id W)).homMap L₂ L₂ g = g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>𝟭 (Subobject A) = lower e.functor ⋙ lower e.inverse
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>𝟭 (Subobject A) = ThinSkeleton.map (𝟭 (MonoOver A))
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>lower e.functor ⋙ lower e.inverse = ThinSkeleton.map (e.functor ⋙ e.inverse)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>lower e.inverse ⋙ lower e.functor = 𝟭 (Subobject B)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>lower e.inverse ⋙ lower e.functor = ThinSkeleton.map (e.inverse ⋙ e.functor)
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>X Y Z : C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>A : C<VAR>B : D<VAR>e : MonoOver A ≌ MonoOver B<GOAL>𝟭 (Subobject B) = ThinSkeleton.map (𝟭 (MonoOver B))
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<VAR>b0 : 0 < b<VAR>d0 : 0 < d<GOAL>a / b ≤ c / d ↔ a * d ≤ c * b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝³ : Preorder ι<VAR>inst✝² : TopologicalSpace α<VAR>inst✝¹ : Preorder α<VAR>inst✝ : SupConvergenceClass α<VAR>f : ι → α<VAR>a : α<VAR>h_anti : Antitone f<VAR>ha : IsLUB (range f) a<GOAL>Tendsto f atBot (𝓝 a)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<VAR>s : Set β<GOAL>(∀ᶠ (x : α × β) in f ×ˢ 𝓟 s, p x) ↔ ∀ᶠ (x : α) in f, ∀ y ∈ s, p (x, y)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Sort u_5<VAR>s✝ : Set α<VAR>t : Set β<VAR>f : Filter α<VAR>g : Filter β<VAR>p : α × β → Prop<VAR>s : Set β<GOAL>{a | ∀ b ∈ s, (a, b) ∈ {x | p x}} ∈ f ↔ {x | ∀ y ∈ s, p (x, y)} ∈ f
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>x : 𝕎 R<GOAL>(ghostComponent 0) x.verschiebungFun = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<GOAL>[l].join = l
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>a b : AddCircle T<VAR>h : a.toCircle = b.toCircle<GOAL>a = b
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>b : AddCircle T<VAR>z✝ : ℝ<VAR>h : toCircle ↑z✝ = b.toCircle<GOAL>↑z✝ = b
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : toCircle ↑z✝¹ = toCircle ↑z✝<GOAL>↑z✝¹ = ↑z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<GOAL>↑z✝¹ = ↑z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)<GOAL>↑z✝¹ = ↑z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)<GOAL>-z✝¹ + z✝ ∈ AddSubgroup.zmultiples T
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)<GOAL>∃ k, ↑k * T = -z✝¹ + z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π / T * z✝ = 2 * π / T * z✝¹ + ↑m * (2 * π)<GOAL>↑m * T = -z✝¹ + z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T<GOAL>↑m * T = -z✝¹ + z✝
<VAR>T : ℝ<VAR>hT : T ≠ 0<VAR>z✝¹ z✝ : ℝ<VAR>h : expMapCircle (2 * π / T * z✝¹) = expMapCircle (2 * π / T * z✝)<VAR>m : ℤ<VAR>hm : 2 * π * z✝ = 2 * π * z✝¹ + ↑m * (2 * π) * T<GOAL>2 * π * (↑m * T) = 2 * π * (-z✝¹ + z✝)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : InnerProductSpace 𝕜 E'<VAR>inst✝⁸ : CompleteSpace E'<VAR>inst✝⁷ : NormedSpace ℝ E'<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>one_le_p : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>μ : Measure α<VAR>hs : MeasurableSet s<VAR>hμs : (μ.trim hm) s ≠ ⊤<VAR>c : F<GOAL>↑↑↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c)) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)
<VAR>α : Type u_1<VAR>E' : Type u_2<VAR>F : Type u_3<VAR>F' : Type u_4<VAR>𝕜 : Type u_5<VAR>p : ℝ≥0∞<VAR>inst✝¹¹ : RCLike 𝕜<VAR>inst✝¹⁰ : NormedAddCommGroup E'<VAR>inst✝⁹ : InnerProductSpace 𝕜 E'<VAR>inst✝⁸ : CompleteSpace E'<VAR>inst✝⁷ : NormedSpace ℝ E'<VAR>inst✝⁶ : NormedAddCommGroup F<VAR>inst✝⁵ : NormedSpace 𝕜 F<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace 𝕜 F'<VAR>inst✝² : NormedSpace ℝ F'<VAR>inst✝¹ : CompleteSpace F'<VAR>m m0 : MeasurableSpace α<VAR>μ✝ : Measure α<VAR>one_le_p : Fact (1 ≤ p)<VAR>inst✝ : NormedSpace ℝ F<VAR>hm : m ≤ m0<VAR>s : Set α<VAR>μ : Measure α<VAR>hs : MeasurableSet s<VAR>hμs : (μ.trim hm) s ≠ ⊤<VAR>c : F<GOAL>↑↑(indicatorConstLp p hs hμs c) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : α → β<VAR>s t u : Finset α<VAR>a b : α<GOAL>_root_.Disjoint {a} s ↔ a ∉ s
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>∀ {x : A}, x ∈ T → x ∈ S ⊔ T
<VAR>F : Type v'<VAR>R' : Type u'<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>C : Type w'<VAR>inst✝¹⁶ : CommSemiring R<VAR>inst✝¹⁵ : StarRing R<VAR>inst✝¹⁴ : NonUnitalSemiring A<VAR>inst✝¹³ : StarRing A<VAR>inst✝¹² : Module R A<VAR>inst✝¹¹ : IsScalarTower R A A<VAR>inst✝¹⁰ : SMulCommClass R A A<VAR>inst✝⁹ : StarModule R A<VAR>inst✝⁸ : NonUnitalSemiring B<VAR>inst✝⁷ : StarRing B<VAR>inst✝⁶ : Module R B<VAR>inst✝⁵ : IsScalarTower R B B<VAR>inst✝⁴ : SMulCommClass R B B<VAR>inst✝³ : StarModule R B<VAR>inst✝² : FunLike F A B<VAR>inst✝¹ : NonUnitalAlgHomClass F R A B<VAR>inst✝ : NonUnitalStarAlgHomClass F R A B<VAR>S T : NonUnitalStarSubalgebra R A<GOAL>T ≤ S ⊔ T
<VAR>G : Type u_1<VAR>g₁ g₂ : Group G<VAR>h_mul : Mul.mul = Mul.mul<VAR>h₁ : One.one = One.one<VAR>f : G →* G := { toFun := id, map_one' := h₁, map_mul' := ⋯ }<GOAL>g₁ = g₂
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : Abelian C<VAR>S : SnakeInput C<GOAL>S.v₀₁.τ₃ ≫ S.v₁₂.τ₃ = 0
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<GOAL>x₁ = x₂
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<VAR>G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<VAR>G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ<VAR>disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<VAR>G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ<VAR>disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ<VAR>disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<VAR>G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ<VAR>disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ<VAR>disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)<VAR>hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ<GOAL>False
<VAR>X : Type u<VAR>inst✝⁷ : TopologicalSpace X<VAR>A D E : Type u<VAR>inst✝⁶ : TopologicalSpace A<VAR>inst✝⁵ : TopologicalSpace D<VAR>inst✝⁴ : TopologicalSpace E<VAR>inst✝³ : ExtremallyDisconnected A<VAR>inst✝² : T2Space A<VAR>inst✝¹ : T2Space E<VAR>inst✝ : CompactSpace E<VAR>ρ : E → A<VAR>ρ_cont : Continuous ρ<VAR>ρ_surj : Surjective ρ<VAR>zorn_subset : ∀ (E₀ : Set E), E₀ ≠ univ → IsClosed E₀ → ρ '' E₀ ≠ univ<VAR>x₁ x₂ : E<VAR>hρx : ρ x₁ = ρ x₂<VAR>hx : ¬x₁ = x₂<VAR>G₁ G₂ : Set E<VAR>G₁_open : IsOpen G₁<VAR>G₂_open : IsOpen G₂<VAR>hx₁ : x₁ ∈ G₁<VAR>hx₂ : x₂ ∈ G₂<VAR>disj : Disjoint G₁ G₂<VAR>G₁_comp : IsCompact G₁ᶜ<VAR>G₂_comp : IsCompact G₂ᶜ<VAR>G₁_open' : IsOpen (ρ '' G₁ᶜ)ᶜ<VAR>G₂_open' : IsOpen (ρ '' G₂ᶜ)ᶜ<VAR>disj' : Disjoint (ρ '' G₁ᶜ)ᶜ (ρ '' G₂ᶜ)ᶜ<VAR>disj'' : Disjoint (closure (ρ '' G₁ᶜ)ᶜ) (closure (ρ '' G₂ᶜ)ᶜ)<VAR>hx₁' : ρ x₁ ∈ closure (ρ '' G₁ᶜ)ᶜ<VAR>hx₂' : ρ x₂ ∈ closure (ρ '' G₂ᶜ)ᶜ<GOAL>False
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>ι : Sort u_1<VAR>u : ι → UniformSpace β<VAR>l : Filter β<VAR>inst✝ : l.NeBot<GOAL>Cauchy l ↔ ∀ (i : ι), Cauchy l
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<GOAL>∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖
<VAR>𝕜 : Type u_1<VAR>𝕜' : Type u_2<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜'<VAR>σ : 𝕜 →+* 𝕜'<VAR>σ' : 𝕜' →+* 𝕜<VAR>inst✝⁹ : RingHomInvPair σ σ'<VAR>inst✝⁸ : RingHomInvPair σ' σ<VAR>inst✝⁷ : RingHomIsometric σ<VAR>inst✝⁶ : RingHomIsometric σ'<VAR>E : Type u_3<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_4<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜' F<VAR>f : E →SL[σ] F<VAR>inst✝¹ : CompleteSpace F<VAR>inst✝ : CompleteSpace E<VAR>surj : Surjective ⇑f<VAR>C : ℝ<VAR>C0 : C ≥ 0<VAR>hC : ∀ (y : F), ∃ x, dist (f x) y ≤ 1 / 2 * ‖y‖ ∧ ‖x‖ ≤ C * ‖y‖<GOAL>∃ C > 0, ∀ (y : F), ∃ x, f x = y ∧ ‖x‖ ≤ C * ‖y‖