ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C X<VAR>x y : ↑X<VAR>h : x ⤳ y<VAR>j✝ : (OpenNhds (f y))ᵒᵖ<GOAL>colimit.ι (((whiskeringLeft (OpenNhds (f y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (f y)).op).obj ((pushforward C f).obj F)) j✝ ≫ ((pushforward C f).obj F).stalkSpecializes ⋯ ≫ colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F) ≫ colimit.pre (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (OpenNhds.map f x).op = colimit.ι (((whiskeringLeft (OpenNhds (f y))ᵒᵖ (Opens ↑Y)ᵒᵖ C).obj (OpenNhds.inclusion (f y)).op).obj ((pushforward C f).obj F)) j✝ ≫ (colim.map (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F) ≫ colimit.pre (((whiskeringLeft (OpenNhds y)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion y).op).obj F) (OpenNhds.map f y).op) ≫ F.stalkSpecializes h
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>inst✝ : HasColimits C<VAR>X Y Z : TopCat<VAR>f : X ⟶ Y<VAR>F : Presheaf C X<VAR>x y : ↑X<VAR>h : x ⤳ y<VAR>j✝ : (OpenNhds (f y))ᵒᵖ<GOAL>(whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f x).inv) F).app (op { obj := (unop j✝).obj, property := ⋯ }) ≫ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) ((OpenNhds.map f x).op.obj (op { obj := (unop j✝).obj, property := ⋯ })) = (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso f y).inv) F).app j✝ ≫ (Cocone.whisker (OpenNhds.map f y).op { pt := (stalkFunctor C x).toPrefunctor.1 F, ι := { app := fun U => colimit.ι ((OpenNhds.inclusion x).op ⋙ F) (op { obj := (unop U).obj, property := ⋯ }), naturality := ⋯ } }).ι.app j✝
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>toIocMod hp a (b + m • p) = toIocMod hp a b
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<VAR>m : ℤ<GOAL>b + m • p - (toIocDiv hp a b • p + m • p) = b - toIocDiv hp a b • p
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝ : Semiring R<VAR>p✝ p q : R[X]<VAR>ι : Type u_1<VAR>ha : a ≠ 0<GOAL>(C a * X + C b).leadingCoeff = a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>r a : R<GOAL>rootMultiplicity a (C r) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>r a : R<VAR>h✝ : Subsingleton R<GOAL>rootMultiplicity a (C r) = 0
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>A : Type z<VAR>a✝ b : R<VAR>n : ℕ<VAR>inst✝ : Ring R<VAR>p q : R[X]<VAR>r a : R<VAR>h✝ : Nontrivial R<GOAL>rootMultiplicity a (C r) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<VAR>i : ℕ<VAR>h : i < L.length<GOAL>drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.join) = L[i]
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>L : List (List α)<VAR>i : ℕ<VAR>h : i < L.length<VAR>this : take i (map length L) = take i (map length (take (i + 1) L))<GOAL>drop (Nat.sum (take i (map length L))) (take (Nat.sum (take (i + 1) (map length L))) L.join) = L[i]
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : ι → X<VAR>x : X<VAR>hf : Tendsto f cofinite (𝓝 x)<VAR>this : TopologicalSpace ι := ⊥<VAR>h : DiscreteTopology ι<GOAL>IsCompact (insert x (range f))
<VAR>X : Type u<VAR>Y : Type v<VAR>ι : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s t : Set X<VAR>f : ι → X<VAR>x : X<VAR>this : TopologicalSpace ι := ⊥<VAR>hf : Tendsto f (cocompact ι) (𝓝 x)<VAR>h : DiscreteTopology ι<GOAL>IsCompact (insert x (range f))
<VAR>x y : ℝ<GOAL>↑x < ↑y ↔ x < y
<VAR>α : Type u_1<VAR>t t₁ t₂ : TopologicalSpace α<VAR>s : Set α<VAR>inst✝ : TopologicalSpace α<GOAL>DiscreteTopology α ↔ ∀ (x : α), 𝓝 x = pure x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u✝ : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hs : MeasurableSet (Subtype.val ⁻¹' s)<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>MeasurableSet (inclusion h '' (Subtype.val ⁻¹' u))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u✝ : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hs : MeasurableSet (Subtype.val ⁻¹' s)<VAR>u : Set α<VAR>hu : MeasurableSet u<GOAL>inclusion h '' (Subtype.val ⁻¹' u) = Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>δ' : Type u_5<VAR>ι : Sort uι<VAR>s✝ t✝ u✝ : Set α<VAR>m : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>s t : Set α<VAR>h : s ⊆ t<VAR>hs : MeasurableSet (Subtype.val ⁻¹' s)<VAR>u : Set α<VAR>hu : MeasurableSet u<VAR>x : α<VAR>hx : x ∈ t<GOAL>⟨x, hx⟩ ∈ inclusion h '' (Subtype.val ⁻¹' u) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' u ∩ Subtype.val ⁻¹' s
<VAR>R S T : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>f : R →+* S<VAR>g : S →+* T<VAR>hf : f.FiniteType<VAR>hg : g.FiniteType<GOAL>(g.comp f).FiniteType
<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>ι : Type u_4<VAR>ι' : Type u_5<VAR>ι'' : Type u_6<VAR>E' : Type u_7<VAR>inst✝³ : NormedAddCommGroup E'<VAR>inst✝² : InnerProductSpace 𝕜 E'<VAR>E'' : Type u_8<VAR>inst✝¹ : NormedAddCommGroup E''<VAR>inst✝ : InnerProductSpace 𝕜 E''<VAR>v : Basis ι 𝕜 E<VAR>hv : Orthonormal 𝕜 ⇑v<VAR>v' : Basis ι' 𝕜 E'<VAR>hv' : Orthonormal 𝕜 ⇑v'<VAR>e : ι ≃ ι'<VAR>v'' : Basis ι'' 𝕜 E''<VAR>hv'' : Orthonormal 𝕜 ⇑v''<VAR>e' : ι' ≃ ι''<VAR>i : ι<GOAL>((hv.equiv hv' e).trans (hv'.equiv hv'' e')) (v i) = (hv.equiv hv'' (e.trans e')) (v i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>x : α<VAR>xs : List α<VAR>h : x ∈ xs<GOAL>map (fun y => s(x, y)) xs <+ xs.sym2
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x y : R<VAR>I : Ideal R<VAR>hqf : IsField (R ⧸ I)<GOAL>I.IsMaximal
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>I✝ : Ideal R<VAR>a b : R<VAR>S : Type v<VAR>x y : R<VAR>I : Ideal R<VAR>hqf : IsField (R ⧸ I)<GOAL>1 ∉ I ∧ ∀ (J : Ideal R) (x : R), I ≤ J → x ∉ I → x ∈ J → 1 ∈ J
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹⁰ : EMetricSpace X<VAR>inst✝⁹ : EMetricSpace Y<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>r✝ : 𝕜<VAR>hr : r✝ ≠ 0<VAR>s✝ : Set E<VAR>r : 𝕜<VAR>a✝ : r ≠ 0<VAR>s : Set E<GOAL>μH[d] (r • s) ≤ ‖r‖₊ ^ d • μH[d] s
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝¹⁰ : EMetricSpace X<VAR>inst✝⁹ : EMetricSpace Y<VAR>inst✝⁸ : MeasurableSpace X<VAR>inst✝⁷ : BorelSpace X<VAR>inst✝⁶ : MeasurableSpace Y<VAR>inst✝⁵ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>d : ℝ<VAR>hd : 0 ≤ d<VAR>r✝ : 𝕜<VAR>hr : r✝ ≠ 0<VAR>s✝ : Set E<VAR>r : 𝕜<VAR>a✝ : r ≠ 0<VAR>s : Set E<GOAL>μH[d] (r • s) ≤ ↑‖r‖₊ ^ d * μH[d] s
<VAR>L : Language<VAR>M : Type u_1<VAR>inst✝ : L.Structure M<GOAL>FG L M ↔ ∃ S, S.Finite ∧ (closure L).toFun S = ⊤
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>t : Set (PrimeSpectrum R)<VAR>f : R<GOAL>f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asIdeal
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α →ᵇ 𝕜<GOAL>⟪(BoundedContinuousFunction.toLp 2 μ 𝕜) f, (BoundedContinuousFunction.toLp 2 μ 𝕜) g⟫_𝕜 = ∫ (x : α), (starRingEnd 𝕜) (f x) * g x ∂μ
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α →ᵇ 𝕜<GOAL>(fun a => ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α →ᵇ 𝕜<VAR>hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<GOAL>(fun a => ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α →ᵇ 𝕜<VAR>hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<VAR>hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g<GOAL>(fun a => ⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a⟫_𝕜) =ᶠ[ae μ] fun a => (starRingEnd 𝕜) (f a) * g a
<VAR>α : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁴ : TopologicalSpace α<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : BorelSpace α<VAR>inst✝¹ : RCLike 𝕜<VAR>μ : Measure α<VAR>inst✝ : IsFiniteMeasure μ<VAR>f g : α →ᵇ 𝕜<VAR>hf_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) =ᶠ[ae μ] ⇑f<VAR>hg_ae : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) =ᶠ[ae μ] ⇑g<VAR>a✝ : α<VAR>hf : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝ = f a✝<VAR>hg : ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝ = g a✝<GOAL>⟪↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) f) a✝, ↑↑((BoundedContinuousFunction.toLp 2 μ 𝕜) g) a✝⟫_𝕜 = (starRingEnd 𝕜) (f a✝) * g a✝
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>a b x : α<VAR>h : (swap a b) x ≠ x<GOAL>x = a ∨ x = b
<VAR>α : Sort u_1<VAR>inst✝ : DecidableEq α<VAR>a b x : α<VAR>h : x ≠ a ∧ x ≠ b<GOAL>(swap a b) x = x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>a : α<VAR>hs : s ∈ 𝓝 (π a)<VAR>this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝<GOAL>π ⁻¹' s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : TopologicalSpace α<VAR>π : α → β<VAR>s : Set β<VAR>a : α<VAR>hs : s ∈ 𝓝 (π a)<VAR>this : TopologicalSpace β := TopologicalSpace.coinduced π inst✝<VAR>V : Set β<VAR>hVs : V ⊆ s<VAR>V_op : IsOpen V<VAR>mem_V : π a ∈ V<GOAL>π ⁻¹' s ∈ 𝓝 a
<VAR>α : Type u_1<VAR>inst✝ : CancelCommMonoidWithZero α<GOAL>WfDvdMonoid α → WellFounded fun x x_1 => x < x_1
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>x₀ : X'<VAR>k : κ<VAR>hk : EquicontinuousAt F x₀<GOAL>EquicontinuousAt F x₀
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>X : Type u_3<VAR>X' : Type u_4<VAR>Y : Type u_5<VAR>Z : Type u_6<VAR>α : Type u_7<VAR>α' : Type u_8<VAR>β : Type u_9<VAR>β' : Type u_10<VAR>γ : Type u_11<VAR>𝓕 : Type u_12<VAR>tX : TopologicalSpace X<VAR>tY : TopologicalSpace Y<VAR>tZ : TopologicalSpace Z<VAR>uα : UniformSpace α<VAR>uβ : UniformSpace β<VAR>uγ : UniformSpace γ<VAR>t : κ → TopologicalSpace X'<VAR>F : ι → X' → α<VAR>x₀ : X'<VAR>k : κ<VAR>hk : EquicontinuousWithinAt F univ x₀<GOAL>EquicontinuousWithinAt F univ x₀
<VAR>L : Type u_1<VAR>X : Type u_2<VAR>inst✝³ : TopologicalSpace L<VAR>inst✝² : TopologicalSpace X<VAR>ι : Type u_3<VAR>inst✝¹ : SemilatticeInf L<VAR>inst✝ : ContinuousInf L<VAR>s : Finset ι<VAR>f : ι → X → L<VAR>t : Set X<VAR>x : X<VAR>hne : s.Nonempty<VAR>hs : ∀ i ∈ s, ContinuousAt (f i) x<GOAL>ContinuousAt (s.inf' hne f) x
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi f<GOAL>Epi (G.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>this : Epi (F.map f ≫ (α.app Y).hom)<GOAL>Epi (G.map f)
<VAR>C : Type u₁<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝² : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>inst✝ : F.PreservesEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi f<VAR>this : Epi (F.map f ≫ (α.app Y).hom)<GOAL>G.map f = (α.app X).inv ≫ F.map f ≫ (α.app Y).hom
<VAR>E : Type u<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>Dense sᶜ
<VAR>E : Type u<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.Countable<GOAL>interior s = ∅
<VAR>E : Type u<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.Countable<VAR>H : ¬interior s = ∅<GOAL>False
<VAR>E : Type u<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : s.Countable<VAR>H : ¬interior s = ∅<GOAL>ℵ₀ < ℵ₀
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : (setOf p).Finite<VAR>n : ℕ<GOAL>count p n ≤ hp.toFinset.card
<VAR>p : ℕ → Prop<VAR>inst✝ : DecidablePred p<VAR>hp : (setOf p).Finite<VAR>n : ℕ<GOAL>(filter p (range n)).card ≤ hp.toFinset.card
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>H : P f<VAR>U : ↑Y.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ f ⁻¹ᵁ ↑U<GOAL>Q (Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>P : MorphismProperty Scheme<VAR>Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop<VAR>inst✝ : HasRingHomProperty P Q<VAR>X Y Z : Scheme<VAR>f : X ⟶ Y<VAR>g : Y ⟶ Z<VAR>H : ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U), Q (Scheme.Hom.appLE f (↑U) (↑V) e)<VAR>U : ↑Y.affineOpens<VAR>V : ↑X.affineOpens<VAR>e : ↑V ≤ f ⁻¹ᵁ ↑U<GOAL>Q (Scheme.Hom.appLE f (↑U) (↑V) e)
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>i : ι<GOAL>((fromEnd R b) f) (Pi.single i 1) = f (b i)
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>i : ι<GOAL>f (((Fintype.total R R) b) (Pi.single i 1)) = f (b i)
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>i : ι<GOAL>((Fintype.total R R) b) (Pi.single i 1) = b i
<VAR>ι : Type u_1<VAR>inst✝⁴ : Fintype ι<VAR>M : Type u_2<VAR>inst✝³ : AddCommGroup M<VAR>R : Type u_3<VAR>inst✝² : CommRing R<VAR>inst✝¹ : Module R M<VAR>I : Ideal R<VAR>b : ι → M<VAR>hb : Submodule.span R (Set.range b) = ⊤<VAR>inst✝ : DecidableEq ι<VAR>f : Module.End R M<VAR>i : ι<GOAL>b i = 1 • b i
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hsg : t = generateFrom s<VAR>hsi : FiniteInter s<GOAL>IsTopologicalBasis s
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hsg : t = generateFrom s<VAR>hsi : FiniteInter s<GOAL>s = (fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s}
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hsg : t = generateFrom s<VAR>hsi : FiniteInter s<GOAL>(fun f => ⋂₀ f) '' {f | f.Finite ∧ f ⊆ s} ≤ s
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s✝ : Set α<VAR>s : Set (Set α)<VAR>hsg : t = generateFrom s<VAR>hsi : FiniteInter s<VAR>g : Finset (Set α)<VAR>hgs : ↑g ⊆ s<GOAL>(fun f => ⋂₀ f) ↑g ∈ s
<VAR>R : Type u<VAR>inst✝³ : Semiring R<VAR>inst✝² : RankCondition R<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Fintype β<VAR>f : (α → R) →ₗ[R] β → R<VAR>i : Surjective ⇑f<VAR>P : (Fin (Fintype.card α) → R) ≃ₗ[R] α → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)<VAR>Q : (Fin (Fintype.card β) → R) ≃ₗ[R] β → R := LinearEquiv.funCongrLeft R R (Fintype.equivFin β)<GOAL>Fintype.card β ≤ Fintype.card α
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>Ico a b - Ico c b = Ico a (min b c)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>s t u v : Finset α<VAR>a b : α<VAR>h : a ∈ t<GOAL>s.erase a ⊆ t ↔ s ⊆ t
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<GOAL>a ≤ b ↔ a < b ∨ a = b
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t x✝¹ x✝ : V<GOAL>(edge s s).Adj x✝¹ x✝ ↔ ⊥.Adj x✝¹ x✝
<VAR>V : Type u_1<VAR>inst✝ : DecidableEq V<VAR>G : SimpleGraph V<VAR>s t x✝¹ x✝ : V<GOAL>(x✝¹ = s ∧ x✝ = s ∨ x✝¹ = s ∧ x✝ = s) ∧ x✝¹ ≠ x✝ ↔ ⊥.Adj x✝¹ x✝
<VAR>m n k : ℤ<GOAL>(m * n).lcm (k * n) = m.lcm k * n.natAbs
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f f' : 𝕜 → G<VAR>s : Set 𝕜<VAR>x✝ y✝ : 𝕜<VAR>hf : Differentiable 𝕜 f<VAR>hf' : ∀ (x : 𝕜), deriv f x = 0<VAR>x y z : 𝕜<GOAL>(fderiv 𝕜 f z) 1 = 0 1
<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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<GOAL>ContinuousWithinAt f 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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<VAR>t : Set α<VAR>tx : t ∈ 𝓝[s] x<VAR>F : α → β<VAR>hFc : ContinuousWithinAt F s x<VAR>hF : ∀ y ∈ t, (f y, F y) ∈ u₂<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<VAR>t : Set α<VAR>tx : t ∈ 𝓝[s] x<VAR>F : α → β<VAR>hFc : ContinuousWithinAt F s x<VAR>hF : ∀ y ∈ t, (f y, F y) ∈ u₂<VAR>A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[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 α<VAR>hx : x ∈ s<VAR>L : ∀ u ∈ 𝓤 β, ∃ t ∈ 𝓝[s] x, ∃ F, ContinuousWithinAt F s x ∧ ∀ y ∈ t, (f y, F y) ∈ u<VAR>u₀ : Set (β × β)<VAR>hu₀ : u₀ ∈ 𝓤 β<VAR>u₁ : Set (β × β)<VAR>h₁ : u₁ ∈ 𝓤 β<VAR>u₁₀ : u₁ ○ u₁ ⊆ u₀<VAR>u₂ : Set (β × β)<VAR>h₂ : u₂ ∈ 𝓤 β<VAR>hsymm : ∀ {a b : β}, (a, b) ∈ u₂ → (b, a) ∈ u₂<VAR>u₂₁ : u₂ ○ u₂ ⊆ u₁<VAR>t : Set α<VAR>tx : t ∈ 𝓝[s] x<VAR>F : α → β<VAR>hFc : ContinuousWithinAt F s x<VAR>hF : ∀ y ∈ t, (f y, F y) ∈ u₂<VAR>A : ∀ᶠ (y : α) in 𝓝[s] x, (f y, F y) ∈ u₂<VAR>B : ∀ᶠ (y : α) in 𝓝[s] x, (F y, F x) ∈ u₂<GOAL>u₀ ∈ map (fun x_1 => (f x_1, f x)) (𝓝[s] x)