ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<VAR>p : Z<GOAL>dist x z ≤ (⨅ p, dist z (Φ p) + dist y (Ψ p)) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<VAR>p q : Z<GOAL>dist x z ≤ dist z (Φ q) + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type w<VAR>inst✝² : MetricSpace X<VAR>inst✝¹ : MetricSpace Y<VAR>Φ✝ : Z → X<VAR>Ψ✝ : Z → Y<VAR>ε✝ : ℝ<VAR>inst✝ : Nonempty Z<VAR>Φ : Z → X<VAR>Ψ : Z → Y<VAR>ε : ℝ<VAR>H : ∀ (p q : Z), |dist (Φ p) (Φ q) - dist (Ψ p) (Ψ q)| ≤ 2 * ε<VAR>x : X<VAR>y : Y<VAR>z : X<VAR>p q : Z<GOAL>dist x z ≤ dist (Φ q) z + dist y (Ψ q) + (dist x (Φ p) + (dist y (Ψ p) + 2 * ε))
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>(mapL fun i => (g i).comp (f i)) = (mapL g).comp (mapL f)
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<GOAL>↑(mapL fun i => (g i).comp (f i)) = ↑((mapL g).comp (mapL f))
<VAR>ι : Type uι<VAR>inst✝⁹ : Fintype ι<VAR>𝕜 : Type u𝕜<VAR>inst✝⁸ : NontriviallyNormedField 𝕜<VAR>E : ι → Type uE<VAR>inst✝⁷ : (i : ι) → SeminormedAddCommGroup (E i)<VAR>inst✝⁶ : (i : ι) → NormedSpace 𝕜 (E i)<VAR>F : Type uF<VAR>inst✝⁵ : SeminormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>E' : ι → Type u_1<VAR>E'' : ι → Type u_2<VAR>inst✝³ : (i : ι) → SeminormedAddCommGroup (E' i)<VAR>inst✝² : (i : ι) → NormedSpace 𝕜 (E' i)<VAR>inst✝¹ : (i : ι) → SeminormedAddCommGroup (E'' i)<VAR>inst✝ : (i : ι) → NormedSpace 𝕜 (E'' i)<VAR>g : (i : ι) → E' i →L[𝕜] E'' i<VAR>f : (i : ι) → E i →L[𝕜] E' i<VAR>x✝ : (i : ι) → E i<GOAL>((↑(mapL fun i => (g i).comp (f i))).compMultilinearMap (tprod 𝕜)) x✝ = ((↑((mapL g).comp (mapL f))).compMultilinearMap (tprod 𝕜)) x✝
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : (f '' s).Subsingleton<GOAL>eVariationOn f s = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : (f '' s).Subsingleton<GOAL>∀ x ∈ s, ∀ y ∈ s, edist (f x) (f y) = 0
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>E : Type u_2<VAR>inst✝ : PseudoEMetricSpace E<VAR>f : α → E<VAR>s : Set α<VAR>hf : (f '' s).Subsingleton<VAR>x : α<VAR>xs : x ∈ s<VAR>y : α<VAR>ys : y ∈ s<GOAL>edist (f x) (f y) = 0
<VAR>f g : CircleDeg1Lift<GOAL>Tendsto (fun n => (f ^ (n + 1)) 0 / (↑n + 1)) atTop (𝓝 (τ f))
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ ((fun n => 1 / ↑n) ∘ fun a => a + 1) n
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<GOAL>dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < ↑n + 1<GOAL>dist ((f ^ (n + 1)) 0 / (↑n + 1)) (τ f) ≤ 1 / ↑(n + 1)
<VAR>f g : CircleDeg1Lift<VAR>n : ℕ<VAR>this : 0 < ↑n + 1<GOAL>dist ((f ^ (n + 1)) 0) (↑(n + 1) * τ f) ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsMarkovKernel η<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>((κ ⊗ₖ η).fst x) s = (κ x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsMarkovKernel η<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), (η (x, b)) {c | (b, c) ∈ {p | p.1 ∈ s}} ∂κ x = (κ x) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsMarkovKernel η<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.1 ∈ s}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>δ : Type u_4<VAR>mδ : MeasurableSpace δ<VAR>γ : Type u_5<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>κ : Kernel α β<VAR>η : Kernel (α × β) γ<VAR>inst✝¹ : IsSFiniteKernel κ<VAR>inst✝ : IsMarkovKernel η<VAR>x : α<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), (η (x, b)) {c | b ∈ s} ∂κ x = (κ x) s
<VAR>a b c d✝ m n : ℤ<VAR>h : b ∣ a<VAR>hb : b ≠ 0<VAR>d : ℤ<GOAL>c = a / b * d ↔ b * c = a * d
<VAR>a b c d✝ m n : ℤ<VAR>h : b ∣ a<VAR>hb : b ≠ 0<VAR>d : ℤ<VAR>this : b ∣ d * a<GOAL>c = a / b * d ↔ b * c = a * d
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : b₁ < b₂<GOAL>Ioc a b₁ ⊆ Ioo a b₂
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a a₁ a₂ b b₁ b₂ c x : α<VAR>h : b₁ < b₂<GOAL>Set.Ioc a b₁ ⊆ Set.Ioo a b₂
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝⁵ : CommSemiring k<VAR>inst✝⁴ : AddMonoid G<VAR>A : Type u₃<VAR>inst✝³ : Semiring A<VAR>inst✝² : Algebra k A<VAR>B : Type u_3<VAR>inst✝¹ : Semiring B<VAR>inst✝ : Algebra k B<VAR>F : Multiplicative G →* A<VAR>f : MonoidAlgebra k G<GOAL>((lift k G A) F) f = sum f fun a b => b • F (Multiplicative.ofAdd a)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.78745, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<GOAL>Mono S.f
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.78745, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>s : S.Splitting<VAR>this : IsSplitMono S.f<GOAL>Mono S.f
<VAR>a✝ b✝ c✝ d m n a b c : ℤ<VAR>hab : a = b<GOAL>b ≤ b
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>seminormFromBounded' f 1 = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>⨆ y, f y / f y = 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>⨆ y, f y / f y ≤ 1
<VAR>R : Type u_1<VAR>inst✝ : CommRing R<VAR>f : R → ℝ<VAR>c : ℝ<VAR>f_ne_zero : f ≠ 0<VAR>f_nonneg : 0 ≤ f<VAR>f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y<GOAL>1 ≤ ⨆ y, f y / f y
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : ExpChar R p<VAR>h : Function.Injective ⇑(frobenius R p)<VAR>x : R<GOAL>x ∈ pNilradical R p → x ∈ ⊥
<VAR>R : Type u_1<VAR>inst✝¹ : CommRing R<VAR>p : ℕ<VAR>inst✝ : ExpChar R p<VAR>h : Function.Injective ⇑(frobenius R p)<VAR>x : R<GOAL>(∃ n, x ^ p ^ n = 0) → x = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>s s' : Finset α<VAR>t t' : Finset β<VAR>a : α<VAR>b : β<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : DecidableEq β<VAR>x : α<VAR>y : β<GOAL>(x, y) ∈ s ×ˢ (t ∪ t') ↔ (x, y) ∈ s ×ˢ t ∪ s ×ˢ t'
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>A : Type u_5<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : NormedSpace ℝ E<VAR>a b c✝ d : ℝ<VAR>f : ℝ → E<VAR>c : ℝ<GOAL>c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R✝ M<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Module K M<VAR>f g : End K M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<VAR>a : End K M<VAR>ha : a ∈ Algebra.adjoin K {f, g}<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}<VAR>S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))<GOAL>a.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R✝ M<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Module K M<VAR>f g : End K M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<VAR>a : End K M<VAR>ha : a ∈ Algebra.adjoin K {f, g}<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}<VAR>S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))<VAR>this : Finite K R<GOAL>a.IsSemisimple
<VAR>R✝ : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : CommRing R✝<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : Module R✝ M<VAR>K : Type u_3<VAR>inst✝³ : Field K<VAR>inst✝² : Module K M<VAR>f g : End K M<VAR>inst✝¹ : FiniteDimensional K M<VAR>inst✝ : PerfectField K<VAR>comm : Commute f g<VAR>hf : f.IsSemisimple<VAR>hg : g.IsSemisimple<VAR>a : End K M<VAR>ha : a ∈ Algebra.adjoin K {f, g}<VAR>R : Type u_3 := K[X] ⧸ Ideal.span {minpoly K f}<VAR>S : Type u_3 := AdjoinRoot (map (algebraMap K R) (minpoly K g))<VAR>this✝ : Finite K R<VAR>this : Finite R S<GOAL>a.IsSemisimple
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this : Algebra K ℂ := φ.toAlgebra<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<GOAL>∃ σ, φ.comp ↑σ.symm = ψ
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<GOAL>φ.comp ↑(ψ'.restrictNormal' K).symm.symm = ψ
<VAR>k : Type u_1<VAR>inst✝⁹ : Field k<VAR>K : Type u_2<VAR>inst✝⁸ : Field K<VAR>F : Type u_3<VAR>inst✝⁷ : Field F<VAR>inst✝⁶ : NumberField K<VAR>inst✝⁵ : Algebra k K<VAR>inst✝⁴ : Algebra k F<VAR>inst✝³ : Algebra K F<VAR>inst✝² : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>inst✝¹ : Algebra k K<VAR>inst✝ : IsGalois k K<VAR>φ ψ : K →+* ℂ<VAR>h : φ.comp (algebraMap k K) = ψ.comp (algebraMap k K)<VAR>this✝¹ : Algebra k ℂ := (φ.comp (algebraMap k K)).toAlgebra<VAR>this✝ : Algebra K ℂ := φ.toAlgebra<VAR>this : IsScalarTower k K ℂ<VAR>ψ' : K →ₐ[k] ℂ := { toRingHom := ψ, commutes' := ⋯ }<VAR>x : K<GOAL>(φ.comp ↑(ψ'.restrictNormal' K).symm.symm) x = ψ x
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>I : Box ι<GOAL>∃ J, (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧ Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)
<VAR>ι : Type u_1<VAR>I✝ J : Box ι<VAR>x y : ι → ℝ<VAR>I : Box ι<VAR>a b : ι → ℕ → ℝ<VAR>ha_anti : ∀ (i : ι), StrictAnti (a i)<VAR>hb_mono : ∀ (i : ι), StrictMono (b i)<VAR>ha_mem : ∀ (i : ι) (k : ℕ), a i k ∈ Ioo (I.lower i) (I.upper i)<VAR>hb_mem : ∀ (i : ι) (l : ℕ), b i l ∈ Ioo (I.lower i) (I.upper i)<VAR>hab : ∀ (i : ι) (k l : ℕ), a i k < b i l<VAR>ha_tendsto : ∀ (i : ι), Tendsto (a i) atTop (𝓝 (I.lower i))<VAR>hb_tendsto : ∀ (i : ι), Tendsto (b i) atTop (𝓝 (I.upper i))<GOAL>∃ J, (∀ (n : ℕ), Box.Icc (J n) ⊆ Box.Ioo I) ∧ Tendsto (lower ∘ ⇑J) atTop (𝓝 I.lower) ∧ Tendsto (upper ∘ ⇑J) atTop (𝓝 I.upper)
<VAR>α : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : StrictOrderedRing R<VAR>inst✝ : Archimedean R<VAR>r : R<VAR>n : ℕ<VAR>hn : -r ≤ ↑n<GOAL>↑(-↑n) ≤ r
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : TopologicalSpace R<VAR>inst✝⁴ : TopologicalSpace M<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : TopologicalRing R<VAR>inst✝ : TopologicalAddGroup M<VAR>hmul : Tendsto (fun p => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)<VAR>hmulleft : ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)<VAR>hmulright : ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)<GOAL>Continuous fun p => p.1 • p.2
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<GOAL>∃ I ∈ nonPrincipals R, ∀ J ∈ c, J ≤ I
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<GOAL>sSup c ∈ nonPrincipals R
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<VAR>hxmem : x ∈ sSup c<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<VAR>hxmem : x ∈ sSup c<VAR>J : Submodule R R<VAR>hJc : J ∈ c<VAR>hxJ : x ∈ J<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hs : c ⊆ nonPrincipals R<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<VAR>hxmem : x ∈ sSup c<VAR>J : Submodule R R<VAR>hJc : J ∈ c<VAR>hxJ : x ∈ J<VAR>hsSupJ : sSup c = J<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<VAR>hxmem : x ∈ sSup c<VAR>J : Submodule R R<VAR>hJc : J ∈ c<VAR>hxJ : x ∈ J<VAR>hsSupJ : sSup c = J<VAR>hs : J ∈ nonPrincipals R<GOAL>False
<VAR>R : Type u<VAR>M : Type v<VAR>inst✝ : CommRing R<VAR>c : Set (Ideal R)<VAR>hchain : IsChain (fun x x_1 => x ≤ x_1) c<VAR>K : Ideal R<VAR>hKmem : K ∈ c<VAR>x : R<VAR>hx : sSup c = Submodule.span R {x}<VAR>hxmem : x ∈ sSup c<VAR>J : Submodule R R<VAR>hJc : J ∈ c<VAR>hxJ : x ∈ J<VAR>hsSupJ : sSup c = J<VAR>hs : ¬(Submodule.span R {x}).IsPrincipal<GOAL>False
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactPair X Y<GOAL>Continuous fun p => p.1 p.2
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>inst✝ : LocallyCompactPair X Y<GOAL>∀ (x : C(X, Y) × X) (i : Set Y), x.1 x.2 ∈ i ∧ IsOpen i → ∀ᶠ (x : C(X, Y) × X) in 𝓝 x, x.1 x.2 ∈ i
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K : Set X<VAR>U✝ : Set Y<VAR>inst✝ : LocallyCompactPair X Y<VAR>f : C(X, Y)<VAR>x : X<VAR>U : Set Y<VAR>hx : f x ∈ U<VAR>hU : IsOpen U<GOAL>∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), x.1 x.2 ∈ U
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝⁴ : TopologicalSpace X<VAR>inst✝³ : TopologicalSpace Y<VAR>inst✝² : TopologicalSpace Z<VAR>inst✝¹ : TopologicalSpace T<VAR>K✝ : Set X<VAR>U✝ : Set Y<VAR>inst✝ : LocallyCompactPair X Y<VAR>f : C(X, Y)<VAR>x : X<VAR>U : Set Y<VAR>hx : f x ∈ U<VAR>hU : IsOpen U<VAR>K : Set X<VAR>hxK : K ∈ 𝓝 x<VAR>hK : IsCompact K<VAR>hKU : MapsTo (⇑f) K U<GOAL>∀ᶠ (x : C(X, Y) × X) in 𝓝 (f, x), x.1 x.2 ∈ U
<VAR>R : Type u_1<VAR>inst✝⁸ : CommRing R<VAR>I : Ideal R<VAR>M : Type u_2<VAR>inst✝⁷ : AddCommGroup M<VAR>inst✝⁶ : Module R M<VAR>N : Type u_3<VAR>inst✝⁵ : AddCommGroup N<VAR>inst✝⁴ : Module R N<VAR>P : Type u_4<VAR>inst✝³ : AddCommGroup P<VAR>inst✝² : Module R P<VAR>T : Type u_5<VAR>inst✝¹ : AddCommGroup T<VAR>inst✝ : Module (AdicCompletion I R) T<VAR>f : M →ₗ[R] N<VAR>g : N →ₗ[R] P<VAR>x : AdicCompletion I M<GOAL>(map I g ∘ₗ map I f) x = (map I (g ∘ₗ f)) x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<VAR>K : Set X<VAR>hK : IsCompact K<VAR>x✝ : X<GOAL>x✝ ∈ closure K ↔ x✝ ∈ ⋃ x ∈ K, {y | Inseparable x y}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>hf : UniformContinuous f<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α<VAR>c : Set α<VAR>hfc : c.Finite<VAR>hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}<GOAL>f '' s ⊆ ⋃ y ∈ f '' c, {x | (x, y) ∈ t}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>hf : UniformContinuous f<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α<VAR>c : Set α<VAR>hfc : c.Finite<VAR>hct : s ⊆ ⋃ y ∈ c, {x | (x, y) ∈ {p | (f p.1, f p.2) ∈ t}}<GOAL>s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝ : UniformSpace β<VAR>f : α → β<VAR>s : Set α<VAR>hs : TotallyBounded s<VAR>hf : UniformContinuous f<VAR>t : Set (β × β)<VAR>ht : t ∈ 𝓤 β<VAR>this : {p | (f p.1, f p.2) ∈ t} ∈ 𝓤 α<VAR>c : Set α<VAR>hfc : c.Finite<VAR>hct : ∀ x ∈ s, ∃ i ∈ c, (f x, f i) ∈ t<GOAL>s ⊆ ⋃ i ∈ c, {a | (f a, f i) ∈ t}
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (node s l x r).Sized<GOAL>0 < s
<VAR>α : Type u_1<VAR>s : ℕ<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>h : (node s l x r).Sized<GOAL>0 < l.size + r.size + 1
<VAR>z✝ : ℂ<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>z : ℂ<GOAL>dist z ((starRingEnd ℂ) z) = 2 * |z.im|
<VAR>𝕜 : Type u_1<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>L : E →L[𝕜] F<VAR>h : s =ᶠ[𝓝 x] t<GOAL>lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t x v
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>β : ι → Type u_3<VAR>inst✝³ : Fintype ι<VAR>inst✝² : (i : ι) → DecidableEq (β i)<VAR>γ : ι → Type u_4<VAR>inst✝¹ : (i : ι) → DecidableEq (γ i)<VAR>inst✝ : (i : ι) → AddGroup (β i)<VAR>x y : (i : ι) → β i<GOAL>hammingDist x y = hammingNorm (x - y)
<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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝ : α → β<VAR>inst✝ : MeasurableSpace α<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>hs : NullMeasurableSet s (comap f μ)<GOAL>(comap f μ) s = μ (f '' 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>m0 : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>inst✝¹ : MeasurableSpace γ<VAR>μ✝ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s s' t : Set α<VAR>f✝ : α → β<VAR>inst✝ : MeasurableSpace α<VAR>f : α → β<VAR>μ : Measure β<VAR>hfi : Injective f<VAR>hf : ∀ (s : Set α), MeasurableSet s → NullMeasurableSet (f '' s) μ<VAR>hs : NullMeasurableSet s (((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯)<GOAL>(((OuterMeasure.comap f) μ.toOuterMeasure).toMeasure ⋯) s = μ (f '' s)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : HasZeroObject C<VAR>inst✝³ : HasShift C ℤ<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive<VAR>inst✝ : Pretriangulated C<VAR>S : Subcategory C<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>S.W f ↔ ∃ Z g h, ∃ (_ : Triangle.mk f g h ∈ distinguishedTriangles), S.P Z
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝ : SDiff α<VAR>a b : α<GOAL>some a \ some b = some (a \ b)
<VAR>α✝ : Type u_1<VAR>α : Type u_2<VAR>inst✝² : OrderedRing α<VAR>inst✝¹ : Nontrivial α<VAR>inst✝ : DecidableRel fun x x_1 => x < x_1<VAR>n : ℤ<GOAL>sign ↑n = sign n
<VAR>α : Type u_1<VAR>inst✝¹⁰ : MetricSpace α<VAR>β : Type u<VAR>inst✝⁹ : SecondCountableTopology α<VAR>inst✝⁸ : MeasurableSpace α<VAR>inst✝⁷ : OpensMeasurableSpace α<VAR>inst✝⁶ : HasBesicovitchCovering α<VAR>inst✝⁵ : MetricSpace β<VAR>inst✝⁴ : MeasurableSpace β<VAR>inst✝³ : BorelSpace β<VAR>inst✝² : SecondCountableTopology β<VAR>inst✝¹ : HasBesicovitchCovering β<VAR>μ : Measure β<VAR>inst✝ : IsLocallyFiniteMeasure μ<VAR>s : Set β<VAR>hs : MeasurableSet s<GOAL>∀ᵐ (x : β) ∂μ, Tendsto (fun r => μ (s ∩ closedBall x r) / μ (closedBall x r)) (𝓝[>] 0) (𝓝 (s.indicator 1 x))