ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>p : α → ι → Prop<VAR>hic : #ι < c<GOAL>(∀ᶠ (x : α) in l, ∀ (i : ι), p x i) ↔ ∀ (i : ι), ∀ᶠ (x : α) in l, p x i
<VAR>ι α β : Type u<VAR>c : Cardinal.{u}<VAR>l : Filter α<VAR>inst✝ : CardinalInterFilter l c<VAR>p : α → ι → Prop<VAR>hic : #ι < c<GOAL>⋂ i, {x | p x i} ∈ l ↔ ∀ (i : ι), {x | p x i} ∈ l
<VAR>C : Type uC<VAR>inst✝² : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>P : MorphismProperty W.Localization<VAR>inst✝ : P.IsStableUnderComposition<VAR>hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)<VAR>hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)<GOAL>P = ⊤
<VAR>C : Type uC<VAR>inst✝² : Category.{uC', uC} C<VAR>W : MorphismProperty C<VAR>D : Type uD<VAR>inst✝¹ : Category.{uD', uD} D<VAR>G : C ⥤ D<VAR>hG : W.IsInvertedBy G<VAR>P : MorphismProperty W.Localization<VAR>inst✝ : P.IsStableUnderComposition<VAR>hP₁ : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), P (W.Q.map f)<VAR>hP₂ : ∀ ⦃X Y : C⦄ (w : X ⟶ Y) (hw : W w), P (wInv w hw)<VAR>X Y : W.Localization<VAR>f : X ⟶ Y<GOAL>P f = ⊤ f
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>hz_re : 0 ≤ re 0<VAR>hz_im : 0 ≤ im 0<GOAL>‖f 0‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>z : ℂ<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>hz_re : 0 ≤ z.re<VAR>hz_im : 0 ≤ z.im<VAR>hzne : z ≠ 0<GOAL>‖f z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<GOAL>‖f (cexp ζ)‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<GOAL>‖(f ∘ cexp) ζ‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<VAR>H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)<GOAL>‖(f ∘ cexp) ζ‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<VAR>H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)<GOAL>∃ c < π / (π / 2 - 0), ∃ B, (f ∘ cexp) =O[comap (_root_.abs ∘ re) atTop ⊓ 𝓟 (im ⁻¹' Ioo 0 (π / 2))] fun z => expR (B * expR (c * |z.re|))
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<VAR>H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)<GOAL>∀ (z : ℂ), z.im = 0 → ‖(f ∘ cexp) z‖ ≤ C
<VAR>E : Type u_1<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace ℂ E<VAR>a b C : ℝ<VAR>f g : ℂ → E<VAR>hd : DiffContOnCl ℂ f (Ioi 0 ×ℂ Ioi 0)<VAR>hB : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 (Ioi 0 ×ℂ Ioi 0)] fun z => expR (B * Complex.abs z ^ c)<VAR>hre : ∀ (x : ℝ), 0 ≤ x → ‖f ↑x‖ ≤ C<VAR>him : ∀ (x : ℝ), 0 ≤ x → ‖f (↑x * I)‖ ≤ C<VAR>ζ : ℂ<VAR>hζ : ζ.im ∈ Icc 0 (π / 2)<VAR>hz_re : 0 ≤ (cexp ζ).re<VAR>hz_im : 0 ≤ (cexp ζ).im<VAR>hzne : cexp ζ ≠ 0<VAR>H : MapsTo cexp (im ⁻¹' Ioo 0 (π / 2)) (Ioi 0 ×ℂ Ioi 0)<GOAL>∀ (z : ℂ), z.im = π / 2 → ‖(f ∘ cexp) z‖ ≤ C
<VAR>R : Type u<VAR>a b : R<VAR>m n✝ : ℕ<VAR>inst✝ : Semiring R<VAR>p q : R[X]<VAR>n : ℕ<GOAL>p * X ^ n * q = p * q * X ^ n
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.eraseLead + C f.leadingCoeff * X ^ f.natDegree = f
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<GOAL>(starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<GOAL>∀ x ∈ Set.range ⇑(canonicalEmbedding K), (starRingEnd ℂ) (x φ) = x (ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<GOAL>(starRingEnd ℂ) (0 φ) = 0 (ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<VAR>x✝¹ x✝ : (K →+* ℂ) → ℂ<VAR>hx : (starRingEnd ℂ) (x✝¹ φ) = x✝¹ (ComplexEmbedding.conjugate φ)<VAR>hy : (starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)<GOAL>(starRingEnd ℂ) ((x✝¹ + x✝) φ) = (x✝¹ + x✝) (ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>inst✝ : Field K<VAR>x : (K →+* ℂ) → ℂ<VAR>φ : K →+* ℂ<VAR>hx✝ : x ∈ Submodule.span ℝ (Set.range ⇑(canonicalEmbedding K))<VAR>a : ℝ<VAR>x✝ : (K →+* ℂ) → ℂ<VAR>hx : (starRingEnd ℂ) (x✝ φ) = x✝ (ComplexEmbedding.conjugate φ)<GOAL>(starRingEnd ℂ) ((a • x✝) φ) = (a • x✝) (ComplexEmbedding.conjugate φ)
<VAR>K : Type u_1<VAR>inst✝² : Field K<VAR>inst✝¹ : NumberField K<VAR>inst✝ : DecidableEq (K →+* ℂ)<GOAL>0 ≤ NumberField.house.supOfBasis K
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : (x : M) → x ∈ span R s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯<VAR>x : M<VAR>hx : x ∈ span R s<GOAL>p x hx
<VAR>R : Type u_1<VAR>R₂ : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M₂ : Type u_5<VAR>V : Type u_6<VAR>S : Type u_7<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : Module R M<VAR>x✝ : M<VAR>p✝ p' : Submodule R M<VAR>inst✝⁴ : Semiring R₂<VAR>σ₁₂ : R →+* R₂<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R₂ M₂<VAR>F : Type u_8<VAR>inst✝¹ : FunLike F M M₂<VAR>inst✝ : SemilinearMapClass F σ₁₂ M M₂<VAR>s t : Set M<VAR>p : (x : M) → x ∈ span R s → Prop<VAR>mem : ∀ (x : M) (h : x ∈ s), p x ⋯<VAR>zero : p 0 ⋯<VAR>add : ∀ (x : M) (hx : x ∈ span R s) (y : M) (hy : y ∈ span R s), p x hx → p y hy → p (x + y) ⋯<VAR>smul : ∀ (a : R) (x : M) (hx : x ∈ span R s), p x hx → p (a • x) ⋯<VAR>x : M<VAR>hx : x ∈ span R s<GOAL>∃ (x_1 : x ∈ span R s), p x x_1
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Bijective ⇑f'<VAR>n : ℕ<GOAL>Bijective ⇑(f' ^ (n + 1))
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>S : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>N : Type u_9<VAR>N₁ : Type u_10<VAR>N₂ : Type u_11<VAR>inst✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommGroup N₁<VAR>inst✝⁴ : Module R M<VAR>inst✝³ : Module R N₁<VAR>inst✝² : Monoid S<VAR>inst✝¹ : DistribMulAction S M<VAR>inst✝ : SMulCommClass R S M<VAR>f' : M →ₗ[R] M<VAR>h : Bijective ⇑f'<VAR>n : ℕ<GOAL>Bijective ⇑((f' ^ n) ∘ₗ f')
<VAR>x y z : ℝ<GOAL>sinh x ≤ 0 ↔ x ≤ 0
<VAR>α : Sort u<VAR>β : Sort v<VAR>f x✝¹ x✝ : α ≃ β<VAR>h : x✝¹.toEmbedding = x✝.toEmbedding<GOAL>x✝¹ = x✝
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>η : Kernel β γ<VAR>inst✝¹ : IsSFiniteKernel η<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>((η ∘ₖ κ) a) s = ((κ ⊗ₖ prodMkLeft α η).snd a) s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>η : Kernel β γ<VAR>inst✝¹ : IsSFiniteKernel η<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>∫⁻ (b : β), (η b) s ∂κ a = ∫⁻ (b : β), ((prodMkLeft α η) (a, b)) {c | (b, c) ∈ {p | p.2 ∈ s}} ∂κ a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>ι : Type u_3<VAR>mα : MeasurableSpace α<VAR>mβ : MeasurableSpace β<VAR>γ : Type u_4<VAR>mγ : MeasurableSpace γ<VAR>f : β → γ<VAR>g : γ → α<VAR>η : Kernel β γ<VAR>inst✝¹ : IsSFiniteKernel η<VAR>κ : Kernel α β<VAR>inst✝ : IsSFiniteKernel κ<VAR>a : α<VAR>s : Set γ<VAR>hs : MeasurableSet s<GOAL>MeasurableSet {p | p.2 ∈ s}
<VAR>G✝ : PGame<VAR>inst✝¹ : G✝.Impartial<VAR>G : PGame<VAR>inst✝ : G.Impartial<GOAL>G ≤ 0 ↔ 0 ≤ G
<VAR>α : Type u_1<VAR>M : Matroid α<VAR>B I J X Y : Set α<VAR>e : α<VAR>hI : M.Basis I X<GOAL>X ∩ M.E = X
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>x : ↥(unop U)<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>m : ↑x ∈ V<VAR>i : V ⟶ unop U<VAR>j : ℕ<VAR>r : A<VAR>r_mem : r ∈ 𝒜 j<VAR>s : A<VAR>s_mem : s ∈ 𝒜 j<VAR>nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>hy : ∀ (x : ↥V), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := j, num := ⟨r, r_mem⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x => (-a) ((fun x => ⟨↑x, ⋯⟩) x)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>x : ↥(unop U)<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>m : ↑x ∈ V<VAR>i : V ⟶ unop U<VAR>j : ℕ<VAR>r : A<VAR>r_mem : r ∈ 𝒜 j<VAR>s : A<VAR>s_mem : s ∈ 𝒜 j<VAR>nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>hy : ∀ (x : ↥V), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := j, num := ⟨r, r_mem⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }<VAR>y : ↥V<GOAL>(fun x => (-a) ((fun x => ⟨↑x, ⋯⟩) x)) y = HomogeneousLocalization.mk { deg := j, num := ⟨-r, ⋯⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>U : (Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ<VAR>a : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>x : ↥(unop U)<VAR>V : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>m : ↑x ∈ V<VAR>i : V ⟶ unop U<VAR>j : ℕ<VAR>r : A<VAR>r_mem : r ∈ 𝒜 j<VAR>s : A<VAR>s_mem : s ∈ 𝒜 j<VAR>nin : ∀ (x : ↥V), ↑⟨s, s_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>y : ↥V<VAR>hy : ∀ (x : ↥V), val (a ⟨↑x, ⋯⟩) = Localization.mk r ⟨s, ⋯⟩<GOAL>(fun x => (-a) ((fun x => ⟨↑x, ⋯⟩) x)) y = HomogeneousLocalization.mk { deg := j, num := ⟨-r, ⋯⟩, den := ⟨s, s_mem⟩, den_mem := ⋯ }
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>x y : α<GOAL>‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u_1<VAR>inst✝ : NormedLatticeAddCommGroup α<VAR>x y : α<VAR>h : ‖x ⊔ y - 0 ⊔ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖<GOAL>‖x ⊔ y‖ ≤ ‖x‖ + ‖y‖
<VAR>α : Type u<VAR>β : Type v<VAR>R r : α → α → Prop<VAR>l l₁✝ l₂✝ : List α<VAR>a✝ b✝ a b : α<VAR>l₁ l₂ : List α<GOAL>Chain R a (l₁ ++ b :: l₂) ↔ Chain R a (l₁ ++ [b]) ∧ Chain R b l₂
<VAR>F : Type u_1<VAR>G : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : FunLike F G H<VAR>a : G<VAR>b : H<VAR>inst✝² : AddGroupWithOne G<VAR>inst✝¹ : AddGroup H<VAR>inst✝ : AddConstMapClass F G H 1 b<VAR>f : F<VAR>x : G<VAR>n : ℤ<GOAL>f (x - ↑n) = f x - n • b
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a < 0<GOAL>ContinuousAt (⇑SignType.sign) a
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a < 0<GOAL>(fun x => -1) =ᶠ[nhds a] ⇑SignType.sign
<VAR>α : Type u_1<VAR>inst✝⁴ : Zero α<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : DecidableRel fun x x_1 => x < x_1<VAR>inst✝ : OrderTopology α<VAR>a : α<VAR>h : a < 0<GOAL>∃ t, (∀ y ∈ t, -1 = SignType.sign y) ∧ IsOpen t ∧ a ∈ t
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).intDegree = x.intDegree + y.intDegree
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(x * y).num.natDegree + (↑x.denom.natDegree + ↑y.denom.natDegree) = ↑x.num.natDegree + ↑y.num.natDegree + ↑(x * y).denom.natDegree
<VAR>K : Type u<VAR>inst✝ : Field K<VAR>x y : RatFunc K<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>(x * y).num.natDegree + (x.denom.natDegree + y.denom.natDegree) = x.num.natDegree + y.num.natDegree + (x * y).denom.natDegree
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>β₂ : Type u_3<VAR>γ : Type u_4<VAR>ι : Sort u_5<VAR>ι' : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ' : ι' → Sort u_8<VAR>inst✝ : CompleteLinearOrder α<VAR>f : ι → α<GOAL>iSup f = ⊤ ↔ ∀ b < ⊤, ∃ i, b < f i
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : IsPreconnected U<VAR>x : α<VAR>hx : x ∈ U<GOAL>AccPt x (𝓟 U)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty<VAR>x : α<VAR>hx : x ∈ U<GOAL>AccPt x (𝓟 U)
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty<VAR>x : α<VAR>hx : x ∈ U<GOAL>U ⊆ {x} ∪ closure (U \ {x})
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty<VAR>x : α<VAR>hx : x ∈ U<GOAL>(U ∩ {x}).Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>h : ∀ (t t' : Set α), IsClosed t → IsClosed t' → U ⊆ t ∪ t' → (U ∩ t).Nonempty → (U ∩ t').Nonempty → (U ∩ (t ∩ t')).Nonempty<VAR>x : α<VAR>hx : x ∈ U<GOAL>(U ∩ closure (U \ {x})).Nonempty
<VAR>α : Type u_1<VAR>inst✝¹ : TopologicalSpace α<VAR>C : Set α<VAR>inst✝ : T1Space α<VAR>U : Set α<VAR>hu : U.Nontrivial<VAR>x : α<VAR>hx : x ∈ U<VAR>h : (U ∩ ({x} ∩ closure (U \ {x}))).Nonempty<GOAL>AccPt x (𝓟 U)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace ℝ F<VAR>inst✝⁷ : FiniteDimensional ℝ F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<GOAL>MeasurePreserving (⇑f) volume volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace ℝ F<VAR>inst✝⁷ : FiniteDimensional ℝ F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<GOAL>map (⇑f) volume = volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace ℝ F<VAR>inst✝⁷ : FiniteDimensional ℝ F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<VAR>w : Finset E<VAR>b : OrthonormalBasis { x // x ∈ w } ℝ E<VAR>_hw : ⇑b = Subtype.val<GOAL>map (⇑f) volume = volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝¹⁰ : Fintype ι<VAR>inst✝⁹ : NormedAddCommGroup F<VAR>inst✝⁸ : InnerProductSpace ℝ F<VAR>inst✝⁷ : FiniteDimensional ℝ F<VAR>inst✝⁶ : MeasurableSpace F<VAR>inst✝⁵ : BorelSpace F<VAR>inst✝⁴ : NormedAddCommGroup E<VAR>inst✝³ : InnerProductSpace ℝ E<VAR>inst✝² : FiniteDimensional ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>f : E ≃ₗᵢ[ℝ] F<VAR>w : Finset E<VAR>b : OrthonormalBasis { x // x ∈ w } ℝ E<VAR>_hw : ⇑b = Subtype.val<GOAL>(b.toBasis.map f.toContinuousLinearEquiv.toLinearEquiv).addHaar = (b.map f).toBasis.addHaar
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<GOAL>cfc (g ∘ f) a = cfc g (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>this : ContinuousOn (g ∘ f) (spectrum R a)<GOAL>cfc (g ∘ f) a = cfc g (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>this : ContinuousOn (g ∘ f) (spectrum R a)<VAR>sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a<GOAL>cfc (g ∘ f) a = cfc g (cfc f a)
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>this : ContinuousOn (g ∘ f) (spectrum R a)<VAR>sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a<GOAL>(cfcHom ha) { toFun := (spectrum R a).restrict (g ∘ f), continuous_toFun := ⋯ } = (cfcHom ⋯) ({ toFun := (spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })).restrict g, continuous_toFun := ⋯ }.comp ?f')
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>p : A → Prop<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : StarRing R<VAR>inst✝⁸ : MetricSpace R<VAR>inst✝⁷ : TopologicalSemiring R<VAR>inst✝⁶ : ContinuousStar R<VAR>inst✝⁵ : TopologicalSpace A<VAR>inst✝⁴ : Ring A<VAR>inst✝³ : StarRing A<VAR>inst✝² : Algebra R A<VAR>inst✝¹ : ContinuousFunctionalCalculus R p<VAR>f✝ g✝ : R → R<VAR>a✝ : A<VAR>ha✝ : autoParam (p a✝) _auto✝<VAR>hf✝ : autoParam (ContinuousOn f✝ (spectrum R a✝)) _auto✝<VAR>hg✝ : autoParam (ContinuousOn g✝ (spectrum R a✝)) _auto✝<VAR>inst✝ : UniqueContinuousFunctionalCalculus R A<VAR>g f : R → R<VAR>a : A<VAR>ha : autoParam (p a) _auto✝<VAR>hg : autoParam (ContinuousOn g (f '' spectrum R a)) _auto✝<VAR>hf : autoParam (ContinuousOn f (spectrum R a)) _auto✝<VAR>this : ContinuousOn (g ∘ f) (spectrum R a)<VAR>sp_eq : spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ }) = f '' spectrum R a<GOAL>C(↑(spectrum R a), ↑(spectrum R ((cfcHom ⋯) { toFun := (spectrum R a).restrict f, continuous_toFun := ⋯ })))