ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>c ∈ perpBisector p₁ p₂ ↔ ⟪(Equiv.pointReflection c) p₁ -ᵥ p₂, p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝³ : NormedAddCommGroup V<VAR>inst✝² : InnerProductSpace ℝ V<VAR>inst✝¹ : MetricSpace P<VAR>inst✝ : NormedAddTorsor V P<VAR>c c₁ c₂ p₁ p₂ : P<GOAL>2⁻¹ * ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫_ℝ = 0 ↔ ⟪c -ᵥ p₁ + (c -ᵥ p₂), p₂ -ᵥ p₁⟫_ℝ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Group α<VAR>inst✝ : Group β<VAR>f✝ : α → β<VAR>hf✝ : IsGroupHom f✝<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>h : Function.Injective f<VAR>x✝ : α<GOAL>f x✝ = 1 → x✝ = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Group α<VAR>inst✝ : Group β<VAR>f✝ : α → β<VAR>hf✝ : IsGroupHom f✝<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>h : Function.Injective f<VAR>x✝ : α<GOAL>f x✝ = f 1 → x✝ = 1
<VAR>α : Type u<VAR>β : Type v<VAR>inst✝¹ : Group α<VAR>inst✝ : Group β<VAR>f✝ : α → β<VAR>hf✝ : IsGroupHom f✝<VAR>f : α → β<VAR>hf : IsGroupHom f<VAR>h : ∀ (a : α), f a = 1 → a = 1<VAR>x y : α<VAR>hxy : f x = f y<GOAL>f (x / y) = 1
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>n : γ → δ<VAR>m' : β' → α' → δ<VAR>n₁ : β → β'<VAR>n₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)<GOAL>map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>γ' : Type u_6<VAR>δ : Type u_7<VAR>δ' : Type u_8<VAR>ε : Type u_9<VAR>ε' : Type u_10<VAR>m : α → β → γ<VAR>f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>h h₁ h₂ : Filter γ<VAR>s s₁ s₂ : Set α<VAR>t t₁ t₂ : Set β<VAR>u : Set γ<VAR>v : Set δ<VAR>a : α<VAR>b : β<VAR>c : γ<VAR>n : γ → δ<VAR>m' : β' → α' → δ<VAR>n₁ : β → β'<VAR>n₂ : α → α'<VAR>h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)<GOAL>map n (map₂ (fun a b => m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<GOAL>(if h : { byteIdx := utf8Len (c :: l) } = 0 then none else let_fun this := ⋯; let pos := { data := (c :: l).reverse ++ r }.prev { byteIdx := utf8Len (c :: l) }; if p ({ data := (c :: l).reverse ++ r }.get pos) = true then some pos else { data := (c :: l).reverse ++ r }.revFindAux p pos) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<GOAL>(let_fun this := ⋯; let pos := { data := (c :: l).reverse ++ r }.prev { byteIdx := utf8Len (c :: l) }; if p ({ data := (c :: l).reverse ++ r }.get pos) = true then some pos else { data := (c :: l).reverse ++ r }.revFindAux p pos) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<VAR>h1 : { data := l.reverse ++ c :: r }.get { byteIdx := utf8Len l.reverse } = (c :: r).headD default<GOAL>(let_fun this := ⋯; let pos := { data := (c :: l).reverse ++ r }.prev { byteIdx := utf8Len (c :: l) }; if p ({ data := (c :: l).reverse ++ r }.get pos) = true then some pos else { data := (c :: l).reverse ++ r }.revFindAux p pos) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<VAR>h1 : { data := l.reverse ++ c :: r }.get { byteIdx := utf8Len l.reverse } = (c :: r).headD default<VAR>h2 : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l.reverse + c.utf8Size } = { byteIdx := utf8Len l.reverse }<GOAL>(let_fun this := ⋯; let pos := { data := (c :: l).reverse ++ r }.prev { byteIdx := utf8Len (c :: l) }; if p ({ data := (c :: l).reverse ++ r }.get pos) = true then some pos else { data := (c :: l).reverse ++ r }.revFindAux p pos) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<VAR>h1 : { data := l.reverse ++ c :: r }.get { byteIdx := utf8Len l } = c<VAR>h2 : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }<GOAL>(let_fun this := ⋯; let pos := { data := (c :: l).reverse ++ r }.prev { byteIdx := utf8Len (c :: l) }; if p ({ data := (c :: l).reverse ++ r }.get pos) = true then some pos else { data := (c :: l).reverse ++ r }.revFindAux p pos) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<VAR>h1 : { data := l.reverse ++ c :: r }.get { byteIdx := utf8Len l } = c<VAR>h2 : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }<GOAL>(if p c = true then some { byteIdx := utf8Len l } else { data := l.reverse ++ c :: r }.revFindAux p { byteIdx := utf8Len l }) = Option.map (fun x => { byteIdx := utf8Len x }) (match !p c with | true => List.dropWhile (fun x => !p x) l | false => c :: l).tail?
<VAR>p : Char → Bool<VAR>c : Char<VAR>l r : List Char<VAR>h1 : { data := l.reverse ++ c :: r }.get { byteIdx := utf8Len l } = c<VAR>h2 : { data := l.reverse ++ c :: r }.prev { byteIdx := utf8Len l + c.utf8Size } = { byteIdx := utf8Len l }<GOAL>{ data := l.reverse ++ c :: r }.revFindAux p { byteIdx := utf8Len l } = Option.map (fun x => { byteIdx := utf8Len x }) (List.dropWhile (fun x => !p x) l).tail?
<VAR>F : Type u₀ → Type u₁ → Type u₂<VAR>inst✝¹ : Bifunctor F<VAR>inst✝ : LawfulBifunctor F<VAR>α₀ α₁ : Type u₀<VAR>β₀ β₁ : Type u₁<VAR>f : α₀ → α₁<VAR>f' : β₀ → β₁<VAR>x : F α₀ β₀<GOAL>fst f (snd f' x) = bimap f f' x
<VAR>R✝ : Type u_1<VAR>inst✝⁸ : CommRing R✝<VAR>S✝ : Submonoid R✝<VAR>P✝ : Type u_2<VAR>inst✝⁷ : CommRing P✝<VAR>inst✝⁶ : Algebra R✝ P✝<VAR>loc : IsLocalization S✝ P✝<VAR>R : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>S : Submonoid R<VAR>P : Type u_4<VAR>inst✝³ : Nontrivial P<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hR : IsNoetherianRing R<VAR>hS : S ≤ R⁰<VAR>I : FractionalIdeal S P<GOAL>(↑I).FG
<VAR>R✝ : Type u_1<VAR>inst✝⁸ : CommRing R✝<VAR>S✝ : Submonoid R✝<VAR>P✝ : Type u_2<VAR>inst✝⁷ : CommRing P✝<VAR>inst✝⁶ : Algebra R✝ P✝<VAR>loc : IsLocalization S✝ P✝<VAR>R : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>S : Submonoid R<VAR>P : Type u_4<VAR>inst✝³ : Nontrivial P<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hR : IsNoetherianRing R<VAR>hS : S ≤ R⁰<VAR>I : FractionalIdeal S P<VAR>this : FG I.num<GOAL>(↑I).FG
<VAR>R✝ : Type u_1<VAR>inst✝⁸ : CommRing R✝<VAR>S✝ : Submonoid R✝<VAR>P✝ : Type u_2<VAR>inst✝⁷ : CommRing P✝<VAR>inst✝⁶ : Algebra R✝ P✝<VAR>loc : IsLocalization S✝ P✝<VAR>R : Type u_3<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : Nontrivial R<VAR>S : Submonoid R<VAR>P : Type u_4<VAR>inst✝³ : Nontrivial P<VAR>inst✝² : CommRing P<VAR>inst✝¹ : Algebra R P<VAR>inst✝ : NoZeroSMulDivisors R P<VAR>hR : IsNoetherianRing R<VAR>hS : S ≤ R⁰<VAR>I : FractionalIdeal S P<VAR>this : ⊤.FG<GOAL>⊤.FG
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>hι : Nonempty ι<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a b : Ordinal.{max u v}<VAR>h : b ≤ nfpFamily f a<VAR>i : ι<GOAL>f i b ≤ nfpFamily f a
<VAR>ι : Type u<VAR>f✝ : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>hι : Nonempty ι<VAR>f : ι → Ordinal.{max u v} → Ordinal.{max u v}<VAR>H : ∀ (i : ι), IsNormal (f i)<VAR>a b : Ordinal.{max u v}<VAR>h : b ≤ nfpFamily f a<VAR>i : ι<GOAL>f i b ≤ f i (nfpFamily f a)
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : 𝓝[s \ {x}] x = ⊥<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<GOAL>derivWithin f s x ∈ closure ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<GOAL>∀ᶠ (x_1 : 𝕜) in 𝓝[(s ∩ t) \ {x}] x, slope f x x_1 ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<VAR>y : 𝕜<VAR>hy : y ∈ (s ∩ t) \ {x}<GOAL>slope f x y ∈ ↑(Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<VAR>y : 𝕜<VAR>hy : y ∈ (s ∩ t) \ {x}<GOAL>(y - x)⁻¹ • (f y - f x) ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<VAR>y : 𝕜<VAR>hy : y ∈ (s ∩ t) \ {x}<GOAL>f y ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f✝ f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x✝ : 𝕜<VAR>s✝ t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<VAR>x : 𝕜<VAR>H : (𝓝[s \ {x}] x).NeBot<VAR>H' : DifferentiableWithinAt 𝕜 f s x<VAR>I : (𝓝[(s ∩ t) \ {x}] x).NeBot<VAR>this : Tendsto (slope f x) (𝓝[(s ∩ t) \ {x}] x) (𝓝 (derivWithin f s x))<VAR>y : 𝕜<VAR>hy : y ∈ (s ∩ t) \ {x}<GOAL>f x ∈ (Submodule.span 𝕜 (f '' t)).topologicalClosure
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S✝<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>S : Set (NonUnitalSubring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>F : Type w<VAR>R : Type u<VAR>S✝ : Type v<VAR>T : Type u_1<VAR>inst✝⁴ : NonUnitalNonAssocRing R<VAR>inst✝³ : NonUnitalNonAssocRing S✝<VAR>inst✝² : NonUnitalNonAssocRing T<VAR>inst✝¹ : FunLike F R S✝<VAR>inst✝ : NonUnitalRingHomClass F R S✝<VAR>g : S✝ →ₙ+* T<VAR>f : R →ₙ+* S✝<VAR>S : Set (NonUnitalSubring R)<VAR>Sne : S.Nonempty<VAR>hS : DirectedOn (fun x x_1 => x ≤ x_1) S<VAR>x : R<VAR>this : Nonempty ↑S<GOAL>x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>hn : h ^ n ∈ Ideal.span {g}<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>hn : h ^ n * h ∈ Ideal.span {g}<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>hn : ∃ a, a * g = h ^ (n + 1)<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>∃ f g i, ↑x ∈ PrimeSpectrum.basicOpen g ∧ const R f g (PrimeSpectrum.basicOpen g) ⋯ = ((structureSheaf R).val.map i.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯ = ((structureSheaf R).val.map (i_basic_open ≫ iVU).op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯ = ((structureSheaf R).val.map iVU.op ≫ (structureSheaf R).val.map i_basic_open.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯ = ((structureSheaf R).val.map i_basic_open.op) (((structureSheaf R).val.map iVU.op) s)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>s : ↑((structureSheaf R).val.obj (op U))<VAR>x : ↥U<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : ↑x ∈ V.carrier<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hVDg : V ≤ PrimeSpectrum.basicOpen g<VAR>s_eq : const R f g V hVDg = ((structureSheaf R).val.map iVU.op) s<VAR>h : R<VAR>hxDh : ↑x ∈ (fun r => ↑(PrimeSpectrum.basicOpen r)) h<VAR>hDhV : PrimeSpectrum.basicOpen h ≤ V<VAR>n : ℕ<VAR>c : R<VAR>hc : c * g = h ^ (n + 1)<VAR>basic_opens_eq : PrimeSpectrum.basicOpen (h ^ (n + 1)) = PrimeSpectrum.basicOpen h<VAR>i_basic_open : PrimeSpectrum.basicOpen (h ^ (n + 1)) ⟶ V<GOAL>const R (f * c) (h ^ (n + 1)) (PrimeSpectrum.basicOpen (h ^ (n + 1))) ⋯ = const R f g (PrimeSpectrum.basicOpen (h ^ (n + 1))) ?right.hv