ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>X : Type u_1<VAR>ι : Type u_2<VAR>inst✝ : PseudoMetricSpace α<VAR>x y z : α<VAR>δ ε ε₁ ε₂ : ℝ<VAR>s : Set α<VAR>h : y ∈ ball x ε<GOAL>dist y x ≤ ε - (ε - dist y x)
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>inst✝¹² : Category.{v₁, u₁} C<VAR>inst✝¹¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝¹⁰ : Category.{v₃, u₃} E<VAR>L : C ⥤ D<VAR>W : MorphismProperty C<VAR>inst✝⁹ : L.IsLocalization W<VAR>A : Type w<VAR>inst✝⁸ : AddMonoid A<VAR>inst✝⁷ : HasShift C A<VAR>inst✝⁶ : W.IsCompatibleWithShift A<VAR>inst✝⁵ : W.HasLocalization<VAR>F : C ⥤ E<VAR>F' : D ⥤ E<VAR>inst✝⁴ : Lifting L W F F'<VAR>inst✝³ : HasShift D A<VAR>inst✝² : HasShift E A<VAR>inst✝¹ : L.CommShift A<VAR>inst✝ : F.CommShift A<VAR>a : A<VAR>X : C<GOAL>(F'.commShiftIso a).inv.app (L.obj X) = (shiftFunctor E a).map ((Lifting.iso L W F F').hom.app X) ≫ (F.commShiftIso a).inv.app X ≫ (Lifting.iso L W F F').inv.app ((shiftFunctor C a).obj X) ≫ F'.map ((L.commShiftIso a).hom.app X)
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>x1 x2 : X<VAR>h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2<GOAL>x1 = x2
<VAR>X : Type u_1<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : T0Space X<VAR>x1 x2 : X<VAR>h : (productOfMemOpens X) x1 = (productOfMemOpens X) x2<GOAL>Inseparable x1 x2
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ conts, (of v).conts n = Pair.map Rat.cast conts
<VAR>K : Type u_1<VAR>inst✝¹ : LinearOrderedField K<VAR>inst✝ : FloorRing K<VAR>v : K<VAR>n : ℕ<GOAL>∃ conts, (of v).contsAux (n + 1) = Pair.map Rat.cast conts
<VAR>z τ : ℂ<GOAL>jacobiTheta₂' z (τ + 2) = jacobiTheta₂' z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>jacobiTheta₂'_term n z (τ + 2) = jacobiTheta₂'_term n z τ
<VAR>z τ : ℂ<VAR>n : ℤ<GOAL>2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * (τ + 2))) = 2 * ↑π * I * ↑n * (cexp (2 * ↑π * I * ↑n * z) * cexp (↑π * I * ↑n ^ 2 * τ))
<VAR>α : Type u_1<VAR>s✝ t : Set α<VAR>a : α<VAR>inst✝¹ : Group α<VAR>inst✝ : StarMul α<VAR>s : Set α<VAR>x✝ : α<GOAL>x✝ ∈ s⁻¹⋆ ↔ x✝ ∈ s⋆⁻¹
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W' : Jacobian R<VAR>F : Type v<VAR>inst✝ : Field F<VAR>W : Jacobian F<VAR>P Q : Fin 3 → R<VAR>hP : W'.Equation P<VAR>hQ : W'.Equation Q<VAR>hx : P x * Q z ^ 2 = Q x * P z ^ 2<GOAL>W'.addX P Q * (P z * Q z) ^ 2 = (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>f g : Filter α<VAR>s : Set α<VAR>a✝ a : α<GOAL>(pure a).ker = {a}
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>n : ℕ∞<VAR>hc : DifferentiableAt ℝ c a<VAR>hR : DifferentiableAt ℝ R a<VAR>hx : DifferentiableAt ℝ x a<VAR>hne : x a ≠ c a<GOAL>DifferentiableAt ℝ (fun a => inversion (c a) (R a) (x a)) a
<VAR>E : Type u_1<VAR>F : Type u_2<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>c x : E → F<VAR>R : E → ℝ<VAR>s : Set E<VAR>a : E<VAR>n : ℕ∞<VAR>hc : DifferentiableWithinAt ℝ c univ a<VAR>hR : DifferentiableWithinAt ℝ R univ a<VAR>hx : DifferentiableWithinAt ℝ x univ a<VAR>hne : x a ≠ c a<GOAL>DifferentiableWithinAt ℝ (fun a => inversion (c a) (R a) (x a)) univ a
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : x.norm.natAbs = 1<VAR>hx : 0 ≤ x.norm<GOAL>1 = x * star x
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : x.norm.natAbs = 1<VAR>hx : x.norm ≤ 0<GOAL>1 = x * -star x
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : IsUnit x<GOAL>x.norm.natAbs = 1
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : IsUnit x<VAR>y : ℤ√d<VAR>hy : 1 = x * y<GOAL>x.norm.natAbs = 1
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : IsUnit x<VAR>y : ℤ√d<VAR>hy : 1 = x * y<VAR>this : (Int.natAbs ∘ norm) 1 = (Int.natAbs ∘ norm) (x * y)<GOAL>x.norm.natAbs = 1
<VAR>d : ℤ<VAR>x : ℤ√d<VAR>h : IsUnit x<VAR>y : ℤ√d<VAR>hy : 1 = x * y<VAR>this : x.norm.natAbs = 1 ∧ y.norm.natAbs = 1<GOAL>x.norm.natAbs = 1
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>x y : ZMod N<VAR>hxy : toAddCircle x = toAddCircle y<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>B : Type u_2<VAR>N : ℕ<VAR>inst✝ : NeZero N<VAR>x y : ZMod N<VAR>hxy : toAddCircle x = toAddCircle y<VAR>this : 0 < ↑N<GOAL>x = y
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝ : CommMonoid α<VAR>s : Finset α<GOAL>s.val.prod = s.prod id
<VAR>G : Type u_1<VAR>G'✝ : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'✝<VAR>f✝ : G →* G'✝<VAR>G' : Type u_3<VAR>G'' : Type u_4<VAR>inst✝¹ : Group G'<VAR>inst✝ : Group G''<VAR>f : G' →* G<VAR>g : G →* G''<VAR>hfg : g.ker ≤ f.range<VAR>hG' : IsSolvable G'<VAR>hG'' : IsSolvable G''<VAR>n : ℕ<VAR>hn : derivedSeries G'' n = ⊥<VAR>m : ℕ<VAR>hm : derivedSeries G' m = ⊥<GOAL>IsSolvable G
<VAR>G : Type u_1<VAR>G'✝ : Type u_2<VAR>inst✝³ : Group G<VAR>inst✝² : Group G'✝<VAR>f✝ : G →* G'✝<VAR>G' : Type u_3<VAR>G'' : Type u_4<VAR>inst✝¹ : Group G'<VAR>inst✝ : Group G''<VAR>f : G' →* G<VAR>g : G →* G''<VAR>hfg : g.ker ≤ f.range<VAR>hG' : IsSolvable G'<VAR>hG'' : IsSolvable G''<VAR>n : ℕ<VAR>hn : derivedSeries G'' n = ⊥<VAR>m : ℕ<VAR>hm : derivedSeries G' m = ⊥<GOAL>derivedSeries G (n + m) ≤ map f (derivedSeries G' m)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>hL : L < ∫⁻ (x : α), ↑(f x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>hL : ∃ i, ∃ (_ : ∀ (x : α), ↑(↑i x) ≤ ↑(f x)), L < (SimpleFunc.map ofNNReal i).lintegral μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>g₀ : α →ₛ ℝ≥0<VAR>hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)<VAR>g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>g₀ : α →ₛ ℝ≥0<VAR>hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)<VAR>g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ<VAR>h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>m✝ m0 : MeasurableSpace α<VAR>E : Type u_5<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : OpensMeasurableSpace E<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝ : SigmaFinite μ<VAR>f : α → ℝ≥0<VAR>L : ℝ≥0∞<VAR>g₀ : α →ₛ ℝ≥0<VAR>hg₀ : ∀ (x : α), ↑(↑g₀ x) ≤ ↑(f x)<VAR>g₀L : L < (SimpleFunc.map ofNNReal g₀).lintegral μ<VAR>h'L : L < ∫⁻ (x : α), ↑(↑g₀ x) ∂μ<VAR>g : α →ₛ ℝ≥0<VAR>hg : ∀ (x : α), ↑g x ≤ ↑g₀ x<VAR>gL : ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤<VAR>gtop : L < ∫⁻ (x : α), ↑(↑g x) ∂μ<GOAL>∃ g, (∀ (x : α), ↑g x ≤ f x) ∧ ∫⁻ (x : α), ↑(↑g x) ∂μ < ⊤ ∧ L < ∫⁻ (x : α), ↑(↑g x) ∂μ
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) ((inv ((linearization k G).μ (Action.leftRegular G) { V := Fin n → G, ρ := 1 })).hom ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) = single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) (↑(finsuppTensorFinsupp' k (Action.leftRegular G).V (Fin n → G)).symm ((lmapDomain k k (actionDiagonalSucc G n).hom.hom) (single f a))) = single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) ((finsuppTensorFinsupp k k k k (Action.leftRegular G).V (Fin n → G)).symm ((lcongr (Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) (TensorProduct.lid k k).symm) (single ((actionDiagonalSucc G n).hom.hom f) a))) = single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) ((finsuppTensorFinsupp k k k k (Action.leftRegular G).V (Fin n → G)).symm (single ((Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) ((actionDiagonalSucc G n).hom.hom f)) ((TensorProduct.lid k k).symm a))) = single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>k G : Type u<VAR>inst✝¹ : CommRing k<VAR>n : ℕ<VAR>inst✝ : Group G<VAR>f : Fin (n + 1) → G<VAR>a : k<GOAL>(𝟙 ((linearization k G).obj (Action.leftRegular G)).V ⊗ (linearizationTrivialIso k G (Fin n → G)).hom.hom) (single ((Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).1 1 ⊗ₜ[k] single ((Equiv.refl ((Action.leftRegular G).V × (Fin n → G))) (f 0, fun i => (f i.castSucc)⁻¹ * f i.succ)).2 a) = single (f 0) 1 ⊗ₜ[k] single (fun i => (f i.castSucc)⁻¹ * f i.succ) a
<VAR>s : ℂ<GOAL>s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ
<VAR>s : ℂ<GOAL>↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) = 2 * (2 * ↑π) ^ (-s) * Gamma s
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedAddCommGroup α<VAR>hα : Archimedean α<VAR>p : α<VAR>hp : 0 < p<VAR>a✝ b✝ c : α<VAR>n : ℤ<VAR>a b : α<GOAL>toIocMod hp a (b + p) = toIocMod hp a b
<VAR>F : Type u_1<VAR>ι : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>inst✝¹ : AddGroupWithOne α<VAR>inst✝ : CharZero α<VAR>m n : ℤ<VAR>h : n = 0<GOAL>↑n = 0
<VAR>E : Type u_1<VAR>𝕜 : Type u_2<VAR>inst✝⁷ : NontriviallyNormedField 𝕜<VAR>inst✝⁶ : CompleteSpace 𝕜<VAR>inst✝⁵ : AddCommGroup E<VAR>inst✝⁴ : Module 𝕜 E<VAR>inst✝³ : Nontrivial E<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul 𝕜 E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>h's : s.Nonempty<GOAL>𝔠 ≤ #↑s
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>(f a + f b).succ * multinomial {a, b} f = (f a).succ * multinomial {a, b} (Function.update f a (f a).succ)
<VAR>α : Type u_1<VAR>s : Finset α<VAR>f : α → ℕ<VAR>a b : α<VAR>n : ℕ<VAR>inst✝ : DecidableEq α<VAR>h : a ≠ b<GOAL>(f a + f b).succ * (f a + f b).choose (f a) = ((f a).succ + f b).choose (f a).succ * (f a).succ
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DivisionMonoid α<VAR>s✝ t s : Finset α<VAR>n : ℕ<GOAL>↑(s ^ Int.negSucc n) = ↑s ^ Int.negSucc n
<VAR>F : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>γ : Type u_4<VAR>inst✝² : DecidableEq α<VAR>inst✝¹ : DecidableEq β<VAR>inst✝ : DivisionMonoid α<VAR>s✝ t s : Finset α<VAR>n : ℕ<GOAL>(↑(npowRec n.succ s))⁻¹ = ↑s ^ Int.negSucc n
<VAR>n : Type u_1<VAR>R : Type u_2<VAR>inst✝² : DecidableEq n<VAR>inst✝¹ : Fintype n<VAR>σ : Perm n<VAR>inst✝ : AddCommMonoidWithOne R<GOAL>∑ i : n, (Perm.permMatrix R σ).diag i = ↑(Function.fixedPoints ⇑σ).ncard
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>r : α → β → Prop<VAR>f : α →ₛ β<VAR>h : ∀ (b : β), MeasurableSet {a | r a b}<GOAL>MeasurableSet {a | r a (↑f a)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>r : α → β → Prop<VAR>f : α →ₛ β<VAR>h : ∀ (b : β), MeasurableSet {a | r a b}<VAR>this : {a | r a (↑f a)} = ⋃ b ∈ range ↑f, {a | r a b} ∩ ↑f ⁻¹' {b}<GOAL>MeasurableSet {a | r a (↑f a)}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>δ : Type u_4<VAR>inst✝ : MeasurableSpace α<VAR>r : α → β → Prop<VAR>f : α →ₛ β<VAR>h : ∀ (b : β), MeasurableSet {a | r a b}<VAR>this : {a | r a (↑f a)} = ⋃ b ∈ range ↑f, {a | r a b} ∩ ↑f ⁻¹' {b}<GOAL>MeasurableSet (⋃ b ∈ range ↑f, {a | r a b} ∩ ↑f ⁻¹' {b})
<VAR>K L : Type<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : IsAlgClosed K<VAR>inst✝³ : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>this✝ : Algebra (ZMod p) K := ZMod.algebra K p<VAR>this : Algebra (ZMod p) L := ZMod.algebra L p<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : IsAlgClosed K<VAR>inst✝³ : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>this✝ : Algebra (ZMod p) K := ZMod.algebra K p<VAR>this : Algebra (ZMod p) L := ZMod.algebra L p<VAR>s : Set K<VAR>hs : IsTranscendenceBasis (ZMod p) Subtype.val<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : IsAlgClosed K<VAR>inst✝³ : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>this✝ : Algebra (ZMod p) K := ZMod.algebra K p<VAR>this : Algebra (ZMod p) L := ZMod.algebra L p<VAR>s : Set K<VAR>hs : IsTranscendenceBasis (ZMod p) Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis (ZMod p) Subtype.val<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : IsAlgClosed K<VAR>inst✝³ : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p<VAR>this✝ : Algebra (ZMod p) L := ZMod.algebra L p<VAR>s : Set K<VAR>hs : IsTranscendenceBasis (ZMod p) Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis (ZMod p) Subtype.val<VAR>this : #↑s = #↑t<GOAL>Nonempty (K ≃+* L)
<VAR>K L : Type<VAR>inst✝⁶ : Field K<VAR>inst✝⁵ : Field L<VAR>inst✝⁴ : IsAlgClosed K<VAR>inst✝³ : IsAlgClosed L<VAR>p : ℕ<VAR>inst✝² : Fact (Nat.Prime p)<VAR>inst✝¹ : CharP K p<VAR>inst✝ : CharP L p<VAR>hK : ℵ₀ < #K<VAR>hKL : #K = #L<VAR>this✝¹ : Algebra (ZMod p) K := ZMod.algebra K p<VAR>this✝ : Algebra (ZMod p) L := ZMod.algebra L p<VAR>s : Set K<VAR>hs : IsTranscendenceBasis (ZMod p) Subtype.val<VAR>t : Set L<VAR>ht : IsTranscendenceBasis (ZMod p) Subtype.val<VAR>this : #↑s = #↑t<VAR>e : ↑s ≃ ↑t<GOAL>Nonempty (K ≃+* L)
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>f : R<VAR>n : ℕ<VAR>hn : 0 < n<VAR>x : PrimeSpectrum R<GOAL>x ∈ zeroLocus {f ^ n} ↔ x ∈ zeroLocus {f}
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<VAR>h : r ∈ Icc 0 1<GOAL>dist (r • x + (1 - r) • y) x = ‖1 - r‖ * ‖x - y‖
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<VAR>h : r ∈ Icc 0 1<GOAL>‖1 - r‖ * ‖x - y‖ = (1 - r) * dist y x
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<VAR>h : r ∈ Icc 0 1<GOAL>0 ≤ r
<VAR>E : Type u_1<VAR>inst✝¹ : SeminormedAddCommGroup E<VAR>inst✝ : NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<VAR>h : r ∈ Icc 0 1<GOAL>(1 - 0) * dist y x = dist y x
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>ι : Type y<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q r : R[X]<VAR>inst✝ : Semiring S<VAR>f✝ f : R →+* S<VAR>p : R[X]<GOAL>eval 1 (map f p) = f (eval 1 p)
<VAR>p n b k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>∑ i ∈ Ico 1 b, n / p ^ i = ∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i
<VAR>p n b k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>∑ i ∈ Ico 1 b, (k + (n - k)) / p ^ i = ∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0)
<VAR>p n b k : ℕ<VAR>hp : Prime p<VAR>hkn : k ≤ n<GOAL>∑ i ∈ Ico 1 b, (k / p ^ i + (n - k) / p ^ i + if p ^ i ≤ k % p ^ i + (n - k) % p ^ i then 1 else 0) = ∑ i ∈ Ico 1 b, k / p ^ i + ∑ i ∈ Ico 1 b, (n - k) / p ^ i + (filter (fun i => p ^ i ≤ k % p ^ i + (n - k) % p ^ i) (Ico 1 b)).card
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>s : Set α<VAR>hreg : c.IsRegular<VAR>S : Set (Set α)<VAR>Sg : S ⊆ g<VAR>Sct : #↑S < c<VAR>hS : ⋂₀ S ⊆ s<GOAL>s ∈ cardinalGenerate g ⋯
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>g : Set (Set α)<VAR>s : Set α<VAR>hreg : c.IsRegular<VAR>S : Set (Set α)<VAR>Sg : S ⊆ g<VAR>Sct : #↑S < c<VAR>hS : ⋂₀ S ⊆ s<VAR>this : CardinalInterFilter (cardinalGenerate g ⋯) c<GOAL>s ∈ cardinalGenerate g ⋯
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>h : Subsingleton R⟦X⟧<GOAL>Subsingleton R
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>h : ∀ (x y : R⟦X⟧), x = y<GOAL>∀ (x y : R), x = y
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>(∀ n > 0, n ∈ s → ∑ i ∈ n.divisors, f i = g n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>(∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, μ x.1 • g x.2 = f n) ↔ ∀ n > 0, n ∈ s → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f n
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<GOAL>∀ (a : ℕ), a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔ a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>a : ℕ<GOAL>a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔ a > 0 → a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>a : ℕ<GOAL>a > 0 → (a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, μ x.1 • g x.2 = f a ↔ a ∈ s → ∑ x ∈ a.divisorsAntidiagonal, ↑(μ x.1) * g x.2 = f a)
<VAR>R : Type u_1<VAR>inst✝ : Ring R<VAR>f g : ℕ → R<VAR>s : Set ℕ<VAR>hs : ∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s<VAR>a : ℕ<VAR>x✝¹ : a > 0<VAR>x✝ : a ∈ s<VAR>x : ℕ × ℕ<VAR>_hx : x ∈ a.divisorsAntidiagonal<GOAL>μ x.1 • g x.2 = ↑(μ x.1) * g x.2
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝² : Ring k<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module k V<VAR>S : AffineSpace V P<VAR>p₁ p₂ : P<GOAL>p₁ ∈ affineSpan k {p₂} ↔ p₁ = p₂
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<GOAL>(fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<GOAL>(fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>hc' : IsBigOWith c atTop ⇑f fun x => |x| ^ (-b)<GOAL>(fun x => ‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖) =O[atTop] fun x => |x| ^ (-b)
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>hc' : ∃ a, ∀ b_1 ≥ a, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<GOAL>∃ c a, ∀ b_1 ≥ a, ‖‖ContinuousMap.restrict (Icc (b_1 + R) (b_1 + S)) f‖‖ ≤ c * ‖|b_1| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : x ≥ max (1 + max 0 (-2 * R)) (d - R)<GOAL>‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<GOAL>‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : max 0 (-2 * R) < x<GOAL>‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<GOAL>‖‖ContinuousMap.restrict (Icc (x + R) (x + S)) f‖‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<GOAL>∀ (x_1 : ↑(Icc (x + R) (x + S))), ‖(ContinuousMap.restrict (Icc (x + R) (x + S)) f) x_1‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖
<VAR>E : Type u_1<VAR>inst✝ : NormedAddCommGroup E<VAR>f : C(ℝ, E)<VAR>b : ℝ<VAR>hb : 0 < b<VAR>hf : ⇑f =O[atTop] fun x => |x| ^ (-b)<VAR>R S : ℝ<VAR>claim : ∀ (x : ℝ), max 0 (-2 * R) < x → ∀ (y : ℝ), x + R ≤ y → y ^ (-b) ≤ (1 / 2) ^ (-b) * x ^ (-b)<VAR>c : ℝ<VAR>hc : c > 0<VAR>d : ℝ<VAR>hd : ∀ b_1 ≥ d, ‖f b_1‖ ≤ c * ‖|b_1| ^ (-b)‖<VAR>x : ℝ<VAR>hx : 1 + max 0 (-2 * R) ≤ x ∧ d - R ≤ x<VAR>hx' : 0 < x ∧ -2 * R < x<VAR>y : ↑(Icc (x + R) (x + S))<GOAL>c * ‖|↑y| ^ (-b)‖ ≤ c * (1 / 2) ^ (-b) * ‖|x| ^ (-b)‖