ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>f : α → Option α<VAR>a : α<VAR>l : List α<VAR>h : f a = none<GOAL>(match none with | some b => b :: l | none => (#[].push a).toListAppend (lookmap f l)) = a :: lookmap.go f l #[]
<VAR>G : Type u_1<VAR>G' : Type u_2<VAR>G'' : Type u_3<VAR>inst✝⁴ : Group G<VAR>inst✝³ : Group G'<VAR>inst✝² : Group G''<VAR>A : Type u_4<VAR>inst✝¹ : AddGroup A<VAR>N : Type u_5<VAR>inst✝ : Group N<VAR>f✝ f : G →* N<VAR>g : N →* G<VAR>hl : LeftInverse ⇑g ⇑f<VAR>hr : Function.RightInverse ⇑g ⇑f<VAR>H : Subgroup G<GOAL>↑(map f H) = ↑(comap g H)
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<VAR>h : l.rotate n = l'.rotate n<GOAL>l = l'
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<VAR>h : l.rotate n = l'.rotate n<VAR>hle : l.length = l'.length<GOAL>l = l'
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<VAR>h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'<VAR>hle : l.length = l'.length<GOAL>l = l'
<VAR>α : Type u<VAR>n : ℕ<VAR>l l' : List α<VAR>h : drop (n % l.length) l ++ take (n % l.length) l = drop (n % l'.length) l' ++ take (n % l'.length) l'<VAR>hle : l.length = l'.length<VAR>hd : drop (n % l.length) l = drop (n % l'.length) l'<VAR>ht : take (n % l.length) l = take (n % l'.length) l'<GOAL>l = l'
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List ι<VAR>i : ℕ<VAR>h : i < l.length<GOAL>(l.eraseIdx i).length + 1 = (take i l ++ drop (i + 1) l).length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List ι<VAR>i : ℕ<VAR>h : i < l.length<GOAL>(take i l ++ drop (i + 1) l).length + 1 = (take i l).length + (drop (i + 1) l).length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List ι<VAR>i : ℕ<VAR>h : i < l.length<GOAL>(take i l).length + (drop (i + 1) l).length + 1 = i + (drop (i + 1) l).length + 1
<VAR>ι : Type u_1<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ l₂ : List α<VAR>inst✝ : DecidableEq α<VAR>l : List ι<VAR>i : ℕ<VAR>h : i < l.length<GOAL>i + (drop (i + 1) l).length + 1 = i + (l.length - (i + 1)) + 1
<VAR>p : ℕ<VAR>inst✝ : Fact (Nat.Prime p)<VAR>F : Polynomial ℤ_[p]<VAR>a : ℤ_[p]<VAR>hnorm : ‖Polynomial.eval a F‖ < ‖Polynomial.eval a (Polynomial.derivative F)‖ ^ 2<VAR>hnsol : Polynomial.eval a F ≠ 0<VAR>n : ℕ<GOAL>‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval (newton_seq n) (Polynomial.derivative F)‖ = ‖Polynomial.eval (newton_seq n) F‖ / ‖Polynomial.eval a (Polynomial.derivative F)‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : μ s < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * (μ s).toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : (μ.restrict s) univ < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝² : MeasurableSpace X<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>f g : X → E<VAR>s t : Set X<VAR>μ ν : Measure X<VAR>l l' : Filter X<VAR>C : ℝ<VAR>hs : (μ.restrict s) univ < ⊤<VAR>hC : ∀ᵐ (x : X) ∂μ.restrict s, ‖f x‖ ≤ C<VAR>this : IsFiniteMeasure (μ.restrict s)<GOAL>‖∫ (x : X) in s, f x ∂μ‖ ≤ C * ((μ.restrict s) univ).toReal
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : DecidableEq α<VAR>l l' : List α<VAR>a : α<VAR>n : l.Nodup<GOAL>(↑l).Nodup
<VAR>R : Type u<VAR>S₁ : Type v<VAR>S₂ : Type w<VAR>S₃ : Type x<VAR>σ : Type u_1<VAR>a a' a₁ a₂ : R<VAR>e : ℕ<VAR>n✝ m : σ<VAR>s✝ : σ →₀ ℕ<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S₁<VAR>p q : MvPolynomial σ R<VAR>inst✝ : Nontrivial R<VAR>s : σ<VAR>n : ℕ<GOAL>(X s ^ n).support = {Finsupp.single s n}
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = minpoly G F x<GOAL>f = 1 ∨ g = 1
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = minpoly G F x<VAR>hf2 : f ∣ minpoly G F x<GOAL>f = 1 ∨ g = 1
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = minpoly G F x<VAR>hf2 : f ∣ minpoly G F x<VAR>hg2 : g ∣ minpoly G F x<GOAL>f = 1 ∨ g = 1
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = minpoly G F x<VAR>hf2 : f ∣ minpoly G F x<VAR>hg2 : g ∣ minpoly G F x<VAR>this : Polynomial.eval₂ (subfield G F).subtype x (minpoly G F x) = 0<GOAL>f = 1 ∨ g = 1
<VAR>M : Type u<VAR>inst✝⁵ : Monoid M<VAR>G : Type u<VAR>inst✝⁴ : Group G<VAR>F : Type v<VAR>inst✝³ : Field F<VAR>inst✝² : MulSemiringAction M F<VAR>inst✝¹ : MulSemiringAction G F<VAR>m : M<VAR>inst✝ : Fintype G<VAR>x : F<VAR>f g : Polynomial ↥(subfield G F)<VAR>hf : f.Monic<VAR>hg : g.Monic<VAR>hfg : f * g = minpoly G F x<VAR>hf2 : f ∣ minpoly G F x<VAR>hg2 : g ∣ minpoly G F x<VAR>this : Polynomial.eval₂ (subfield G F).subtype x f = 0 ∨ Polynomial.eval₂ (subfield G F).subtype x g = 0<GOAL>f = 1 ∨ g = 1
<VAR>s : ℝ<VAR>hs : 0 < s<GOAL>s.doublingGamma = Gamma s
<VAR>s : ℝ<VAR>hs : 0 < s<VAR>y : ℝ<VAR>hy : 0 < y<GOAL>0 < y.doublingGamma
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<GOAL>HasDerivAt cexp (cexp x) x
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<GOAL>(fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<VAR>this : 1 < 2<GOAL>(fun h => cexp (x + h) - cexp x - h • cexp x) =o[𝓝 0] fun h => h
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<VAR>this : 1 < 2<GOAL>∀ᶠ (x_1 : ℂ) in 𝓝 0, ‖cexp (x + x_1) - cexp x - x_1 • cexp x‖ ≤ ‖cexp x‖ * ‖x_1 ^ 2‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<VAR>this : 1 < 2<GOAL>∀ a ∈ Metric.ball 0 1, ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a ^ 2‖
<VAR>𝕜 : Type u_1<VAR>inst✝¹ : NontriviallyNormedField 𝕜<VAR>inst✝ : NormedAlgebra 𝕜 ℂ<VAR>x : ℂ<VAR>this : 1 < 2<GOAL>∀ (a : ℂ), ‖a‖ < 1 → ‖cexp (x + a) - cexp x - a • cexp x‖ ≤ ‖cexp x‖ * ‖a‖ ^ 2
<VAR>ι : Type u_1<VAR>α : ι → Type u_2<VAR>β✝ : ι → Type u_3<VAR>s s₁ s₂ : Set ι<VAR>t✝ t₁ t₂ : (i : ι) → Set (α i)<VAR>i✝ : ι<VAR>inst✝ : DecidableEq ι<VAR>β : ι → Type u_4<VAR>i : ι<VAR>f : (j : ι) → α j<VAR>a : α i<VAR>t : (j : ι) → α j → Set (β j)<GOAL>(univ.pi fun j => t j (update f i a j)) = {x | x i ∈ t i a} ∩ {i}ᶜ.pi fun j => t j (f j)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>ht : μ (s \ t) = 0<GOAL>μ (s ∩ t) = μ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>ι : Type u_5<VAR>R : Type u_6<VAR>R' : Type u_7<VAR>m : MeasurableSpace α<VAR>μ μ₁ μ₂ : Measure α<VAR>s s₁ s₂ t : Set α<VAR>ht : μ (s \ t) = 0<GOAL>μ (s ∩ tᶜ) = 0
<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>f₁ f₁' : α₁ → β₁ → Finset γ₁<VAR>f₂ f₂' : α₂ → β₂ → Finset γ₂<VAR>g₁ g₁' : α₁ → β₂ → Finset γ₁<VAR>g₂ g₂' : α₁ → β₂ → Finset γ₂<VAR>a : α₁ ⊕ α₂<VAR>b : β₁ ⊕ β₂<VAR>c : γ₁ ⊕ γ₂<VAR>c₂ : γ₂<GOAL>inr c₂ ∈ sumLexLift f₁ f₂ g₁ g₂ a b ↔ (∃ a₁ b₂, a = inl a₁ ∧ b = inr b₂ ∧ c₂ ∈ g₂ a₁ b₂) ∨ ∃ a₂ b₂, a = inr a₂ ∧ b = inr b₂ ∧ c₂ ∈ f₂ a₂ b₂
<VAR>R✝ : Type u_1<VAR>inst✝³ : AddMonoidWithOne R✝<VAR>p✝ a✝ b✝ : ℕ<VAR>R : Type u_1<VAR>inst✝² : AddMonoidWithOne R<VAR>p : ℕ<VAR>inst✝¹ : CharP R p<VAR>a b : ℕ<VAR>inst✝ : IsRightCancelAdd R<VAR>hle : a ≤ b<GOAL>↑a = ↑b ↔ a ≡ b [MOD p]
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>α : Type u_3<VAR>inst✝³ : NormedRing E<VAR>inst✝² : StarRing E<VAR>inst✝¹ : CstarRing E<VAR>inst✝ : Nontrivial E<VAR>U : ↥(unitary E)<GOAL>‖↑U‖ = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>F : Type u_3<VAR>inst✝¹ : FunLike F (Set α) ℝ≥0∞<VAR>inst✝ : OuterMeasureClass F α<VAR>μ : F<VAR>s✝ t s : Set α<GOAL>sᶜ ∈ ae μ ↔ μ s = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>p : PMF α<VAR>s : Set α<VAR>h : ∃ a ∈ s, a ∈ p.support<VAR>a : α<GOAL>(p.filter s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ p.support
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Icc (inlₗ a₁) (inlₗ a₂) = map (Embedding.inl.trans toLex.toEmbedding) (Icc a₁ a₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝⁵ : Preorder α<VAR>inst✝⁴ : Preorder β<VAR>inst✝³ : OrderTop α<VAR>inst✝² : OrderBot β<VAR>inst✝¹ : LocallyFiniteOrder α<VAR>inst✝ : LocallyFiniteOrder β<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<GOAL>Icc (inlₗ a₁) (inlₗ a₂) = map toLex.toEmbedding (map Embedding.inl (Icc a₁ a₂))
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : ℤ → R<VAR>f : R →+* S<VAR>b c d : R<VAR>n : ℤ<GOAL>normEDS b c d (-n) = -normEDS b c d n
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<GOAL>MeasurableSet {x | DifferentiableAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<VAR>this : IsComplete univ<GOAL>MeasurableSet {x | DifferentiableAt 𝕜 f x}
<VAR>𝕜 : Type u_1<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝⁴ : NormedAddCommGroup F<VAR>inst✝³ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>K : Set (E →L[𝕜] F)<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>inst✝ : CompleteSpace F<VAR>this : IsComplete univ<VAR>x✝ : E<GOAL>DifferentiableAt 𝕜 f x✝ ↔ DifferentiableAt 𝕜 f x✝ ∧ fderiv 𝕜 f x✝ ∈ univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>f : α → ℝ≥0∞<VAR>A B : Set α<VAR>hB : MeasurableSet B<VAR>hAB : Disjoint A B<GOAL>∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ
<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✝ : TopologicalSpace γ<VAR>t : Set γ<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>g : γ → α<VAR>hg : MapsTo g t s<VAR>cg : ContinuousOn g t<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : γ<VAR>hx : x ∈ t<VAR>a : Set α<VAR>ha : a ∈ 𝓝[s] g x<VAR>H : ∀ᶠ (n : ι) in p, ∀ y ∈ a, (f y, F n y) ∈ u<GOAL>∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
<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✝ : TopologicalSpace γ<VAR>t : Set γ<VAR>h : TendstoLocallyUniformlyOn F f p s<VAR>g : γ → α<VAR>hg : MapsTo g t s<VAR>cg : ContinuousOn g t<VAR>u : Set (β × β)<VAR>hu : u ∈ 𝓤 β<VAR>x : γ<VAR>hx : x ∈ t<VAR>a : Set α<VAR>ha : a ∈ 𝓝[s] g x<VAR>H : ∀ᶠ (n : ι) in p, ∀ y ∈ a, (f y, F n y) ∈ u<VAR>this : g ⁻¹' a ∈ 𝓝[t] x<GOAL>∃ t_1 ∈ 𝓝[t] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t_1, ((f ∘ g) y, (fun n => F n ∘ g) n y) ∈ u
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<GOAL>WithSeminorms p ↔ 𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕝 : Type u_3<VAR>𝕝₂ : Type u_4<VAR>E : Type u_5<VAR>F : Type u_6<VAR>G : Type u_7<VAR>ι : Type u_8<VAR>ι' : Type u_9<VAR>inst✝⁴ : NormedField 𝕜<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : Nonempty ι<VAR>t : TopologicalSpace E<VAR>inst✝ : TopologicalAddGroup E<VAR>p : SeminormFamily 𝕜 E ι<VAR>h : WithSeminorms p<GOAL>𝓝 0 = AddGroupFilterBasis.toFilterBasis.filter
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>k : K<VAR>q : TM1.Stmt Γ' Λ' σ<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse<VAR>o : StAct k<GOAL>let v' := stVar v (S k) o; let Sk' := stWrite v (S k) o; let S' := update S k Sk'; ∃ L', (∀ (k : K), ListBlank.map (proj k) L' = ListBlank.mk (List.map some (S' k)).reverse) ∧ TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) = TM1.stepAux q v' ((Tape.move Dir.right)^[(S' k).length] (Tape.mk' ∅ (addBottom L')))
<VAR>K : Type u_1<VAR>inst✝² : DecidableEq K<VAR>Γ : K → Type u_2<VAR>Λ : Type u_3<VAR>inst✝¹ : Inhabited Λ<VAR>σ : Type u_4<VAR>inst✝ : Inhabited σ<VAR>k : K<VAR>q : TM1.Stmt Γ' Λ' σ<VAR>v : σ<VAR>S : (k : K) → List (Γ k)<VAR>L : ListBlank ((k : K) → Option (Γ k))<VAR>hL : ∀ (k : K), ListBlank.map (proj k) L = ListBlank.mk (List.map some (S k)).reverse<VAR>o : StAct k<GOAL>∃ L', (∀ (k_1 : K), ListBlank.map (proj k_1) L' = ListBlank.mk (List.map some (update S k (stWrite v (S k) o) k_1)).reverse) ∧ TM1.stepAux (trStAct q o) v ((Tape.move Dir.right)^[(S k).length] (Tape.mk' ∅ (addBottom L))) = TM1.stepAux q (stVar v (S k) o) ((Tape.move Dir.right)^[(stWrite v (S k) o).length] (Tape.mk' ∅ (addBottom L')))
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : IsClosedMap g<VAR>hf : IsClosedMap f<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (g ∘ f '' s)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>ι : Type u_4<VAR>f : X → Y<VAR>g : Y → Z<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>inst✝ : TopologicalSpace Z<VAR>hg : IsClosedMap g<VAR>hf : IsClosedMap f<VAR>s : Set X<VAR>hs : IsClosed s<GOAL>IsClosed (g '' (f '' s))
<VAR>α : Type u<VAR>L L₁ L₂ L₃ L₄ L1 L2 : List (α × Bool)<VAR>x : α<VAR>b : Bool<GOAL>sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h' : DenseRange ⇑f'<GOAL>UniqueDiffWithinAt 𝕜 (f '' s) (f x)
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h' : DenseRange ⇑f'<GOAL>MapsTo ⇑f' ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 s x)) ↑(Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h' : DenseRange ⇑f'<GOAL>Submodule.span 𝕜 (tangentConeAt 𝕜 s x) ≤ Submodule.comap f' (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x)))
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h' : DenseRange ⇑f'<GOAL>tangentConeAt 𝕜 s x ⊆ ↑(Submodule.comap f' (Submodule.span 𝕜 (tangentConeAt 𝕜 (f '' s) (f x))))
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : LinearOrderedRing α<VAR>inst✝ : FloorRing α<VAR>z : ℤ<VAR>a✝ a : α<GOAL>⌈a - 1⌉ = ⌈a⌉ - 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>E : Type u_4<VAR>Eₗ : Type u_5<VAR>F : Type u_6<VAR>Fₗ : Type u_7<VAR>G : Type u_8<VAR>Gₗ : Type u_9<VAR>𝓕 : Type u_10<VAR>inst✝¹⁸ : SeminormedAddCommGroup E<VAR>inst✝¹⁷ : SeminormedAddCommGroup Eₗ<VAR>inst✝¹⁶ : SeminormedAddCommGroup F<VAR>inst✝¹⁵ : SeminormedAddCommGroup Fₗ<VAR>inst✝¹⁴ : SeminormedAddCommGroup G<VAR>inst✝¹³ : SeminormedAddCommGroup Gₗ<VAR>inst✝¹² : NontriviallyNormedField 𝕜<VAR>inst✝¹¹ : NontriviallyNormedField 𝕜₂<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜₃<VAR>inst✝⁹ : NormedSpace 𝕜 E<VAR>inst✝⁸ : NormedSpace 𝕜 Eₗ<VAR>inst✝⁷ : NormedSpace 𝕜₂ F<VAR>inst✝⁶ : NormedSpace 𝕜 Fₗ<VAR>inst✝⁵ : NormedSpace 𝕜₃ G<VAR>inst✝⁴ : NormedSpace 𝕜 Gₗ<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>σ₁₃ : 𝕜 →+* 𝕜₃<VAR>inst✝³ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃<VAR>inst✝² : FunLike 𝓕 E F<VAR>inst✝¹ : RingHomIsometric σ₁₂<VAR>inst✝ : RingHomIsometric σ₂₃<VAR>f✝ g : E →SL[σ₁₂] F<VAR>h : F →SL[σ₂₃] G<VAR>x✝ : E<VAR>f : E →SL[σ₁₂] F<VAR>M : ℝ≥0<VAR>hM : ∀ (x : E), ‖x‖₊ ≠ 0 → ‖f x‖₊ ≤ M * ‖x‖₊<VAR>x : E<VAR>hx : ‖x‖ ≠ 0<GOAL>‖x‖₊ ≠ 0
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>S₀ : Subalgebra R S<VAR>M : Submonoid ↥S₀<VAR>left✝ : FiniteType R ↥S₀<VAR>right✝ : IsLocalization M S<GOAL>EssFiniteType R S
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : CommRing T<VAR>inst✝³ : Algebra R S<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>S₀ : Subalgebra R S<VAR>M : Submonoid ↥S₀<VAR>left✝ : FiniteType R ↥S₀<VAR>right✝ : IsLocalization M S<VAR>this : EssFiniteType (↥S₀) S := of_isLocalization S M<GOAL>EssFiniteType R S
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : Type u_3<VAR>n : Type u_4<VAR>A : Matrix n n α<VAR>inst✝⁴ : AddMonoid α<VAR>inst✝³ : StarAddMonoid α<VAR>inst✝² : AddMonoid β<VAR>inst✝¹ : StarAddMonoid β<VAR>inst✝ : DecidableEq n<VAR>d : n → α<GOAL>(diagonal d).IsHermitian ↔ ∀ (i : n), IsSelfAdjoint (d i)
<VAR>M✝ : Type u_1<VAR>N : Type u_2<VAR>A : Type u_3<VAR>inst✝² : Monoid M✝<VAR>inst✝¹ : Monoid N<VAR>s : Set M✝<VAR>M : Type u_4<VAR>inst✝ : Monoid M<VAR>a : M<GOAL>a ∈ setOf IsUnit ↔ IsUnit a
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z w : ℂ<VAR>h : z.re = w.re<GOAL>dist z w = dist z.im w.im
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>c : E''<GOAL>(fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<GOAL>(fun _x => 0) =o[l] g'' ↔ 0 = 0 ∨ Tendsto (norm ∘ g'') l atTop
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>G : Type u_5<VAR>E' : Type u_6<VAR>F' : Type u_7<VAR>G' : Type u_8<VAR>E'' : Type u_9<VAR>F'' : Type u_10<VAR>G'' : Type u_11<VAR>E''' : Type u_12<VAR>R : Type u_13<VAR>R' : Type u_14<VAR>𝕜 : Type u_15<VAR>𝕜' : Type u_16<VAR>inst✝¹³ : Norm E<VAR>inst✝¹² : Norm F<VAR>inst✝¹¹ : Norm G<VAR>inst✝¹⁰ : SeminormedAddCommGroup E'<VAR>inst✝⁹ : SeminormedAddCommGroup F'<VAR>inst✝⁸ : SeminormedAddCommGroup G'<VAR>inst✝⁷ : NormedAddCommGroup E''<VAR>inst✝⁶ : NormedAddCommGroup F''<VAR>inst✝⁵ : NormedAddCommGroup G''<VAR>inst✝⁴ : SeminormedRing R<VAR>inst✝³ : SeminormedAddGroup E'''<VAR>inst✝² : SeminormedRing R'<VAR>inst✝¹ : NormedDivisionRing 𝕜<VAR>inst✝ : NormedDivisionRing 𝕜'<VAR>c✝ c' c₁ c₂ : ℝ<VAR>f : α → E<VAR>g : α → F<VAR>k : α → G<VAR>f' : α → E'<VAR>g' : α → F'<VAR>k' : α → G'<VAR>f'' : α → E''<VAR>g'' : α → F''<VAR>k'' : α → G''<VAR>l l' : Filter α<VAR>c : E''<VAR>hc : c ≠ 0<GOAL>(fun _x => c) =o[l] g'' ↔ c = 0 ∨ Tendsto (norm ∘ g'') l atTop