ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>ι' : Type v'<VAR>E : ι → Type wE<VAR>E₁ : ι → Type wE₁<VAR>E' : ι' → Type wE'<VAR>G : Type wG<VAR>G' : Type wG'<VAR>inst✝¹² : Fintype ι<VAR>inst✝¹¹ : Fintype ι'<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<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>inst✝⁵ : (i : ι') → SeminormedAddCommGroup (E' i)<VAR>inst✝⁴ : (i : ι') → NormedSpace 𝕜 (E' i)<VAR>inst✝³ : SeminormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>inst✝¹ : SeminormedAddCommGroup G'<VAR>inst✝ : NormedSpace 𝕜 G'<VAR>f✝ : MultilinearMap 𝕜 E G<VAR>k n : ℕ<VAR>f : MultilinearMap 𝕜 (fun x => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<VAR>C : ℝ<VAR>H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖<VAR>v : Fin k → G<GOAL>(∏ i : { x // x ∈ s }, ‖v ((s.orderIsoOfFin hk).symm i)‖) * ‖z‖ ^ (n - k) = (∏ a : { a // a ∈ s }, ‖v ((s.orderIsoOfFin hk).symm ⟨↑a, ⋯⟩)‖) * ‖z‖ ^ (n - k)
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>N : Type u_3<VAR>inst✝¹ : AddCommMonoid M<VAR>inst✝ : AddCommMonoid N<VAR>I₀ : WithTop (Box ι)<VAR>I✝ J : Box ι<VAR>i : ι<VAR>f : ι →ᵇᵃ[I₀] M<VAR>g : M →+ N<VAR>I : Box ι<VAR>hI : ↑I ≤ I₀<VAR>π : Prepartition I<VAR>hπ : π.IsPartition<GOAL>∑ Ji ∈ π.boxes, (⇑g ∘ ⇑f) Ji = (⇑g ∘ ⇑f) I
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (riemannZeta s))
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>Tendsto (fun n => ∏ p ∈ n.primesBelow, (1 - ↑p ^ (-s))⁻¹) atTop (𝓝 (∑' (n : ℕ), (riemannZetaSummandHom ⋯) n))
<VAR>α : Type u_1<VAR>N : α → Type u_2<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : (a : α) → DecidableEq (N a)<VAR>inst✝ : (a : α) → AddGroup (N a)<VAR>f f₁ f₂ g g₁ g₂ : Π₀ (a : α), N a<GOAL>(f - g₁).neLocus (f - g₂) = g₁.neLocus g₂
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : Convex ℝ s<VAR>h0 : μ t ≠ 0<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : Convex ℝ s<VAR>h0 : μ (toMeasurable μ t) ≠ 0<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>ht : ⨍ (x : α) in t, f x ∂μ ∈ interior s<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : Convex ℝ s<VAR>h0 : μ (toMeasurable μ t) ≠ 0<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁶ : NormedAddCommGroup E<VAR>inst✝⁵ : NormedSpace ℝ E<VAR>inst✝⁴ : CompleteSpace E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace ℝ F<VAR>inst✝¹ : CompleteSpace F<VAR>μ : Measure α<VAR>s : Set E<VAR>t : Set α<VAR>f : α → E<VAR>g : E → ℝ<VAR>C : ℝ<VAR>inst✝ : IsFiniteMeasure μ<VAR>hs : Convex ℝ s<VAR>h0 : μ (toMeasurable μ t) ≠ 0<VAR>hfs : ∀ᵐ (x : α) ∂μ, f x ∈ s<VAR>hfi : Integrable f μ<VAR>ht : ⨍ (x : α) in toMeasurable μ t, f x ∂μ ∈ interior s<VAR>h0' : ¬μ (toMeasurable μ t)ᶜ = 0<GOAL>⨍ (x : α), f x ∂μ ∈ interior s
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>N : Type u_3<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : Module R M<VAR>inst✝¹ : AddCommGroup N<VAR>inst✝ : Module R N<VAR>p : PerfectPairing R M N<VAR>x : M<VAR>f : Dual R M<GOAL>(p.toDualRight.symm.dualMap (p.toDualLeft x)) f = ((Dual.eval R M) x) f
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝ : InvolutiveInv α<VAR>s✝ t : Set α<VAR>a✝ a : α<VAR>s : Set α<GOAL>(insert a s)⁻¹ = insert a⁻¹ s⁻¹
<VAR>α : Type u<VAR>β : Type u_1<VAR>t : TopologicalSpace α<VAR>B : Set (Set α)<VAR>s : Set α<VAR>inst✝ : DiscreteTopology α<GOAL>SeparableSpace α ↔ Countable α
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝² : Semiring R<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero N<VAR>n : N<VAR>i : ι<VAR>a : η i<VAR>j : ι<VAR>b : η j<VAR>h : ¬i = j<GOAL>((sigmaFinsuppEquivDFinsupp (single ⟨i, a⟩ n)) j) b = ((DFinsupp.single ⟨i, a⟩.fst (single ⟨i, a⟩.snd n)) j) b
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝² : Semiring R<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero N<VAR>n : N<VAR>i : ι<VAR>a : η i<VAR>j : ι<VAR>b : η j<VAR>h : ¬i = j<GOAL>(single ⟨i, a⟩ n) ⟨j, b⟩ = 0
<VAR>ι : Type u_1<VAR>R : Type u_2<VAR>M : Type u_3<VAR>η : ι → Type u_4<VAR>N : Type u_5<VAR>inst✝² : Semiring R<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : Zero N<VAR>n : N<VAR>i : ι<VAR>a : η i<VAR>j : ι<VAR>b : η j<VAR>h : ¬i = j<VAR>H : ⟨i, a⟩ ≠ ⟨j, b⟩<GOAL>(single ⟨i, a⟩ n) ⟨j, b⟩ = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝² : Preorder α<VAR>inst✝¹ : TopologicalSpace α<VAR>inst✝ : IsScott α<VAR>s : Set α<VAR>a : α<GOAL>IsClosed s ↔ IsLowerSet s ∧ DirSupClosed s
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : CauchySeq u<VAR>f g : ℕ → ℕ<VAR>hf : Tendsto f atTop atTop<VAR>hg : Tendsto g atTop atTop<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
<VAR>α : Type u<VAR>β : Type v<VAR>uniformSpace : UniformSpace α<VAR>V : ℕ → Set (α × α)<VAR>hV : ∀ (n : ℕ), V n ∈ 𝓤 α<VAR>u : ℕ → α<VAR>hu : Tendsto (Prod.map u u) atTop (𝓤 α)<VAR>f g : ℕ → ℕ<VAR>hf : Tendsto f atTop atTop<VAR>hg : Tendsto g atTop atTop<GOAL>∃ φ, StrictMono φ ∧ ∀ (n : ℕ), ((u ∘ f ∘ φ) n, (u ∘ g ∘ φ) n) ∈ V n
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>inst✝⁴ : DivisionRing K<VAR>inst✝³ : AddCommGroup V<VAR>inst✝² : AddCommGroup V'<VAR>inst✝¹ : Module K V<VAR>inst✝ : Module K V'<VAR>v✝ : ι → V<VAR>s t : Set V<VAR>x y z : V<VAR>n : ℕ<VAR>v : Fin (n + 1) → V<GOAL>LinearIndependent K v ↔ LinearIndependent K (Fin.init v) ∧ v (Fin.last n) ∉ span K (range (Fin.init v))
<VAR>α : Type u_1<VAR>inst✝² : TopologicalSpace α<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>f : ℝ → ℂ<VAR>x : ℝ<VAR>f' : ℂ<VAR>h₁ : HasStrictDerivAt f f' x<VAR>h₂ : f x ∈ slitPlane<GOAL>HasStrictDerivAt (fun t => log (f t)) (f' / f x) x
<VAR>R : Type u<VAR>M : Type u_1<VAR>Mp : Type u_2<VAR>Rp : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : CommRing Rp<VAR>inst✝⁶ : Algebra R Rp<VAR>inst✝⁵ : AddCommGroup Mp<VAR>inst✝⁴ : Module R Mp<VAR>inst✝³ : Module Rp Mp<VAR>inst✝² : IsScalarTower R Rp Mp<VAR>f✝ : M →ₗ[R] Mp<VAR>inst✝¹ : Flat R M<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S Rp<VAR>f : M →ₗ[R] Mp<VAR>h : IsLocalizedModule S f<GOAL>Flat Rp Mp
<VAR>R : Type u<VAR>M : Type u_1<VAR>Mp : Type u_2<VAR>Rp : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : CommRing Rp<VAR>inst✝⁶ : Algebra R Rp<VAR>inst✝⁵ : AddCommGroup Mp<VAR>inst✝⁴ : Module R Mp<VAR>inst✝³ : Module Rp Mp<VAR>inst✝² : IsScalarTower R Rp Mp<VAR>f✝ : M →ₗ[R] Mp<VAR>inst✝¹ : Flat R M<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S Rp<VAR>f : M →ₗ[R] Mp<VAR>h : IsLocalizedModule S f<GOAL>IsBaseChange Rp ?m.190213
<VAR>R : Type u<VAR>M : Type u_1<VAR>Mp : Type u_2<VAR>Rp : Type v<VAR>inst✝¹⁰ : CommRing R<VAR>inst✝⁹ : AddCommGroup M<VAR>inst✝⁸ : Module R M<VAR>inst✝⁷ : CommRing Rp<VAR>inst✝⁶ : Algebra R Rp<VAR>inst✝⁵ : AddCommGroup Mp<VAR>inst✝⁴ : Module R Mp<VAR>inst✝³ : Module Rp Mp<VAR>inst✝² : IsScalarTower R Rp Mp<VAR>f✝ : M →ₗ[R] Mp<VAR>inst✝¹ : Flat R M<VAR>S : Submonoid R<VAR>inst✝ : IsLocalization S Rp<VAR>f : M →ₗ[R] Mp<VAR>h : IsLocalizedModule S f<GOAL>M →ₗ[R] Mp
<VAR>τ : ℍ<GOAL>jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ
<VAR>τ : ℍ<GOAL>↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
<VAR>τ : ℍ<VAR>this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2<GOAL>↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
<VAR>τ : ℍ<VAR>this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2<GOAL>↑↑2 + ↑τ = 2 + ↑τ
<VAR>b n : ℕ<GOAL>log b (n / b * b) = log b n
<VAR>b n : ℕ<VAR>hb : b ≤ 1<GOAL>log b (n / b * b) = log b n
<VAR>b n : ℕ<VAR>hb : 1 < b<GOAL>log b (n / b * b) = log b n
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>h : n < b<GOAL>log b (n / b * b) = log b n
<VAR>b n : ℕ<VAR>hb : 1 < b<VAR>h : b ≤ n<GOAL>log b (n / b * b) = log b n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>s : Set β<GOAL>eLpNorm (fun x => κ.density ν a x s) 1 (ν a) ≤ (ν a) univ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>s : Set β<VAR>t : γ<GOAL>‖κ.density ν a t s‖ ≤ 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>mγ : MeasurableSpace γ<VAR>inst✝ : CountablyGenerated γ<VAR>κ : Kernel α (γ × β)<VAR>ν : Kernel α γ<VAR>hκν : κ.fst ≤ ν<VAR>a : α<VAR>s : Set β<GOAL>(ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Surjective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>z : Q<GOAL>∃ a, (f.map ⋯ k) a = z
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Surjective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>y : P<VAR>s : M<VAR>hs : s ∈ ↑S<GOAL>∃ a, (f.map ⋯ k) a = k.mk' y ⟨g s, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Surjective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>s : M<VAR>hs : s ∈ ↑S<VAR>x : M<GOAL>∃ a, (f.map ⋯ k) a = k.mk' (g x) ⟨g s, ⋯⟩
<VAR>M : Type u_1<VAR>inst✝³ : CommMonoid M<VAR>S : Submonoid M<VAR>N : Type u_2<VAR>inst✝² : CommMonoid N<VAR>P : Type u_3<VAR>inst✝¹ : CommMonoid P<VAR>f : S.LocalizationMap N<VAR>g : M →* P<VAR>hg✝ : ∀ (y : ↥S), IsUnit (g ↑y)<VAR>T : Submonoid P<VAR>hy : ∀ (y : ↥S), g ↑y ∈ T<VAR>Q : Type u_4<VAR>inst✝ : CommMonoid Q<VAR>k✝ : T.LocalizationMap Q<VAR>hg : Surjective ⇑g<VAR>k : (Submonoid.map g S).LocalizationMap Q<VAR>s : M<VAR>hs : s ∈ ↑S<VAR>x : M<GOAL>(f.map ⋯ k) (f.mk' x ⟨s, hs⟩) = k.mk' (g x) ⟨g s, ⋯⟩
<VAR>α : Type u<VAR>inst✝ : Infinite α<VAR>K : Type u := FractionRing (MvPolynomial α (ULift.{u, 0} ℚ))<GOAL>Nonempty (Field α)
<VAR>α : Type u<VAR>inst✝ : Infinite α<VAR>K : Type u := FractionRing (MvPolynomial α (ULift.{u, 0} ℚ))<GOAL>#α = #K
<VAR>α : Type u<VAR>inst✝ : Infinite α<VAR>K : Type u := FractionRing (MvPolynomial α (ULift.{u, 0} ℚ))<GOAL>#α = #(MvPolynomial α (ULift.{u, 0} ℚ))
<VAR>α : Type u<VAR>inst✝ : Infinite α<VAR>K : Type u := FractionRing (MvPolynomial α (ULift.{u, 0} ℚ))<GOAL>#α ≤ #(MvPolynomial α (ULift.{u, 0} ℚ))
<VAR>α : Type u<VAR>inst✝ : Infinite α<VAR>K : Type u := FractionRing (MvPolynomial α (ULift.{u, 0} ℚ))<GOAL>#(MvPolynomial α (ULift.{u, 0} ℚ)) ≤ #α
<VAR>R : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>δ : Type u_4<VAR>γ : Type u_5<VAR>ι : Type u_6<VAR>m0 : MeasurableSpace α<VAR>inst✝¹ : MeasurableSpace β<VAR>inst✝ : MeasurableSpace γ<VAR>μ μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α<VAR>s✝ s' t : Set α<VAR>S : Set ι<VAR>s : ι → Set α<VAR>hc : S.Countable<VAR>hs : ⋃ i ∈ S, s i = univ<GOAL>μ = ν ↔ ∀ i ∈ S, μ.restrict (s i) = ν.restrict (s i)
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>v : E<GOAL>Tendsto (fun c => c • (f (x + c⁻¹ • v) - f x)) atTop (𝓝 (f' v))
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>v : E<GOAL>Tendsto (fun n => ‖n‖) atTop atTop
<VAR>E : Type u_1<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : NormedSpace ℝ F<VAR>f : E → F<VAR>f' : E →L[ℝ] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>v : E<GOAL>∀ (b : ℝ), ∃ i, ∀ (a : ℝ), i ≤ a → b ≤ ‖a‖
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝³ : TopologicalSpace X<VAR>m : MeasurableSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : T2Space Y<VAR>μ ν : Measure X<VAR>inst✝ : μ.IsOpenPosMeasure<VAR>s U F : Set X<VAR>x : X<VAR>hF : IsClosed F<VAR>h : F =ᶠ[ae μ] univ<GOAL>F = univ
<VAR>k : Type u₁<VAR>G : Type u₂<VAR>H : Type u_1<VAR>R : Type u_2<VAR>inst✝¹ : Semiring k<VAR>inst✝ : Mul G<VAR>a b : G<GOAL>(fun a => single a 1) (a * b) = (fun a => single a 1) a * (fun a => single a 1) b
<VAR>C : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} C<VAR>inst✝³ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>φ : S₁ ⟶ S₂<VAR>h : S₂.RightHomologyData<VAR>inst✝² : Epi φ.τ₁<VAR>inst✝¹ : IsIso φ.τ₂<VAR>inst✝ : Mono φ.τ₃<GOAL>(ofEpiOfIsIsoOfMono' φ h).g' ≫ φ.τ₃ = h.g'
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>R : Cᵒᵖ ⥤ RingCat<VAR>P : PresheafOfModules R<VAR>X : Cᵒᵖ<VAR>x✝ : ↑(P.obj X)<GOAL>(P.map (𝟙 X)) x✝ = id' x✝
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<VAR>J : ↥(Ideal (𝓞 K))⁰<VAR>hJ : ClassGroup.mk0 J = C⁻¹<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<VAR>J : ↥(Ideal (𝓞 K))⁰<VAR>hJ : ClassGroup.mk0 J = C⁻¹<VAR>a : 𝓞 K<VAR>ha : a ∈ ↑↑J<VAR>h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<VAR>J : ↥(Ideal (𝓞 K))⁰<VAR>hJ : ClassGroup.mk0 J = C⁻¹<VAR>a : 𝓞 K<VAR>ha : a ∈ ↑↑J<VAR>h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<VAR>I₀ : Ideal (𝓞 K)<VAR>hI : Ideal.span {a} = ↑J * I₀<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<VAR>J : ↥(Ideal (𝓞 K))⁰<VAR>hJ : ClassGroup.mk0 J = C⁻¹<VAR>a : 𝓞 K<VAR>ha : a ∈ ↑↑J<VAR>h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<VAR>I₀ : Ideal (𝓞 K)<VAR>hI : Ideal.span {a} = ↑J * I₀<VAR>this : I₀ ≠ 0<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>K : Type u_1<VAR>inst✝¹ : Field K<VAR>inst✝ : NumberField K<VAR>C : ClassGroup (𝓞 K)<VAR>J : ↥(Ideal (𝓞 K))⁰<VAR>hJ : ClassGroup.mk0 J = C⁻¹<VAR>a : 𝓞 K<VAR>ha : a ∈ ↑↑J<VAR>h_nz : (Algebra.linearMap (𝓞 K) K) a ≠ 0<VAR>h_nm : ↑|(Algebra.norm ℚ) ((Algebra.linearMap (𝓞 K) K) a)| ≤ ↑(FractionalIdeal.absNorm ↑((FractionalIdeal.mk0 K) J)) * (4 / π) ^ NrComplexPlaces K * ↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|<VAR>I₀ : Ideal (𝓞 K)<VAR>hI : Ideal.span {a} = ↑J * I₀<VAR>this : I₀ ≠ 0<VAR>I : ↥(Ideal (𝓞 K))⁰ := ⟨I₀, ⋯⟩<GOAL>∃ I, ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ (4 / π) ^ NrComplexPlaces K * (↑(finrank ℚ K).factorial / ↑(finrank ℚ K) ^ finrank ℚ K * √|↑(discr K)|)
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<VAR>h : ↑n ≠ 0<GOAL>(W.preΨ n).leadingCoeff = ↑(if Even n then n / 2 else n)
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>n : ℕ<GOAL>(X ^ n - 1).Separable ↔ ↑n ≠ 0
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>n : ℕ<GOAL>(X ^ n - 1).Separable → ↑n ≠ 0
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>n : ℕ<GOAL>(∃ a b, a * (X ^ n - 1) + b * (C ↑n * X ^ (n - 1)) = 1) → ↑n ≠ 0
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>h : IsCoprime (X ^ n - 1) (C ↑n * X ^ (n - 1))<VAR>hn' : ↑n = 0<GOAL>False
<VAR>F : Type u<VAR>inst✝¹ : Field F<VAR>K : Type v<VAR>inst✝ : Field K<VAR>n : ℕ<VAR>h : IsUnit (X ^ n - 1)<VAR>hn' : ↑n = 0<GOAL>False
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s : Multiset ι<VAR>f : ι → R[X]<GOAL>derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<GOAL>derivative (Multiset.map f (i ::ₘ s)).prod = (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) (i ::ₘ s)).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<GOAL>(Multiset.map f s).prod * derivative (f i) + f i * derivative (Multiset.map f s).prod = (Multiset.map f s).prod * derivative (f i) + (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<GOAL>f i * derivative (Multiset.map f s).prod = (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<GOAL>(Multiset.map (HMul.hMul (f i)) (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s)).sum = (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<GOAL>(Multiset.map (fun x => f i * ((Multiset.map f (s.erase x)).prod * derivative (f x))) s).sum = (Multiset.map (fun i_1 => (Multiset.map f ((i ::ₘ s).erase i_1)).prod * derivative (f i_1)) s).sum
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<VAR>j : ι<VAR>hj : j ∈ s<GOAL>f i * ((Multiset.map f (s.erase j)).prod * derivative (f j)) = (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>A : Type z<VAR>a b : R<VAR>n : ℕ<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : DecidableEq ι<VAR>s✝ : Multiset ι<VAR>f : ι → R[X]<VAR>i : ι<VAR>s : Multiset ι<VAR>h : derivative (Multiset.map f s).prod = (Multiset.map (fun i => (Multiset.map f (s.erase i)).prod * derivative (f i)) s).sum<VAR>j : ι<VAR>hj : j ∈ s<GOAL>(Multiset.map f (i ::ₘ s.erase j)).prod * derivative (f j) = (Multiset.map f ((i ::ₘ s).erase j)).prod * derivative (f j)
<VAR>X✝ Y : Scheme<VAR>f : X✝ ⟶ Y<VAR>Z X : Scheme<VAR>U : X.Opens<VAR>hU : IsCompact ↑U<VAR>s : Set ↑Γ(X, U)<GOAL>X.zeroLocus s = ⊤ ↔ s ⊆ ↑(nilradical ↑Γ(X, U))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s t : Finset α<GOAL>s.card * t.card ≤ (s \\ t).card * (t \\ s).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : DecidableEq α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>s t : Finset α<VAR>this : ∀ (s t : Finset α), map { toFun := ⇑liftLatticeHom, inj' := ⋯ } (s \\ t) = map { toFun := ⇑liftLatticeHom, inj' := ⋯ } s \\ map { toFun := ⇑liftLatticeHom, inj' := ⋯ } t<GOAL>s.card * t.card ≤ (s \\ t).card * (t \\ s).card
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : t.Infinite<VAR>hst : s ⊆ t<VAR>hs : s.Finite<VAR>k : ℕ<VAR>hsk : s.ncard ≤ k<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>s✝ t✝ : Set α<VAR>f : α → β<VAR>s t : Set α<VAR>ht : t.Infinite<VAR>hst : s ⊆ t<VAR>hs : s.Finite<VAR>k : ℕ<VAR>hsk : s.ncard ≤ k<VAR>s₁ : Set α<VAR>hs₁ : s₁ ⊆ t \ s<VAR>hs₁fin : s₁.Finite<VAR>hs₁card : s₁.ncard = k - s.ncard<GOAL>∃ s', s ⊆ s' ∧ s' ⊆ t ∧ s'.ncard = k