ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<GOAL>((structureSheaf R).presheaf.germ ⟨x, hxU⟩ ≫ stalkToFiberRingHom R x ≫ localizationToStalk R x) s = ((structureSheaf R).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<GOAL>(localizationToStalk R x) (↑s ⟨x, hxU⟩) = ((structureSheaf R).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : x ∈ V<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hg : V ≤ PrimeSpectrum.basicOpen g<VAR>hs : const R f g V hg = ((structureSheaf R).val.map iVU.op) s<GOAL>(localizationToStalk R x) (↑s ⟨x, hxU⟩) = ((structureSheaf R).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : x ∈ V<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hg : V ≤ PrimeSpectrum.basicOpen g<VAR>hs : const R f g V hg = ((structureSheaf R).val.map iVU.op) s<GOAL>((structureSheaf R).presheaf.germ ⟨x, ⋯⟩) (const R f (↑⟨g, ⋯⟩) (PrimeSpectrum.basicOpen ↑⟨g, ⋯⟩) ⋯) = ((structureSheaf R).presheaf.germ ⟨x, hxU⟩) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : x ∈ V<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hg : V ≤ PrimeSpectrum.basicOpen g<VAR>hs : const R f g V hg = ((structureSheaf R).val.map iVU.op) s<GOAL>((structureSheaf R).presheaf.map (homOfLE hg).op) (const R f (↑⟨g, ⋯⟩) (PrimeSpectrum.basicOpen ↑⟨g, ⋯⟩) ⋯) = ((structureSheaf R).presheaf.map iVU.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>U : Opens ↑(PrimeSpectrum.Top R)<VAR>hxU : x ∈ U<VAR>s : (forget CommRingCat).obj ((structureSheaf R).presheaf.obj (op U))<VAR>V : Opens ↑(PrimeSpectrum.Top R)<VAR>hxV : x ∈ V<VAR>iVU : V ⟶ U<VAR>f g : R<VAR>hg : V ≤ PrimeSpectrum.basicOpen g<VAR>hs : const R f g V hg = ((structureSheaf R).val.map iVU.op) s<GOAL>((structureSheaf R).presheaf.map (homOfLE hg).op) (const R f g (PrimeSpectrum.basicOpen g) ⋯) = ((structureSheaf R).presheaf.map iVU.op) s
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>f : R<GOAL>((RingHom.comp (stalkToFiberRingHom R x) (localizationToStalk R x)).comp (algebraMap R (Localization.AtPrime x.asIdeal))) f = ((RingHom.id (Localization.AtPrime x.asIdeal)).comp (algebraMap R (Localization.AtPrime x.asIdeal))) f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>f : R<GOAL>(stalkToFiberRingHom R x) ((localizationToStalk R x) ((algebraMap R (Localization.AtPrime x.asIdeal)) f)) = ((RingHom.id (Localization.AtPrime x.asIdeal)).comp (algebraMap R (Localization.AtPrime x.asIdeal))) f
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>x : ↑(PrimeSpectrum.Top R)<VAR>f : R<GOAL>(algebraMap R (Localization.AtPrime x.asIdeal)) f = ((RingHom.id (Localization.AtPrime x.asIdeal)).comp (algebraMap R (Localization.AtPrime x.asIdeal))) f
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<GOAL>∃ a, IsFundamental a
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a : Solution₁ d<VAR>ha₁ : 1 < a.x<VAR>ha₂ : 0 < a.y<GOAL>∃ a, IsFundamental a
<VAR>d : ℤ<VAR>h₀ : 0 < d<VAR>hd : ¬IsSquare d<VAR>a : Solution₁ d<VAR>ha₁ : 1 < a.x<VAR>ha₂ : 0 < a.y<VAR>P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1<GOAL>∃ a, IsFundamental a
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖{ toFun := integral, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ 1 * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_4<VAR>inst✝¹⁰ : NormedAddCommGroup E<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>inst✝⁸ : NormedField 𝕜<VAR>inst✝⁷ : NormedSpace 𝕜 E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>inst✝⁵ : SMulCommClass ℝ 𝕜 E<VAR>F' : Type u_5<VAR>inst✝⁴ : NormedAddCommGroup F'<VAR>inst✝³ : NormedSpace ℝ F'<VAR>E' : Type u_6<VAR>inst✝² : NormedAddCommGroup E'<VAR>inst✝¹ : NormedSpace ℝ E'<VAR>inst✝ : NormedSpace 𝕜 E'<VAR>f : ↥(simpleFunc E 1 μ)<GOAL>‖{ toFun := integral, map_add' := ⋯, map_smul' := ⋯ } f‖ ≤ ‖f‖
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>Summable fun n => ‖(riemannZetaSummandHom ⋯) n‖
<VAR>s : ℂ<VAR>hs : 1 < s.re<GOAL>Summable fun n => ‖↑n ^ (-s)‖
<VAR>s : ℂ<VAR>hs : 1 < s.re<VAR>n : ℕ<GOAL>‖↑n ^ (-s)‖ = (↑n ^ s.re)⁻¹
<VAR>𝕜 : Type u<VAR>𝕜' : Type u'<VAR>E : Type v<VAR>F : Type w<VAR>G : Type x<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f : 𝕜 → E<VAR>n : ℕ<VAR>z z₀ : 𝕜<VAR>y : Fin n → 𝕜<GOAL>‖p n‖ = ‖p.coeff n‖
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<VAR>c : Chain ((a : α) → (b : β a) → γ a b)<VAR>x : α<VAR>y : β x<GOAL>ωSup ((c.map (evalOrderHom x)).map (evalOrderHom y)) = ωSup ((c.map (monotoneUncurry α β γ)).map (evalOrderHom ⟨x, y⟩))
<VAR>α : Type u_1<VAR>β : α → Type u_2<VAR>γ : (a : α) → β a → Type u_3<VAR>inst✝ : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)<VAR>c : Chain ((a : α) → (b : β a) → γ a b)<VAR>x : α<VAR>y : β x<GOAL>ωSup (c.map ((evalOrderHom y).comp (evalOrderHom x))) = ωSup (c.map ((evalOrderHom ⟨x, y⟩).comp (monotoneUncurry α β γ)))
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<GOAL>⌈logb (↑b) r⌉ = Int.clog b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>⌈logb (↑b) r⌉ = Int.clog b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>⌈logb (↑b) r⌉ ≤ Int.clog b r
<VAR>b✝ x y : ℝ<VAR>b : ℕ<VAR>r : ℝ<VAR>hb : 1 < b<VAR>hr✝ : 0 ≤ r<VAR>hr : 0 < r<VAR>hb1' : 1 < ↑b<GOAL>Int.clog b r ≤ ⌈logb (↑b) r⌉
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(deriv fun x => x ^ p * (1 - ε x)) =ᶠ[atTop] fun x => deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<GOAL>deriv (fun x => x ^ p * (1 - ε x)) x = deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ (fun x => x ^ p) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<GOAL>DifferentiableAt ℝ (fun x => 1 - ε x) x
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(fun x => deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x) =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 1 < x<VAR>hderiv : deriv (fun x => 1 - ε x) x = x⁻¹ / log x ^ 2<GOAL>deriv (fun x => x ^ p) x * (1 - ε x) + x ^ p * deriv (fun x => 1 - ε x) x = p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p : ℝ<GOAL>(fun x => p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2)) =ᶠ[atTop] fun x => p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2
<VAR>α : Type u_1<VAR>inst✝¹ : Fintype α<VAR>inst✝ : Nonempty α<VAR>T : ℕ → ℝ<VAR>g : ℝ → ℝ<VAR>a b : α → ℝ<VAR>r : α → ℕ → ℕ<VAR>R : AkraBazziRecurrence T g a b r<VAR>p x : ℝ<VAR>hx : 0 < x<GOAL>p * x ^ (p - 1) * (1 - ε x) + x ^ p * (x⁻¹ / log x ^ 2) = p * x ^ (p - 1) * (1 - ε x) + x ^ (p - 1) / log x ^ 2
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>o.bsup f = o.blsub f ∨ succ (o.bsup f) = o.blsub f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u}<VAR>f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}<GOAL>sup (o.familyOfBFamily f) = lsub (o.familyOfBFamily f) ∨ succ (sup (o.familyOfBFamily f)) = lsub (o.familyOfBFamily f)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian f φ<VAR>inst✝ : IsIso f<GOAL>IsIso φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ⟶ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<GOAL>IsIso φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<GOAL>IsIso φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<GOAL>IsIso φ
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<GOAL>φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<VAR>inv_hom : φ' ≫ φ = 𝟙 b<GOAL>φ ≫ φ' = 𝟙 a ∧ φ' ≫ φ = 𝟙 b
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<VAR>inv_hom : φ' ≫ φ = 𝟙 b<GOAL>φ ≫ φ' = 𝟙 a
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<VAR>inv_hom : φ' ≫ φ = 𝟙 b<VAR>h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')<GOAL>φ ≫ φ' = 𝟙 a
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝³ : Category.{v₁, u₁} 𝒮<VAR>inst✝² : Category.{v₂, u₂} 𝒳<VAR>p : 𝒳 ⥤ 𝒮<VAR>a b : 𝒳<VAR>φ : a ⟶ b<VAR>inst✝¹ : p.IsStronglyCartesian (p.map φ) φ<VAR>inst✝ : IsIso (p.map φ)<VAR>φ' : b ⟶ a := map p (p.map φ) φ ⋯ (𝟙 b)<VAR>inv_hom : φ' ≫ φ = 𝟙 b<VAR>h₁ : p.IsHomLift (𝟙 (p.obj a)) (φ ≫ φ')<GOAL>(φ ≫ φ') ≫ φ = 𝟙 a ≫ φ
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<GOAL>min φ.order ψ.order ≤ (φ + ψ).order
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>φ✝ φ ψ : R⟦X⟧<GOAL>∀ (i : ℕ), ↑i < min φ.order ψ.order → (coeff R i) (φ + ψ) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : Preorder α<VAR>inst✝ : Preorder β<VAR>e : α ↪o β<VAR>he : (range ⇑e).OrdConnected<VAR>x y : α<GOAL>⇑e '' Ico x y = Ico (e x) (e y)
<VAR>α : Type u_1<VAR>inst✝ : LinearOrderedRing α<VAR>a b x : α<GOAL>x * ↑(sign x) = |x|
<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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x ≤ 0<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>deriv f x ≤ 0
<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>D : Set ℝ<VAR>hD : Convex ℝ D<VAR>f f' : ℝ → ℝ<VAR>hf : ContinuousOn f D<VAR>hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x<VAR>hf'₀ : ∀ x ∈ interior D, f' x ≤ 0<VAR>x : ℝ<VAR>hx : x ∈ interior D<GOAL>f' x ≤ 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<GOAL>‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹<GOAL>‖(2 * ↑π * I)⁻¹ • ∮ (z : ℂ) in C(c, R), f z‖ ≤ R * C
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : NormedSpace ℂ E<VAR>inst✝ : CompleteSpace E<VAR>f : ℂ → E<VAR>c : ℂ<VAR>R C : ℝ<VAR>hR : 0 ≤ R<VAR>hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C<VAR>this : ‖(2 * ↑π * I)⁻¹‖ = (2 * π)⁻¹<GOAL>‖∮ (z : ℂ) in C(c, R), f z‖ ≤ 2 * π * R * C
<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>x : M<VAR>y : ↥S<GOAL>f.toMap ↑y * f.mk' x y = f.toMap x
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>r : ℝ≥0<GOAL>(r • s).singularPart μ = r • s.singularPart μ
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>m : MeasurableSpace α<VAR>μ✝ ν : Measure α<VAR>s✝ t s : SignedMeasure α<VAR>μ : Measure α<VAR>r : ℝ≥0<GOAL>((r • s).toJordanDecomposition.posPart.singularPart μ).toSignedMeasure - ((r • s).toJordanDecomposition.negPart.singularPart μ).toSignedMeasure = (r • s.toJordanDecomposition.posPart.singularPart μ).toSignedMeasure - (r • s.toJordanDecomposition.negPart.singularPart μ).toSignedMeasure
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>inst✝ : CompleteLattice α<VAR>f g : Filter β<VAR>p q : β → Prop<VAR>u v : β → α<VAR>h : ∀ (x : β), p x → q x<VAR>a : α<VAR>ha : a ∈ {a | ∀ᶠ (x : β) in f, q x → a ≤ u x}<GOAL>∀ (x : β), (q x → a ≤ u x) → p x → a ≤ u x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>h : I ≤ J<VAR>i : ι<VAR>x : ℝ<GOAL>(split J i x).restrict I = split I i x
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>h : I ≤ J<VAR>i : ι<VAR>x : ℝ<GOAL>((split J i x).restrict I).boxes ⊆ (split I i x).boxes
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>h : I ≤ J<VAR>i : ι<VAR>x : ℝ<GOAL>∀ ⦃x_1 : Box ι⦄, (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') → ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
<VAR>ι : Type u_1<VAR>M : Type u_2<VAR>n : ℕ<VAR>I J : Box ι<VAR>i✝ : ι<VAR>x✝ : ℝ<VAR>h : I ≤ J<VAR>i : ι<VAR>x : ℝ<VAR>this : ∀ (s : Set (ι → ℝ)), ↑I ∩ s ⊆ ↑J<GOAL>∀ ⦃x_1 : Box ι⦄, (∃ J', (↑J' = ↑J ∩ {y | y i ≤ x} ∨ ↑J' = ↑J ∩ {y | x < y i}) ∧ ↑x_1 = ↑I ∩ ↑J') → ↑x_1 = ↑I ∩ {y | y i ≤ x} ∨ ↑x_1 = ↑I ∩ {y | x < y i}
<VAR>a : ℤ<VAR>b₁ b₂ : ℕ<VAR>hb₁ : b₁ ≠ 0<VAR>hb₂ : b₂ ≠ 0<GOAL>J(a | b₁ * b₂) = J(a | b₁) * J(a | b₂)
<VAR>a : ℤ<VAR>b₁ b₂ : ℕ<VAR>hb₁ : b₁ ≠ 0<VAR>hb₂ : b₂ ≠ 0<GOAL>(List.pmap (fun p pp => legendreSym p a) b₁.primeFactorsList ⋯).prod * (List.pmap (fun p pp => legendreSym p a) b₂.primeFactorsList ⋯).prod = J(a | b₁) * J(a | b₂)
<VAR>a : ℤ<VAR>b₁ b₂ : ℕ<VAR>hb₁ : b₁ ≠ 0<VAR>hb₂ : b₂ ≠ 0<GOAL>∀ a ∈ b₁.primeFactorsList ++ b₂.primeFactorsList, Nat.Prime a
<VAR>n : ℕ<GOAL>Monoid.exponent (DihedralGroup n) = lcm n 2
<GOAL>Monoid.exponent (DihedralGroup 0) = lcm 0 2
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>Monoid.exponent (DihedralGroup n) = lcm n 2
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>Monoid.exponent (DihedralGroup n) ∣ lcm n 2
<VAR>n : ℕ<VAR>hn : NeZero n<GOAL>lcm n 2 ∣ Monoid.exponent (DihedralGroup n)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>a : ℕ<VAR>h : a ∈ f.eraseLead.support<GOAL>a < f.natDegree
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f : R[X]<VAR>a : ℕ<VAR>h : a ≠ f.natDegree ∧ a ∈ f.support<GOAL>a < f.natDegree
<VAR>α : Type u_1<VAR>inst✝ : PseudoEMetricSpace α<VAR>δ : ℝ<VAR>E : Set α<GOAL>thickenedIndicatorAux δ (closure E) = thickenedIndicatorAux δ E
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>f✝ : X → Y<VAR>s : Set X<VAR>f : X → Y<VAR>hf : Embedding f<GOAL>IsLocallyClosed s ↔ ∃ s', IsLocallyClosed s' ∧ s' ∩ range f = f '' s
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>hR : IsField R<VAR>I : Ideal R[X]<VAR>hI : I.IsMaximal<VAR>x : R<VAR>hx : C x ∈ I<GOAL>x = 0
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>hR : IsField R<VAR>I : Ideal R[X]<VAR>hI : I.IsMaximal<VAR>x : R<VAR>hx : C x ∈ I<VAR>hx0 : ¬x = 0<GOAL>1 ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>hR : IsField R<VAR>I : Ideal R[X]<VAR>hI : I.IsMaximal<VAR>x : R<VAR>hx : C x ∈ I<VAR>hx0 : ¬x = 0<VAR>y : R<VAR>hy : x * y = 1<GOAL>1 ∈ I
<VAR>R : Type u<VAR>S : Type u_1<VAR>inst✝ : Ring R<VAR>hR : IsField R<VAR>I : Ideal R[X]<VAR>hI : I.IsMaximal<VAR>x : R<VAR>hx : C x ∈ I<VAR>hx0 : ¬x = 0<VAR>y : R<VAR>hy : x * y = 1<GOAL>1 = C y * C x
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<GOAL>Mono S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>this : S.HasHomology<GOAL>Mono S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>this✝ : S.HasHomology<VAR>this : Epi S.toCycles<GOAL>Mono S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Epi S.toCycles<VAR>this : S.iCycles = 0<GOAL>Mono S.g
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Epi S.toCycles<VAR>this : S.iCycles = 0<GOAL>∀ {P : C} (g : P ⟶ S.X₂), g ≫ S.g = 0 → g = 0
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝³ : Category.{u_3, u_1} C<VAR>inst✝² : Category.{?u.64946, u_2} D<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : Preadditive D<VAR>S : ShortComplex C<VAR>hS : S.Exact<VAR>hf : S.f = 0<VAR>this✝¹ : S.HasHomology<VAR>this✝ : Epi S.toCycles<VAR>this : S.iCycles = 0<VAR>A : C<VAR>x₂ : A ⟶ S.X₂<VAR>hx₂ : x₂ ≫ S.g = 0<GOAL>x₂ = 0
<VAR>R : Type u_1<VAR>n✝ : ℕ<VAR>x y : ℤ<VAR>n : ℕ<VAR>hxy : 4 ∣ x - y<VAR>hx : ¬2 ∣ x<GOAL>multiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = multiplicity 2 (x - y) + ↑n
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>A : ι → AddSubmonoid M<VAR>h : IsInternal A<GOAL>iSup A = ⊤
<VAR>ι : Type v<VAR>β : ι → Type w<VAR>inst✝² : (i : ι) → AddCommMonoid (β i)<VAR>M : Type u_1<VAR>inst✝¹ : DecidableEq ι<VAR>inst✝ : AddCommMonoid M<VAR>A : ι → AddSubmonoid M<VAR>h : IsInternal A<GOAL>Surjective ⇑(DFinsupp.sumAddHom fun i => (A i).subtype)
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<GOAL>Nonempty ↑↑(↑U).toPresheafedSpace ↔ (↑U).Nonempty
<VAR>C : Type u₁<VAR>inst✝ : Category.{v, u₁} C<VAR>X : Scheme<VAR>U : X.Opens<GOAL>(∃ x, x ∈ U) ↔ (↑U).Nonempty
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<GOAL>Kᗮ = ⊥ ↔ K = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<GOAL>Kᗮ = ⊥ → K = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>h : Kᗮ = ⊥<GOAL>K = ⊤
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁵ : _root_.RCLike 𝕜<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : InnerProductSpace ℝ F<VAR>K : Submodule 𝕜 E<VAR>inst✝ : HasOrthogonalProjection K<VAR>h : Kᗮ = ⊥<VAR>this : K ⊔ Kᗮ = ⊤<GOAL>K = ⊤
<VAR>a b c : Ordinal.{u_1}<VAR>ab : a < b<GOAL>a ^ succ c < b ^ succ c
<VAR>a b c : Ordinal.{u_1}<VAR>ab : a < b<GOAL>a ^ c * a < b ^ c * b
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<GOAL>∃ k, ↑(weightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ k)
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<GOAL>↑(weightSpace M χ) ≤ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ ((toEnd R L M) x).maxGenEigenspaceIndex (χ x))
<VAR>K : Type u_1<VAR>R : Type u_2<VAR>L : Type u_3<VAR>M : Type u_4<VAR>inst✝⁸ : CommRing R<VAR>inst✝⁷ : LieRing L<VAR>inst✝⁶ : LieAlgebra R L<VAR>inst✝⁵ : LieAlgebra.IsNilpotent R L<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : LieRingModule L M<VAR>inst✝¹ : LieModule R L M<VAR>inst✝ : IsNoetherian R M<VAR>χ : L → R<VAR>x : L<VAR>m : M<VAR>hm : m ∈ ↑(weightSpace M χ)<GOAL>m ∈ LinearMap.ker (((toEnd R L M) x - (algebraMap R (Module.End R M)) (χ x)) ^ ((toEnd R L M) x).maxGenEigenspaceIndex (χ x))