ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u<VAR>inst✝ : CommRing R<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>x : X<GOAL>IsGδ {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>U : ℕ → Set X<VAR>hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)<VAR>h_basis : (𝓝 x).HasAntitoneBasis fun i => U i<GOAL>IsGδ {x}
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : T1Space X<VAR>x : X<VAR>U : ℕ → Set X<VAR>hU : ∀ (i : ℕ), x ∈ U i ∧ IsOpen (U i)<VAR>h_basis : (𝓝 x).HasAntitoneBasis fun i => U i<GOAL>IsGδ (⋂ i, ⋂ (_ : True), U i)
<VAR>X : Type u<VAR>Y : Type v<VAR>Z : Type u_1<VAR>W : Type u_2<VAR>ε : Type u_3<VAR>ζ : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>κ : Type u_7<VAR>inst✝ : TopologicalSpace X<VAR>T : (i : ι) → TopologicalSpace (π i)<VAR>f : X → (i : ι) → π i<VAR>𝔖 : Set (Set ι)<GOAL>induced (⋃₀ 𝔖).restrict topologicalSpace = ⨅ S ∈ 𝔖, induced S.restrict topologicalSpace
<VAR>m n✝ : ℤ<VAR>n : ℕ<GOAL>Odd (m ^ n) ↔ Odd m ∨ n = 0
<VAR>V : Type u_1<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : InnerProductSpace ℝ V<VAR>x y : V<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : InnerProductSpace ℝ F<VAR>f : E →ₗᵢ[ℝ] F<VAR>u v : E<GOAL>angle (f u) (f v) = angle u v
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>n : ℕ<VAR>t : Finset (Fin n)<VAR>this : ∀ (m : ℕ) (hm : n = m), (p n) (t.piecewise (fun x_1 => x) fun x => y) = (p m) ((Finset.map (finCongr hm).toEmbedding t).piecewise (fun x_1 => x) fun x => y)<GOAL>let s := changeOriginIndexEquiv.symm ⟨n, t⟩; (((p.changeOriginSeriesTerm s.fst s.snd.fst ↑s.snd.snd ⋯) fun x_1 => x) fun x => y) = (p n) (t.piecewise (fun x_1 => x) fun x => y)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>p : FormalMultilinearSeries 𝕜 E F<VAR>x y : E<VAR>r R : ℝ≥0<VAR>n : ℕ<VAR>t : Finset (Fin n)<VAR>this : ∀ (m : ℕ) (hm : n = m), (p n) (t.piecewise (fun x_1 => x) fun x => y) = (p m) ((Finset.map (finCongr hm).toEmbedding t).piecewise (fun x_1 => x) fun x => y)<GOAL>(p n) (t.piecewise (fun x_1 => x) fun x => y) = (p ((changeOriginIndexEquiv.symm ⟨n, t⟩).fst + (changeOriginIndexEquiv.symm ⟨n, t⟩).snd.fst)) ((↑(changeOriginIndexEquiv.symm ⟨n, t⟩).snd.snd).piecewise (fun x_1 => x) fun x => y)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h : ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)<VAR>S : Finset ι<VAR>f : ι → Set Ω<VAR>hf : ∀ i ∈ S, f i ∈ (fun i => {s i}) i<GOAL>∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (κ a) (f i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h : ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)<VAR>S : Finset ι<VAR>f : ι → Set Ω<VAR>hf : ∀ i ∈ S, f i ∈ (fun i => {s i}) i<VAR>a : α<VAR>ha : (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)<GOAL>(κ a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (κ a) (f i)
<VAR>α : Type u_1<VAR>Ω : Type u_2<VAR>ι : Type u_3<VAR>_mα : MeasurableSpace α<VAR>s : ι → Set Ω<VAR>_mΩ : MeasurableSpace Ω<VAR>κ : Kernel α Ω<VAR>μ : Measure α<VAR>h : ∀ (S : Finset ι), ∀ᵐ (a : α) ∂μ, (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)<VAR>S : Finset ι<VAR>f : ι → Set Ω<VAR>hf : ∀ i ∈ S, f i ∈ (fun i => {s i}) i<VAR>a : α<VAR>ha : (κ a) (⋂ i ∈ S, s i) = ∏ i ∈ S, (κ a) (s i)<VAR>this : ∀ i ∈ S, (κ a) (f i) = (κ a) (s i)<GOAL>(κ a) (⋂ i ∈ S, f i) = ∏ i ∈ S, (κ a) (f i)
<VAR>R : Type u_1<VAR>n : ℕ<VAR>hn : IsPrimePow n<VAR>hn' : ¬Nat.Prime n<GOAL>μ n = 0
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<VAR>hn : IsPrimePow (p ^ k)<VAR>hn' : ¬Nat.Prime (p ^ k)<GOAL>μ (p ^ k) = 0
<VAR>R : Type u_1<VAR>p k : ℕ<VAR>hp : Nat.Prime p<VAR>hk : 0 < k<VAR>hn : IsPrimePow (p ^ k)<VAR>hn' : ¬Nat.Prime (p ^ k)<GOAL>¬k = 1
<VAR>z : ℂ<GOAL>abs z = √(z.re ^ 2 + z.im ^ 2)
<VAR>a b : ℕ+<GOAL>(uIcc a b).card = (↑↑b - ↑↑a).natAbs + 1
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁹ : NormedAddCommGroup E<VAR>inst✝²⁸ : NormedAddCommGroup E'<VAR>inst✝²⁷ : NormedAddCommGroup E''<VAR>inst✝²⁶ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²⁵ : RCLike 𝕜<VAR>inst✝²⁴ : NormedSpace 𝕜 E<VAR>inst✝²³ : NormedSpace 𝕜 E'<VAR>inst✝²² : NormedSpace 𝕜 E''<VAR>inst✝²¹ : NormedSpace ℝ F<VAR>inst✝²⁰ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁹ : CompleteSpace F<VAR>inst✝¹⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁷ : NormedAddCommGroup F'<VAR>inst✝¹⁶ : NormedSpace ℝ F'<VAR>inst✝¹⁵ : NormedSpace 𝕜 F'<VAR>inst✝¹⁴ : CompleteSpace F'<VAR>inst✝¹³ : NormedAddCommGroup F''<VAR>inst✝¹² : NormedSpace ℝ F''<VAR>inst✝¹¹ : NormedSpace 𝕜 F''<VAR>inst✝¹⁰ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁹ : AddGroup G<VAR>inst✝⁸ : SFinite μ<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : μ.IsAddRightInvariant<VAR>inst✝⁵ : MeasurableAdd₂ G<VAR>inst✝⁴ : MeasurableNeg G<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ E'<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace E'<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<GOAL>∫ (x : G), (f ⋆[L, ν] g) x ∂μ = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁹ : NormedAddCommGroup E<VAR>inst✝²⁸ : NormedAddCommGroup E'<VAR>inst✝²⁷ : NormedAddCommGroup E''<VAR>inst✝²⁶ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²⁵ : RCLike 𝕜<VAR>inst✝²⁴ : NormedSpace 𝕜 E<VAR>inst✝²³ : NormedSpace 𝕜 E'<VAR>inst✝²² : NormedSpace 𝕜 E''<VAR>inst✝²¹ : NormedSpace ℝ F<VAR>inst✝²⁰ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁹ : CompleteSpace F<VAR>inst✝¹⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁷ : NormedAddCommGroup F'<VAR>inst✝¹⁶ : NormedSpace ℝ F'<VAR>inst✝¹⁵ : NormedSpace 𝕜 F'<VAR>inst✝¹⁴ : CompleteSpace F'<VAR>inst✝¹³ : NormedAddCommGroup F''<VAR>inst✝¹² : NormedSpace ℝ F''<VAR>inst✝¹¹ : NormedSpace 𝕜 F''<VAR>inst✝¹⁰ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁹ : AddGroup G<VAR>inst✝⁸ : SFinite μ<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : μ.IsAddRightInvariant<VAR>inst✝⁵ : MeasurableAdd₂ G<VAR>inst✝⁴ : MeasurableNeg G<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ E'<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace E'<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<GOAL>∫ (y : G), ∫ (x : G), (L (f y)) (g (x - y)) ∂μ ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
<VAR>𝕜 : Type u𝕜<VAR>G : Type uG<VAR>E : Type uE<VAR>E' : Type uE'<VAR>E'' : Type uE''<VAR>F : Type uF<VAR>F' : Type uF'<VAR>F'' : Type uF''<VAR>P : Type uP<VAR>inst✝²⁹ : NormedAddCommGroup E<VAR>inst✝²⁸ : NormedAddCommGroup E'<VAR>inst✝²⁷ : NormedAddCommGroup E''<VAR>inst✝²⁶ : NormedAddCommGroup F<VAR>f f' : G → E<VAR>g g' : G → E'<VAR>x x' : G<VAR>y y' : E<VAR>inst✝²⁵ : RCLike 𝕜<VAR>inst✝²⁴ : NormedSpace 𝕜 E<VAR>inst✝²³ : NormedSpace 𝕜 E'<VAR>inst✝²² : NormedSpace 𝕜 E''<VAR>inst✝²¹ : NormedSpace ℝ F<VAR>inst✝²⁰ : NormedSpace 𝕜 F<VAR>n : ℕ∞<VAR>inst✝¹⁹ : CompleteSpace F<VAR>inst✝¹⁸ : MeasurableSpace G<VAR>μ ν : Measure G<VAR>L : E →L[𝕜] E' →L[𝕜] F<VAR>inst✝¹⁷ : NormedAddCommGroup F'<VAR>inst✝¹⁶ : NormedSpace ℝ F'<VAR>inst✝¹⁵ : NormedSpace 𝕜 F'<VAR>inst✝¹⁴ : CompleteSpace F'<VAR>inst✝¹³ : NormedAddCommGroup F''<VAR>inst✝¹² : NormedSpace ℝ F''<VAR>inst✝¹¹ : NormedSpace 𝕜 F''<VAR>inst✝¹⁰ : CompleteSpace F''<VAR>k : G → E''<VAR>L₂ : F →L[𝕜] E'' →L[𝕜] F'<VAR>L₃ : E →L[𝕜] F'' →L[𝕜] F'<VAR>L₄ : E' →L[𝕜] E'' →L[𝕜] F''<VAR>inst✝⁹ : AddGroup G<VAR>inst✝⁸ : SFinite μ<VAR>inst✝⁷ : SFinite ν<VAR>inst✝⁶ : μ.IsAddRightInvariant<VAR>inst✝⁵ : MeasurableAdd₂ G<VAR>inst✝⁴ : MeasurableNeg G<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : NormedSpace ℝ E'<VAR>inst✝¹ : CompleteSpace E<VAR>inst✝ : CompleteSpace E'<VAR>hf : Integrable f ν<VAR>hg : Integrable g μ<GOAL>∫ (y : G), (L (f y)) (∫ (x : G), g x ∂μ) ∂ν = (L (∫ (x : G), f x ∂ν)) (∫ (x : G), g x ∂μ)
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : -(star c * c) = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : -(star c * c) = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : star c * c + c * star c = 2 • (↑(ℜ c) * ↑(ℜ c) + ↑(ℑ c) * ↑(ℑ c))<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : -(star c * c) = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : -(star c * c) = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : -(star c * c) = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : 0 = a_neg ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : 0 = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a ^ 3<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<GOAL>∀ x ∈ σ ℝ a, 0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<GOAL>0 ≤ x
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<VAR>hx' : x < 0<GOAL>False
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<VAR>hx' : 0 < -x<GOAL>False
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<VAR>hx' : 0 < -x<GOAL>0 = (-x) ^ 3
<VAR>A : Type u_1<VAR>inst✝⁵ : NormedRing A<VAR>inst✝⁴ : StarRing A<VAR>inst✝³ : CstarRing A<VAR>inst✝² : CompleteSpace A<VAR>inst✝¹ : NormedAlgebra ℂ A<VAR>inst✝ : StarModule ℂ A<VAR>b : A<VAR>a : A := star b * b<VAR>a_def : a = star b * b<VAR>a_neg : A := cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x) a<VAR>c : A := b * a_neg<VAR>h_eq_a_neg : cfc 0 a = cfc (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) a<VAR>h_c_spec₀ : SpectrumRestricts (-(star c * c)) fun x => ContinuousMap.realToNNReal x<VAR>c_eq : c * star c = 2 • (↑(ℜ c) ^ 2 + ↑(ℑ c) ^ 2) + -(star c * c)<VAR>h_c_spec₁ : SpectrumRestricts (c * star c) ⇑ContinuousMap.realToNNReal<VAR>h_c_spec₂ : SpectrumRestricts (star c * c) ⇑ContinuousMap.realToNNReal<VAR>x : ℝ<VAR>hx : x ∈ σ ℝ a<VAR>hx' : 0 < -x<VAR>h_eqOn : Set.EqOn 0 (fun x => (-ContinuousMap.id ℝ ⊔ 0) x ^ 3) (σ ℝ a)<GOAL>0 = (-x) ^ 3
<VAR>ι : Type u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝ : LinearOrderedSemifield α<VAR>a b c d e : α<VAR>m n : ℤ<GOAL>a / 2 < a ↔ 0 < a
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout b.inl 0 b.snd 0
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout 0 b.inl 0 b.snd
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>inst✝¹ : HasZeroObject C<VAR>inst✝ : HasZeroMorphisms C<VAR>b : BinaryBicone X Y<VAR>h : b.IsBilimit<GOAL>IsPushout (0 ≫ 0) 0 0 (b.inr ≫ b.snd)
<VAR>α : Type u_1<VAR>p✝ : α → Bool<VAR>b : α<VAR>l✝ : List α<VAR>p : α → Bool<VAR>l : List α<VAR>n : Nat<GOAL>findIdx.go p l (n + 1) = findIdx.go p l n + 1
<VAR>σ : Type u_1<VAR>τ : Type u_2<VAR>R : Type u_3<VAR>S : Type u_4<VAR>T : Type u_5<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring S<VAR>inst✝ : CommSemiring T<VAR>f✝ : σ → MvPolynomial τ R<VAR>f : R →+* S<VAR>g : σ → S<VAR>r : R<GOAL>((eval₂Hom f g).comp C) r = f r
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atBot<GOAL>Tendsto (fun x => f x / r) l atBot ↔ 0 < r
<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 b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), (fun x => b ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<GOAL>∃ V, ∃ (_ : ↑x ∈ V), ∃ i, (isFractionPrelocal 𝒜).pred fun x => (a * b) ((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 b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), (fun x => b ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<VAR>y : ↥(Va ⊓ Vb)<GOAL>(fun x => (a * b) ((fun x => ⟨↑x, ⋯⟩) x)) y = HomogeneousLocalization.mk { deg := ja + jb, num := ⟨ra * rb, ⋯⟩, den := ⟨sa * sb, ⋯⟩, 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 b : (x : ↥(unop U)) → at ↑x<VAR>ha : (isLocallyFraction 𝒜).pred a<VAR>hb : (isLocallyFraction 𝒜).pred b<VAR>x : ↥(unop U)<VAR>Va : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>ma : ↑x ∈ Va<VAR>ia : Va ⟶ unop U<VAR>ja : ℕ<VAR>ra : A<VAR>ra_mem : ra ∈ 𝒜 ja<VAR>sa : A<VAR>sa_mem : sa ∈ 𝒜 ja<VAR>hwa : ∀ (x : ↥Va), ↑⟨sa, sa_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wa : ∀ (x : ↥Va), (fun x => a ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := ja, num := ⟨ra, ra_mem⟩, den := ⟨sa, sa_mem⟩, den_mem := ⋯ }<VAR>Vb : Opens ↑(ProjectiveSpectrum.top 𝒜)<VAR>mb : ↑x ∈ Vb<VAR>ib : Vb ⟶ unop U<VAR>jb : ℕ<VAR>rb : A<VAR>rb_mem : rb ∈ 𝒜 jb<VAR>sb : A<VAR>sb_mem : sb ∈ 𝒜 jb<VAR>hwb : ∀ (x : ↥Vb), ↑⟨sb, sb_mem⟩ ∉ (↑x).asHomogeneousIdeal<VAR>wb : ∀ (x : ↥Vb), (fun x => b ((fun x => ⟨↑x, ⋯⟩) x)) x = HomogeneousLocalization.mk { deg := jb, num := ⟨rb, rb_mem⟩, den := ⟨sb, sb_mem⟩, den_mem := ⋯ }<VAR>y : ↥(Va ⊓ Vb)<GOAL>Localization.mk (ra * rb) (⟨sa, ⋯⟩ * ⟨sb, ⋯⟩) = Localization.mk (ra * rb) ⟨sa * sb, ⋯⟩
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<GOAL>IsFiniteAdele 0
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<GOAL>{x | 0 x ∉ adicCompletionIntegers K x}.Finite
<VAR>R : Type u_1<VAR>K : Type u_2<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : IsDedekindDomain R<VAR>inst✝² : Field K<VAR>inst✝¹ : Algebra R K<VAR>inst✝ : IsFractionRing R K<VAR>v : HeightOneSpectrum R<VAR>h_empty : {v | 0 ∉ adicCompletionIntegers K v} = ∅<GOAL>{x | 0 x ∉ adicCompletionIntegers K x}.Finite