ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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<VAR>h : HasFTaylorSeriesUpTo n f p<GOAL>Continuous f
<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<VAR>h : HasFTaylorSeriesUpToOn n f p univ<GOAL>Continuous f
<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<VAR>h : HasFTaylorSeriesUpToOn n f p univ<GOAL>ContinuousOn f univ
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<GOAL>CompleteSpace ((n : ℕ) → E n)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<GOAL>∀ (u : ℕ → (n : ℕ) → E n), (∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N) → ∃ x, Tendsto u atTop (𝓝 x)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>u : ℕ → (n : ℕ) → E n<VAR>hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N<GOAL>∃ x, Tendsto u atTop (𝓝 x)
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>u : ℕ → (n : ℕ) → E n<VAR>hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N<VAR>i : ℕ<GOAL>Tendsto (fun i_1 => u i_1 i) atTop (𝓝 (u i i))
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>u : ℕ → (n : ℕ) → E n<VAR>hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N<VAR>i : ℕ<GOAL>(fun x => u i i) =ᶠ[atTop] fun i_1 => u i_1 i
<VAR>E : ℕ → Type u_1<VAR>inst✝¹ : (n : ℕ) → TopologicalSpace (E n)<VAR>inst✝ : ∀ (n : ℕ), DiscreteTopology (E n)<VAR>u : ℕ → (n : ℕ) → E n<VAR>hu : ∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < (fun n => (1 / 2) ^ n) N<VAR>i n : ℕ<VAR>hn : n ∈ Ici i<GOAL>u i i = u n i
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>inst✝ : AddGroup G<VAR>f : α →₀ G<VAR>a : α<VAR>b : G<GOAL>f.update a b = f - single a (f a) + single a b
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>A B : C<VAR>inst✝ : MonoCoprod C<VAR>c : BinaryCofan A B<VAR>hc : IsColimit c<GOAL>Mono c.inr
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>A B : C<VAR>inst✝ : MonoCoprod C<VAR>c : BinaryCofan A B<VAR>hc : IsColimit c<VAR>hc' : IsColimit (BinaryCofan.mk c.inr c.inl)<GOAL>Mono c.inr
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝ : Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>i : ι<GOAL>i ∈ l.splitSupport ↔ l.split i ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>M : Type u_5<VAR>M' : Type u_6<VAR>N : Type u_7<VAR>P : Type u_8<VAR>G : Type u_9<VAR>H : Type u_10<VAR>R : Type u_11<VAR>S : Type u_12<VAR>αs : ι → Type u_13<VAR>inst✝ : Zero M<VAR>l : (i : ι) × αs i →₀ M<VAR>i : ι<GOAL>(∃ a ∈ l.support, a.fst = i) ↔ ∃ x, x ∈ { support := l.support.preimage (Sigma.mk i) ⋯, toFun := fun a => l ⟨i, a⟩, mem_support_toFun := ⋯ }.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ s t : Set α<GOAL>(s \ t).encard + (s ∩ t).encard = s.encard
<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>x : A<GOAL>x ∈ ⊥.toNonUnitalSubalgebra ↔ x ∈ ⊥
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f g : α → β<VAR>c c₁ c₂ x : α<VAR>inst✝ : AddCommGroup α<VAR>h : Periodic f c<VAR>a : α<GOAL>Periodic (fun x => f (x - a)) c
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Sort w<VAR>κ : ι → Sort w'<VAR>inst✝ : Frame α<VAR>s t : Set α<VAR>a✝ b : α<VAR>f : (i : ι) → κ i → α<VAR>a : α<GOAL>(⨆ i, ⨆ j, f i j) ⊓ a = ⨆ i, ⨆ j, f i j ⊓ a
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁴ : Ring k<VAR>inst✝¹³ : AddCommGroup V1<VAR>inst✝¹² : AffineSpace V1 P1<VAR>inst✝¹¹ : AddCommGroup V2<VAR>inst✝¹⁰ : AffineSpace V2 P2<VAR>inst✝⁹ : AddCommGroup V3<VAR>inst✝⁸ : AffineSpace V3 P3<VAR>inst✝⁷ : Module k V1<VAR>inst✝⁶ : Module k V2<VAR>inst✝⁵ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁴ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝³ : (i : ι) → Module k (φv i)<VAR>inst✝² : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>h₂ : f 0 = g 0<GOAL>f = g
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁴ : Ring k<VAR>inst✝¹³ : AddCommGroup V1<VAR>inst✝¹² : AffineSpace V1 P1<VAR>inst✝¹¹ : AddCommGroup V2<VAR>inst✝¹⁰ : AffineSpace V2 P2<VAR>inst✝⁹ : AddCommGroup V3<VAR>inst✝⁸ : AffineSpace V3 P3<VAR>inst✝⁷ : Module k V1<VAR>inst✝⁶ : Module k V2<VAR>inst✝⁵ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁴ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝³ : (i : ι) → Module k (φv i)<VAR>inst✝² : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>h₂ : f 0 = g 0<GOAL>f.linear = g.linear
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁴ : Ring k<VAR>inst✝¹³ : AddCommGroup V1<VAR>inst✝¹² : AffineSpace V1 P1<VAR>inst✝¹¹ : AddCommGroup V2<VAR>inst✝¹⁰ : AffineSpace V2 P2<VAR>inst✝⁹ : AddCommGroup V3<VAR>inst✝⁸ : AffineSpace V3 P3<VAR>inst✝⁷ : Module k V1<VAR>inst✝⁶ : Module k V2<VAR>inst✝⁵ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁴ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝³ : (i : ι) → Module k (φv i)<VAR>inst✝² : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>h₂ : f 0 = g 0<GOAL>f ?p = g ?p
<VAR>R : Type u_1<VAR>k : Type u_2<VAR>V1 : Type u_3<VAR>P1 : Type u_4<VAR>V2 : Type u_5<VAR>P2 : Type u_6<VAR>V3 : Type u_7<VAR>P3 : Type u_8<VAR>inst✝¹⁴ : Ring k<VAR>inst✝¹³ : AddCommGroup V1<VAR>inst✝¹² : AffineSpace V1 P1<VAR>inst✝¹¹ : AddCommGroup V2<VAR>inst✝¹⁰ : AffineSpace V2 P2<VAR>inst✝⁹ : AddCommGroup V3<VAR>inst✝⁸ : AffineSpace V3 P3<VAR>inst✝⁷ : Module k V1<VAR>inst✝⁶ : Module k V2<VAR>inst✝⁵ : Module k V3<VAR>ι : Type u_9<VAR>φv : ι → Type u_10<VAR>φp : ι → Type u_11<VAR>inst✝⁴ : (i : ι) → AddCommGroup (φv i)<VAR>inst✝³ : (i : ι) → Module k (φv i)<VAR>inst✝² : (i : ι) → AffineSpace (φv i) (φp i)<VAR>fp : (i : ι) → P1 →ᵃ[k] φp i<VAR>fv : (i : ι) → P1 →ᵃ[k] φv i<VAR>f' : ι → P1 →ᵃ[k] P2<VAR>inst✝¹ : Finite ι<VAR>inst✝ : DecidableEq ι<VAR>f g : ((i : ι) → φv i) →ᵃ[k] P2<VAR>h : ∀ (i : ι) (x : φv i), f (Pi.single i x) = g (Pi.single i x)<VAR>h₂ : f 0 = g 0<GOAL>(i : ι) → φv i
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝² : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : CompactSpace α<GOAL>TendstoLocallyUniformly F f p ↔ TendstoUniformly F f p
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<GOAL>∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V<GOAL>∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>hU : ∀ (x : α), U x ∈ 𝓝 x ∧ ∀ᶠ (n : ι) in p, ∀ y ∈ U x, (f y, F n y) ∈ V<VAR>t : Finset ↑univ<VAR>ht : univ ⊆ ⋃ x ∈ t, U ↑x<GOAL>∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>t : Finset ↑univ<VAR>ht : univ ⊆ ⋃ x ∈ t, U ↑x<VAR>hU : ∀ (x : { x // x ∈ t }), ∀ᶠ (n : ι) in p, ∀ y ∈ U ↑↑x, (f y, F n y) ∈ V<GOAL>∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>t : Finset ↑univ<VAR>ht : univ ⊆ ⋃ x ∈ t, U ↑x<VAR>hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V<GOAL>∀ᶠ (n : ι) in p, ∀ (x : α), (f x, F n x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>t : Finset ↑univ<VAR>ht : univ ⊆ ⋃ x ∈ t, U ↑x<VAR>hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V<VAR>i : ι<VAR>hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V<VAR>x : α<GOAL>(f x, F i x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>t : Finset ↑univ<VAR>hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V<VAR>i : ι<VAR>hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V<VAR>x : α<VAR>ht : x ∈ ⋃ x ∈ t, U ↑x<GOAL>(f x, F i x) ∈ V
<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>inst✝ : CompactSpace α<VAR>h : TendstoLocallyUniformly F f p<VAR>V : Set (β × β)<VAR>hV : V ∈ 𝓤 β<VAR>U : α → Set α<VAR>t : Finset ↑univ<VAR>hU : ∀ᶠ (x : ι) in p, ∀ (i : { x // x ∈ t }), ∀ y ∈ U ↑↑i, (f y, F x y) ∈ V<VAR>i : ι<VAR>hi : ∀ (i_1 : { x // x ∈ t }), ∀ y ∈ U ↑↑i_1, (f y, F i y) ∈ V<VAR>x : α<VAR>ht : ∃ x_1, (∃ (x : x_1 ∈ univ), ⟨x_1, ⋯⟩ ∈ t) ∧ x ∈ U x_1<GOAL>(f x, F i x) ∈ V
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Semiring B<VAR>hB : IsField B<VAR>e : A ≃* B<VAR>x y : A<GOAL>e (x * y) = e (y * x)
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Semiring B<VAR>hB : IsField B<VAR>e : A ≃* B<VAR>a✝ : A<VAR>h : a✝ ≠ 0<GOAL>∃ b, a✝ * b = 1
<VAR>A : Type u_1<VAR>B : Type u_2<VAR>inst✝¹ : Semiring A<VAR>inst✝ : Semiring B<VAR>hB : IsField B<VAR>e : A ≃* B<VAR>a✝ : A<VAR>h : a✝ ≠ 0<VAR>a' : B<VAR>he : e a✝ * a' = 1<GOAL>∃ b, a✝ * b = 1
<VAR>α : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>P : Type u_4<VAR>R : Type u_5<VAR>S : Type u_6<VAR>inst✝⁹ : Semiring R<VAR>inst✝⁸ : Semiring S<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : AddCommMonoid N<VAR>inst✝⁴ : Module R N<VAR>inst✝³ : AddCommMonoid P<VAR>inst✝² : Module R P<VAR>α' : Type u_7<VAR>M' : Type u_8<VAR>inst✝¹ : AddCommMonoid M'<VAR>inst✝ : Module R M'<VAR>v✝ : α → M<VAR>v' : α' → M'<VAR>v : α → M<VAR>x : M<GOAL>x ∈ span R (Set.range v) ↔ ∃ c, (c.sum fun i a => a • v i) = x
<VAR>L : Type u<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>n✝ n : ℕ+<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R L<VAR>μ : L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>g : L ≃ₐ[R] L<GOAL>↑((autToPow R hμ) g) = ↑((ModularCyclotomicCharacter L ⋯) ↑g)
<VAR>L : Type u<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>n✝ n : ℕ+<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R L<VAR>μ : L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>g : L ≃ₐ[R] L<GOAL>(↑((autToPow R hμ) g)).val = (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val
<VAR>L : Type u<VAR>inst✝³ : CommRing L<VAR>inst✝² : IsDomain L<VAR>n✝ n : ℕ+<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>inst✝ : Algebra R L<VAR>μ : L<VAR>hμ : IsPrimitiveRoot μ ↑n<VAR>g : L ≃ₐ[R] L<GOAL>μ ^ (↑((autToPow R hμ) g)).val = μ ^ (↑((ModularCyclotomicCharacter L ⋯) ↑g)).val
<VAR>α : Type u<VAR>β✝ : Type v<VAR>ι : Sort w<VAR>γ : Type x<VAR>β : α → Type u_1<VAR>inst✝ : DecidableEq α<VAR>s : Finset ((a : α) × β a)<VAR>t : Finset α<VAR>x : (i : α) × β i<GOAL>(x ∈ t.sigma fun a => s.preimage (Sigma.mk a) ⋯) ↔ x ∈ filter (fun a => a.fst ∈ t) s
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝ : Inhabited Λ<VAR>M : Machine₀<VAR>S : Set Λ<VAR>ss : Supports M S<VAR>q : Λ<VAR>T : Tape Γ<VAR>c' : Cfg₀<VAR>h₁ : c' ∈ step M { q := q, Tape := T }<VAR>h₂ : { q := q, Tape := T }.q ∈ S<GOAL>c'.q ∈ S
<VAR>Γ : Type u_1<VAR>inst✝¹ : Inhabited Γ<VAR>Λ : Type u_2<VAR>inst✝ : Inhabited Λ<VAR>M : Machine₀<VAR>S : Set Λ<VAR>ss : Supports M S<VAR>q : Λ<VAR>T : Tape Γ<VAR>h₂ : { q := q, Tape := T }.q ∈ S<VAR>q' : Λ<VAR>a : Stmt₀<VAR>h : M q T.head = some (q', a)<VAR>h₁ : (match (q', a) with | (q', a) => { q := q', Tape := match a with | Stmt.move d => Tape.move d T | Stmt.write a => Tape.write a T }) ∈ step M { q := q, Tape := T }<GOAL>(match (q', a) with | (q', a) => { q := q', Tape := match a with | Stmt.move d => Tape.move d T | Stmt.write a => Tape.write a T }).q ∈ S
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>inst✝ : Nonempty ι<VAR>S : ι → Submodule R M<VAR>H : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>x ∈ iSup S ↔ ∃ i, x ∈ S i
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S✝ : Type u_7<VAR>inst✝⁸ : Semiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>x✝ : M<VAR>p p' : Submodule R M<VAR>inst✝⁵ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝⁴ : AddCommMonoid M₂<VAR>inst✝³ : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝² : FunLike F M M₂<VAR>inst✝¹ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>ι : Sort u_9<VAR>inst✝ : Nonempty ι<VAR>S : ι → Submodule R M<VAR>H : Directed (fun x x_1 => x ≤ x_1) S<VAR>x : M<GOAL>(∃ i, x ∈ ↑(S i)) ↔ ∃ i, x ∈ S i
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>ι : Type u_2<VAR>I : ι → TwoSidedIdeal R<VAR>x : R<GOAL>(∀ x_1 ∈ ringCon '' Set.range I, x_1 x 0) ↔ ∀ (i : ι), x ∈ I i
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>p q r : R[X]<VAR>a✝ : Subsingleton R<GOAL>(∀ (f g : R[X]), f = g) ∧ ∀ (a b : R), a = b
<GOAL>Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
<VAR>this : Tendsto eulerMascheroniSeq atTop (𝓝 (⨆ i, eulerMascheroniSeq i))<GOAL>Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)
<GOAL>BddAbove (Set.range eulerMascheroniSeq)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ i j k : ι<VAR>hk : P.root k = (P.reflection i) (P.root j)<GOAL>P.coroot k = (P.coreflection i) (P.coroot j)
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>N : Type u_4<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>P : RootPairing ι R M N<VAR>i✝ j✝ i j k : ι<VAR>hk : k = (P.reflection_perm i) j<GOAL>P.coroot k = (P.coreflection i) (P.coroot j)
<VAR>X Y : Scheme<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>IsAffineOpen (Scheme.Hom.opensRange f)
<VAR>X Y : Scheme<VAR>inst✝ : IsAffine X<VAR>f : X ⟶ Y<VAR>H : IsOpenImmersion f<GOAL>Set.range ⇑f.val.base = Set.range ⇑(Y.ofRestrict ⋯).val.base
<VAR>K : Type u_1<VAR>inst✝³ : Field K<VAR>inst✝² : NumberField K<VAR>inst✝¹ : IsCyclotomicExtension {3} ℚ K<VAR>ζ : K<VAR>hζ : IsPrimitiveRoot ζ ↑3<VAR>S : Solution hζ<VAR>S' : Solution' hζ<VAR>inst✝ : DecidableRel fun a b => a ∣ b<GOAL>∃ S₁, S₁.isMinimal
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s s₁ t u : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x x₀ : E<VAR>c : F<VAR>b : E × F → G<VAR>m n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>f₂ : 𝕜 → F<VAR>s₂ : Set 𝕜<VAR>n : ℕ<GOAL>ContDiff 𝕜 (↑(n + 1)) f₂ ↔ Differentiable 𝕜 f₂ ∧ ContDiff 𝕜 (↑n) (deriv f₂)
<VAR>R : Type u_1<VAR>inst✝⁸ : Semiring R<VAR>C : Type u_2<VAR>D : Type u_3<VAR>inst✝⁷ : Category.{u_4, u_2} C<VAR>inst✝⁶ : Category.{u_5, u_3} D<VAR>inst✝⁵ : Preadditive C<VAR>inst✝⁴ : Preadditive D<VAR>inst✝³ : CategoryTheory.Linear R C<VAR>inst✝² : CategoryTheory.Linear R D<VAR>F : C ⥤ D<VAR>inst✝¹ : F.Additive<VAR>inst✝ : Linear R F<VAR>X Y : C<VAR>r : Rˣ<VAR>f : X ⟶ Y<GOAL>F.map (r • f) = r • F.map f
<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>𝕜' : Type u_1<VAR>inst✝³ : NontriviallyNormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' F<VAR>inst✝ : IsScalarTower 𝕜 𝕜' F<VAR>s' t' : Set 𝕜'<VAR>h : 𝕜 → 𝕜'<VAR>h₁ : 𝕜 → 𝕜<VAR>h₂ : 𝕜' → 𝕜'<VAR>h' h₂' : 𝕜'<VAR>h₁' : 𝕜<VAR>g₁ : 𝕜' → F<VAR>g₁' : F<VAR>L' : Filter 𝕜'<VAR>y : 𝕜'<VAR>f : E → 𝕜'<VAR>f' : E →L[𝕜] 𝕜'<VAR>s : Set E<VAR>x : E<VAR>hh : HasDerivAt h₂ h₂' (f x)<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hy : y = f x<GOAL>HasFDerivWithinAt (h₂ ∘ f) (h₂' • f') s x
<VAR>S : Type u_1<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : IsDomain S<VAR>inst✝³ : Nontrivial S<VAR>inst✝² : IsDedekindDomain S<VAR>inst✝¹ : Module.Free ℤ S<VAR>inst✝ : Module.Finite ℤ S<VAR>I : Ideal S<GOAL>↑(absNorm I) ∈ I
<VAR>z x✝ y x r : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ (r / 2) = √x ^ r
<VAR>z x✝ y x r : ℝ<VAR>hx : 0 ≤ x<GOAL>x ^ (r / 2) = x ^ (1 / 2 * r)
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>t : TopologicalSpace α<VAR>inst✝² : PolishSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>AnalyticSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>t : TopologicalSpace α<VAR>inst✝² : PolishSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t' : TopologicalSpace α<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<GOAL>AnalyticSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>t : TopologicalSpace α<VAR>inst✝² : PolishSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t' : TopologicalSpace α<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<VAR>A : AnalyticSet s<GOAL>AnalyticSet s
<VAR>α✝ : Type u_1<VAR>ι : Type u_2<VAR>inst✝³ : TopologicalSpace α✝<VAR>α : Type u_3<VAR>t : TopologicalSpace α<VAR>inst✝² : PolishSpace α<VAR>inst✝¹ : MeasurableSpace α<VAR>inst✝ : BorelSpace α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t' : TopologicalSpace α<VAR>t't : t' ≤ t<VAR>t'_polish : PolishSpace α<VAR>s_closed : IsClosed s<VAR>right✝ : IsOpen s<VAR>A : AnalyticSet s<GOAL>s = id '' s
<VAR>ι : Type u_1<VAR>I J J₁ J₂ : Box ι<VAR>π✝ π₁ π₂ : Prepartition I<VAR>x : ι → ℝ<VAR>πi πi₁ πi₂ : (J : Box ι) → Prepartition J<VAR>π : Prepartition I<GOAL>π.IsPartition ↔ π.iUnion = ↑I
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>ι : Type x<VAR>inst✝¹ : UniformSpace β<VAR>F : ι → α → β<VAR>f : α → β<VAR>s s' : Set α<VAR>x✝ : α<VAR>p : Filter ι<VAR>p' : Filter α<VAR>g : ι → α<VAR>inst✝ : TopologicalSpace α<VAR>hs : IsOpen s<VAR>x : α<VAR>hx : x ∈ s<GOAL>Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝[s] x) (𝓤 β) ↔ Tendsto (fun y => (f y.2, F y.1 y.2)) (p ×ˢ 𝓝 x) (𝓤 β)
<VAR>α : Type u<VAR>β : Type v<VAR>ι : Type u_1<VAR>π : ι → Type u_2<VAR>inst✝ : TopologicalSpace α<VAR>s t u v : Set α<GOAL>LocallyConnectedSpace α ↔ ∀ (x : α), ∀ U ∈ 𝓝 x, ∃ V ⊆ U, IsOpen V ∧ x ∈ V ∧ IsConnected V