ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0<VAR>s : O<VAR>hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0<VAR>hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s = 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r + (Ideal.Quotient.mk (Ideal.span {↑p})) s) ≤ max (preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r)) (preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0<VAR>s : O<VAR>hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0<VAR>hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0<GOAL>preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) (r + s)) ≤ max (preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) r)) (preVal K v O hv p ((Ideal.Quotient.mk (Ideal.span {↑p})) s))
<VAR>K : Type u₁<VAR>inst✝² : Field K<VAR>v : Valuation K ℝ≥0<VAR>O : Type u₂<VAR>inst✝¹ : CommRing O<VAR>inst✝ : Algebra O K<VAR>hv : v.Integers O<VAR>p : ℕ<VAR>hp : Fact (Nat.Prime p)<VAR>hvp : Fact (v ↑p ≠ 1)<VAR>r : O<VAR>hx0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) r = 0<VAR>s : O<VAR>hy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) s = 0<VAR>hxy0 : ¬(Ideal.Quotient.mk (Ideal.span {↑p})) (r + s) = 0<GOAL>v ((algebraMap O K) r + (algebraMap O K) s) ≤ max (v ((algebraMap O K) r)) (v ((algebraMap O K) s))
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>i : ι<VAR>b₁ : β₁ i<VAR>b₂ : β₂ i<VAR>j : ι<GOAL>(zipWith f hf (single i b₁) (single i b₂)) j = (single i (f i b₁ b₂)) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>i : ι<VAR>b₁ : β₁ i<VAR>b₂ : β₂ i<VAR>j : ι<GOAL>f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>i : ι<VAR>b₁ : β₁ i<VAR>b₂ : β₂ i<GOAL>f i ((single i b₁) i) ((single i b₂) i) = (single i (f i b₁ b₂)) i
<VAR>ι : Type u<VAR>γ : Type w<VAR>β : ι → Type v<VAR>β₁ : ι → Type v₁<VAR>β₂ : ι → Type v₂<VAR>inst✝³ : DecidableEq ι<VAR>inst✝² : (i : ι) → Zero (β i)<VAR>s : Finset ι<VAR>x : (i : ↑↑s) → β ↑i<VAR>i✝ : ι<VAR>inst✝¹ : (i : ι) → Zero (β₁ i)<VAR>inst✝ : (i : ι) → Zero (β₂ i)<VAR>f : (i : ι) → β₁ i → β₂ i → β i<VAR>hf : ∀ (i : ι), f i 0 0 = 0<VAR>i : ι<VAR>b₁ : β₁ i<VAR>b₂ : β₂ i<VAR>j : ι<VAR>hij : i ≠ j<GOAL>f j ((single i b₁) j) ((single i b₂) j) = (single i (f i b₁ b₂)) j
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>inst✝⁴ : MeasurableSpace α<VAR>μ : Measure α<VAR>l : Filter ι<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : AECover μ l φ<VAR>f : α → E<VAR>hfi : Integrable f μ<VAR>h : Tendsto (fun i => ∫ (x : α), (φ i).indicator f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))<VAR>x✝ : ι<GOAL>∫ (x : α) in φ x✝, f x ∂μ = ∫ (x : α), (φ x✝).indicator f x ∂μ
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>inst✝⁴ : NonUnitalNonAssocSemiring R<VAR>M : Subsemigroup R<VAR>inst✝³ : NonUnitalNonAssocSemiring S<VAR>inst✝² : NonUnitalNonAssocSemiring T<VAR>F : Type u_1<VAR>inst✝¹ : FunLike F R S<VAR>inst✝ : NonUnitalRingHomClass F R S<VAR>s : NonUnitalSubsemiring R<VAR>x : R × S<GOAL>x ∈ s.prod ⊤ ↔ x ∈ comap (NonUnitalRingHom.fst R S) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m : MeasurableSpace α<VAR>μ ν : Measure α<VAR>inst✝² : MeasurableSpace δ<VAR>inst✝¹ : NormedAddCommGroup β<VAR>inst✝ : NormedAddCommGroup γ<VAR>f : α → β<VAR>hf : Integrable f μ<GOAL>↑‖toL1 f hf‖₊ = ∫⁻ (a : α), ↑‖f a‖₊ ∂μ
<VAR>ι : Type u_1<VAR>a s : ι → ℕ<VAR>l : List ι<VAR>co : List.Pairwise (Coprime on s) l<VAR>hs : ∀ i ∈ l, s i ≠ 0<GOAL>↑(chineseRemainderOfList a s l co) < (List.map s l).prod
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : Group β<VAR>u₁ u₂ : UniformSpace β<VAR>h₁ : UniformGroup β<VAR>h₂ : UniformGroup β<GOAL>UniformGroup β
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : UniformSpace α<VAR>inst✝² : Group α<VAR>inst✝¹ : UniformGroup α<VAR>inst✝ : Group β<VAR>u₁ u₂ : UniformSpace β<VAR>h₁ : UniformGroup β<VAR>h₂ : UniformGroup β<VAR>b : Bool<GOAL>UniformGroup β
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : CompleteSpace (α × β)<VAR>h : Nonempty β<VAR>f✝ : Filter α<VAR>hf : Cauchy f✝<VAR>y : β<VAR>a : α<VAR>b : β<VAR>hab : f✝ ×ˢ pure y ≤ 𝓝 (a, b)<GOAL>f✝ ≤ 𝓝 a
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>W.Equation (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (W.negAddY x₁ x₂ y₁ (W.slope x₁ x₂ y₁ y₂))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>eval (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) (-((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))))) = 0
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Affine R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Affine F<VAR>x₁ x₂ y₁ y₂ : F<VAR>h₁ : W.Equation x₁ y₁<VAR>h₂ : W.Equation x₂ y₂<VAR>hxy : x₁ = x₂ → y₁ ≠ W.negY x₂ y₂<GOAL>-((W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₁) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - x₂) * (W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) - W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂))) = 0
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : CompactSpace α<VAR>f : C(α, 𝕜)<VAR>a : α<GOAL>(exp 𝕜 f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : CompactSpace α<VAR>f : C(α, 𝕜)<VAR>a : α<GOAL>(∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : CompactSpace α<VAR>f : C(α, 𝕜)<VAR>a : α<VAR>h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f<GOAL>(∑' (n : ℕ), (expSeries 𝕜 C(α, 𝕜) n) fun x => f) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a
<VAR>𝕜 : Type u_1<VAR>α : Type u_2<VAR>inst✝² : RCLike 𝕜<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : CompactSpace α<VAR>f : C(α, 𝕜)<VAR>a : α<VAR>h_sum : Summable fun n => (expSeries 𝕜 C(α, 𝕜) n) fun x => f<GOAL>∑' (i : ℕ), ((↑i.factorial)⁻¹ • f ^ i) a = { toFun := exp 𝕜 ∘ ⇑f, continuous_toFun := ⋯ } a
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a b : α<VAR>n : ℕ<GOAL>count a (replicate n b) = if a = b then n else 0
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s : Multiset α<VAR>a b : α<VAR>n : ℕ<GOAL>count a (replicate n b) = List.count a (List.replicate n b)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>a a₁ a₂ : α<VAR>b b₁ b₂ : β<VAR>inst✝⁶ : Zero α<VAR>inst✝⁵ : Zero β<VAR>inst✝⁴ : SMulWithZero α β<VAR>inst✝³ : Preorder α<VAR>inst✝² : Preorder β<VAR>inst✝¹ : SMulPosStrictMono α β<VAR>inst✝ : SMulPosReflectLT α β<VAR>hb : 0 < b<GOAL>0 < a • b ↔ 0 < a
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>M : Type u_3<VAR>inst✝⁷ : CommRing R<VAR>inst✝⁶ : LieRing L<VAR>inst✝⁵ : LieAlgebra R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>h e f : L<VAR>inst✝ : NoZeroSMulDivisors ℤ M<VAR>t : IsSl2Triple h e f<VAR>m : M<VAR>μ ρ : R<VAR>hm : m ≠ 0<VAR>hm' : ⁅h, m⁆ = μ • m<VAR>he : ⁅e, m⁆ = ρ • m<GOAL>2 • ⁅e, m⁆ = 0
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝² : UniformSpace α<VAR>inst✝¹ : UniformSpace β<VAR>inst✝ : UniformSpace γ<VAR>ι : Sort u_1<VAR>ι' : Sort u_2<VAR>p : ι → Prop<VAR>p' : ι' → Prop<VAR>s : ι → Set (α × α)<VAR>s' : ι' → Set (β × β)<VAR>h : (𝓤 α).HasBasis p s<VAR>h' : (𝓤 β).HasBasis p' s'<VAR>f : α → β<GOAL>UniformEmbedding f ↔ Injective f ∧ (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧ ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
<VAR>S : Type u_1<VAR>α : Type u_2<VAR>inst✝² : InvolutiveStar α<VAR>inst✝¹ : SetLike S α<VAR>inst✝ : StarMemClass S α<VAR>s : S<VAR>x : α<GOAL>x ∈ star ↑s ↔ x ∈ ↑s
<VAR>S : Type u_1<VAR>α : Type u_2<VAR>inst✝² : InvolutiveStar α<VAR>inst✝¹ : SetLike S α<VAR>inst✝ : StarMemClass S α<VAR>s : S<VAR>x : α<GOAL>star x ∈ s ↔ x ∈ s
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : CompactSpace X<VAR>W : Clopens (X × Y)<GOAL>∃ I, W = I.sup fun i => i.1 ×ˢ i.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : CompactSpace X<VAR>W : Clopens (X × Y)<VAR>U : X × Y → Clopens X<VAR>hxU : ∀ x ∈ W, x.1 ∈ U x<VAR>V : X × Y → Clopens Y<VAR>hxV : ∀ x ∈ W, x.2 ∈ V x<VAR>hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W<GOAL>∃ I, W = I.sup fun i => i.1 ×ˢ i.2
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : CompactSpace Y<VAR>inst✝ : CompactSpace X<VAR>W : Clopens (X × Y)<VAR>U : X × Y → Clopens X<VAR>hxU : ∀ x ∈ W, x.1 ∈ U x<VAR>V : X × Y → Clopens Y<VAR>hxV : ∀ x ∈ W, x.2 ∈ V x<VAR>hUV : ∀ x ∈ W, U x ×ˢ V x ≤ W<VAR>I : Finset (X × Y)<VAR>hIW : ∀ x ∈ I, x ∈ W.carrier<VAR>hWI : W.carrier ⊆ ⋃ x ∈ I, ↑(U x) ×ˢ ↑(V x)<GOAL>∃ I, W = I.sup fun i => i.1 ×ˢ i.2
<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.ReflectsEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi (G.map f)<GOAL>Epi 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.ReflectsEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi (G.map f)<GOAL>Epi (F.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.ReflectsEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi (G.map f)<VAR>this : Epi (G.map f ≫ (α.app Y).inv)<GOAL>Epi (F.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.ReflectsEpimorphisms<VAR>α : F ≅ G<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>h : Epi (G.map f)<VAR>this : Epi (G.map f ≫ (α.app Y).inv)<GOAL>F.map f = (α.app X).hom ≫ G.map f ≫ (α.app Y).inv
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>l₁ : Filter α<VAR>l₂ : Filter β<VAR>f : α → β<GOAL>Tendsto f l₁ l₂ ↔ RTendsto (Function.graph f) l₁ l₂
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : CommSemiring R₂<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.SeparatingRight ↔ ker B.flip = ⊥
<VAR>R : Type u<VAR>S : Type v<VAR>a b : R<VAR>m n : ℕ<VAR>ι : Type y<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>i : ℕ<VAR>hi : f.degree = ↑i<GOAL>f.integralNormalization.coeff i = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : AddCommGroup E<VAR>inst✝² : Module ℝ E<VAR>s t : Set E<VAR>x✝ : E<VAR>a : ℝ<VAR>inst✝¹ : TopologicalSpace E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>hs₂ : IsOpen s<VAR>x : E<VAR>hx : x ∈ s<GOAL>x ∈ interior s
<VAR>N : ℕ<VAR>χ : DirichletCharacter ℂ N<GOAL>(((fun n => χ ↑n) * fun n => ↑(Λ n)) ⍟ fun n => χ ↑n) = (fun n => χ ↑n) * fun n => Complex.log ↑n
<VAR>x y : ℝ<GOAL>abs (↑x + ↑y * I) = √(x ^ 2 + y ^ 2)
<VAR>x y : ℝ<GOAL>abs (↑x + ↑y * I) = √(normSq (↑x + ↑y * I))
<VAR>ι : Type u_1<VAR>M : ι → Type u_2<VAR>inst✝¹ : (i : ι) → Monoid (M i)<VAR>N : Type u_3<VAR>inst✝ : Monoid N<VAR>i : ι<GOAL>Function.Injective ⇑of
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PartialOrder β<VAR>f : α → β<VAR>𝒜 𝒜₁ 𝒜₂ : Finset (Finset α)<VAR>s t u : Finset α<VAR>a b : α<GOAL>{ ofColex := {a} } < { ofColex := {b} } ↔ a < b
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.18276, u_2} D<VAR>inst✝¹ : HasZeroMorphisms C<VAR>inst✝ : HasZeroMorphisms D<VAR>S✝ S₁ S₂ : ShortComplex C<VAR>S : ShortComplex Cᵒᵖ<VAR>h : S.HomologyData<VAR>z : IsZero h.left.H<GOAL>S.unop.Exact
<VAR>α β : Type u<VAR>c : Cardinal.{u}<GOAL>lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atBot atBot<GOAL>Tendsto (↑(hf.stieltjesFunction a)) atBot (𝓝 0)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atBot atBot<VAR>x : ℝ<GOAL>↑(hf.stieltjesFunction a) x ≤ (f a ∘ qs) x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>inst✝ : MeasurableSpace α<VAR>f : α → ℚ → ℝ<VAR>hf : IsMeasurableRatCDF f<VAR>a : α<VAR>h_exists : ∀ (x : ℝ), ∃ q, x < ↑q ∧ ↑q < x + 1<VAR>qs : ℝ → ℚ := fun x => ⋯.choose<VAR>hqs_tendsto : Tendsto qs atBot atBot<VAR>x : ℝ<GOAL>↑(hf.stieltjesFunction a) x ≤ ↑(hf.stieltjesFunction a) ↑(qs x)
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X : C<GOAL>∃ A a, IsGalois A ∧ Function.Bijective fun f => F.map f a
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X A : C<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>a : ↑(F.obj A)<VAR>h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>h2 : IsConnected A<VAR>h3 : Mono u<GOAL>∃ A a, IsGalois A ∧ Function.Bijective fun f => F.map f a
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X A : C<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>a : ↑(F.obj A)<VAR>h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>h2 : IsConnected A<VAR>h3 : Mono u<GOAL>∃ a, IsGalois A ∧ Function.Bijective fun f => F.map f a
<VAR>C : Type u₁<VAR>inst✝² : Category.{u₂, u₁} C<VAR>inst✝¹ : GaloisCategory C<VAR>F : C ⥤ FintypeCat<VAR>inst✝ : FiberFunctor F<VAR>X A : C<VAR>u : A ⟶ CategoryTheory.PreGaloisCategory.selfProd F X<VAR>a : ↑(F.obj A)<VAR>h1 : F.map u a = CategoryTheory.PreGaloisCategory.mkSelfProdFib F X<VAR>h2 : IsConnected A<VAR>h3 : Mono u<GOAL>IsGalois A ∧ Function.Bijective fun f => F.map f a
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>b : α<GOAL>sSup {a | IsAtom a ∧ a ≤ b} = b
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝¹ : CompleteLattice α<VAR>inst✝ : IsAtomistic α<VAR>s : Set α<VAR>hs : ∀ a ∈ s, IsAtom a<GOAL>sSup {a | IsAtom a ∧ a ≤ sSup s} = sSup s
<VAR>R : Type u_1<VAR>F : Type u<VAR>K : Type v<VAR>L : Type w<VAR>inst✝³ : CommRing R<VAR>inst✝² : Field K<VAR>inst✝¹ : Field L<VAR>inst✝ : Field F<VAR>i✝ : K →+* L<VAR>p : K[X]<VAR>i : K →+* L<VAR>p_ne_zero : p ≠ 0<VAR>hsplit : Splits i p<GOAL>p.degree = ↑(Multiset.card (map i p).roots)
<VAR>α : Type u_1<VAR>β : Type v<VAR>γ : Type u_2<VAR>inst✝ : DecidableEq α<VAR>s✝ s : Multiset α<VAR>n : ℕ<VAR>x : α<GOAL>s ∩ replicate n x = replicate (min (count x s) n) x
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hstar : ∀ (x y : A), p x y → p (star x) (star y)<VAR>Hstar_left : ∀ (x y : A), p x y → p (star x) y<VAR>Hstar_right : ∀ (x y : A), p x y → p x (star y)<GOAL>p a b
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hstar : ∀ (x y : A), p x y → p (star x) (star y)<VAR>Hstar_left : ∀ (x y : A), p x y → p (star x) y<VAR>Hstar_right : ∀ (x y : A), p x y → p x (star y)<VAR>x : A<VAR>hx : x ∈ s ∪ star s<VAR>y : A<VAR>hy : y ∈ s ∪ star s<GOAL>p x y
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hstar : ∀ (x y : A), p x y → p (star x) (star y)<VAR>Hstar_left : ∀ (x y : A), p x y → p (star x) y<VAR>Hstar_right : ∀ (x y : A), p x y → p x (star y)<VAR>r : R<VAR>x : A<VAR>hx : x ∈ s ∪ star s<GOAL>p ((algebraMap R A) r) x
<VAR>F : Type u_1<VAR>R : Type u_2<VAR>A : Type u_3<VAR>B : Type u_4<VAR>inst✝⁹ : CommSemiring R<VAR>inst✝⁸ : StarRing R<VAR>inst✝⁷ : Semiring A<VAR>inst✝⁶ : Algebra R A<VAR>inst✝⁵ : StarRing A<VAR>inst✝⁴ : StarModule R A<VAR>inst✝³ : Semiring B<VAR>inst✝² : Algebra R B<VAR>inst✝¹ : StarRing B<VAR>inst✝ : StarModule R B<VAR>s : Set A<VAR>p : A → A → Prop<VAR>a b : A<VAR>ha : a ∈ adjoin R s<VAR>hb : b ∈ adjoin R s<VAR>Hs : ∀ x ∈ s, ∀ y ∈ s, p x y<VAR>Halg : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂)<VAR>Halg_left : ∀ (r : R), ∀ x ∈ s, p ((algebraMap R A) r) x<VAR>Halg_right : ∀ (r : R), ∀ x ∈ s, p x ((algebraMap R A) r)<VAR>Hadd_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ + x₂) y<VAR>Hadd_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ + y₂)<VAR>Hmul_left : ∀ (x₁ x₂ y : A), p x₁ y → p x₂ y → p (x₁ * x₂) y<VAR>Hmul_right : ∀ (x y₁ y₂ : A), p x y₁ → p x y₂ → p x (y₁ * y₂)<VAR>Hstar : ∀ (x y : A), p x y → p (star x) (star y)<VAR>Hstar_left : ∀ (x y : A), p x y → p (star x) y<VAR>Hstar_right : ∀ (x y : A), p x y → p x (star y)<VAR>r : R<VAR>x : A<VAR>hx : x ∈ s ∪ star s<GOAL>p x ((algebraMap R A) r)
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedAddCommGroup X<VAR>inst✝¹ : NormedSpace ℝ X<VAR>inst✝ : HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>hx : x ∈ ball c f.rOut<GOAL>↑f x ≠ 0
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>h0 : ↑a ≠ 0<GOAL>StrictMono fun x => ↑a * x
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>h0 : a ≠ 0<GOAL>StrictMono fun x => ↑a * x
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>h0 : a ≠ 0<VAR>x y : ℝ≥0∞<VAR>h : x < y<GOAL>(fun x => ↑a * x) x < (fun x => ↑a * x) y
<VAR>b c d : ℝ≥0∞<VAR>r p q a : ℝ≥0<VAR>h0 : a ≠ 0<VAR>x y : ℝ≥0∞<VAR>h : ↑a * y ≤ ↑a * x<GOAL>y ≤ x
<VAR>a b c d : Ordinal.{u}<GOAL>a ⨳ (b ⨳ c) ≤ d ↔ ∀ a' < a, ∀ b' < b, ∀ c' < c, a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>a b c d : Ordinal.{u}<GOAL>¬a ⨳ (b ⨳ c) ≤ d ↔ ¬∀ a' < a, ∀ b' < b, ∀ c' < c, a' ⨳ (b ⨳ c) ♯ a ⨳ (b' ⨳ c) ♯ a ⨳ (b ⨳ c') ♯ a' ⨳ (b' ⨳ c') < d ♯ a' ⨳ (b' ⨳ c) ♯ a' ⨳ (b ⨳ c') ♯ a ⨳ (b' ⨳ c')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>δ : Type u_1<VAR>ι : Sort x<VAR>l f f₁ f₂ : Filter α<VAR>g g₁ g₂ : Filter β<VAR>m : α → β<VAR>m' : β → γ<VAR>s : Set α<VAR>t : Set β<VAR>φ : α → β<VAR>θ : α → γ<VAR>ψ : β → δ<VAR>ρ : γ → δ<VAR>H : ψ ∘ φ = ρ ∘ θ<VAR>G : Filter δ<GOAL>comap φ (comap ψ G) = comap θ (comap ρ G)
<VAR>α : Type u_1<VAR>β✝ : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>x y : α<VAR>β : Type u_3<VAR>inst✝ : LinearOrder β<VAR>x' y' : β<VAR>h : cmp y x = cmp y' x'<GOAL>cmp x y = cmp x' y'
<VAR>α : Type u_1<VAR>inst✝ : CommMonoid α<VAR>x z d : α<VAR>h : IsRelPrime (x * d) z<GOAL>IsRelPrime x z