ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule<VAR>x : L<GOAL>(ad R L) (D x) ∈ Submodule.map (ad R L).range.subtype (LinearMap.ker (killingForm R ↥(ad R L).range))
<VAR>R : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field R<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra R L<VAR>inst✝ : Module.Finite R L<VAR>D : LieDerivation R L L<VAR>hD : D ∈ (killingForm R (LieDerivation R L L)).orthogonal (ad R L).range.toSubmodule<VAR>x : L<GOAL>(ad R L) (D x) ∈ Submodule.map (ad R L).range.subtype (LinearMap.ker ((killingForm R (LieDerivation R L L)).restrict (ad R L).range.toSubmodule))
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_ne : j z₀ ≠ 0<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<GOAL>m = n
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<VAR>hj_ne : m ≠ n<GOAL>j z₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<VAR>hj_ne : m ≠ n<VAR>this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z<GOAL>j z₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<VAR>hj_ne : m ≠ n<VAR>this : ∀ᶠ (z : 𝕜) in 𝓝 z₀, j z = (z - z₀) ^ (m - n) • g z<GOAL>j z₀ = 0
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<VAR>hj_ne : m ≠ n<VAR>this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z<GOAL>AnalyticAt 𝕜 (fun z => (z - z₀) ^ (m - n) • g z) z₀
<VAR>𝕜 : Type u_1<VAR>inst✝² : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>s : E<VAR>p q : FormalMultilinearSeries 𝕜 𝕜 E<VAR>f g✝ : 𝕜 → E<VAR>n✝ : ℕ<VAR>z z₀ : 𝕜<VAR>m n : ℤ<VAR>hm : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>hn : ∃ g, AnalyticAt 𝕜 g z₀ ∧ g z₀ ≠ 0 ∧ ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • g z<VAR>h_le : n ≤ m<VAR>g : 𝕜 → E<VAR>hg_an : AnalyticAt 𝕜 g z₀<VAR>left✝ : g z₀ ≠ 0<VAR>hg_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ m • g z<VAR>j : 𝕜 → E<VAR>hj_an : AnalyticAt 𝕜 j z₀<VAR>hj_eq : ∀ᶠ (z : 𝕜) in 𝓝[≠] z₀, f z = (z - z₀) ^ n • j z<VAR>hj_ne : m ≠ n<VAR>this : ∃ᶠ (z : 𝕜) in 𝓝[≠] z₀, j z = (z - z₀) ^ (m - n) • g z<GOAL>AnalyticAt 𝕜 (fun z => (z - z₀) ^ (m - n).toNat • g z) z₀
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[>] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<GOAL>∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x<GOAL>∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>A : Type u_1<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra ℝ A<VAR>a b : ℝ<VAR>a' b' : A<VAR>u v u' v' : ℝ → A<VAR>inst✝ : CompleteSpace A<VAR>hu : ∀ x ∈ Ioi a, HasDerivAt u (u' x) x<VAR>hv : ∀ x ∈ Ioi a, HasDerivAt v (v' x) x<VAR>huv : IntegrableOn (u' * v + u * v') (Ioi a) volume<VAR>h_zero : Tendsto (u * v) (𝓝[Ici a \ {a}] a) (𝓝 a')<VAR>h_infty : Tendsto (u * v) atTop (𝓝 b')<VAR>f : ℝ → A := Function.update (u * v) a a'<VAR>hderiv : ∀ x ∈ Ioi a, HasDerivAt f (u' x * v x + u x * v' x) x<VAR>htendsto : Tendsto f atTop (𝓝 b')<GOAL>∫ (x : ℝ) in Ioi a, u' x * v x + u x * v' x = b' - a'
<VAR>T : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} T<VAR>X✝¹ : T<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>X : T<VAR>F : T ⥤ D<VAR>X✝ Y✝ : Under X<VAR>f : X✝ ⟶ Y✝<GOAL>((fun Y => mk (F.map Y.hom)) X✝).hom ≫ F.map f.right = ((fun Y => mk (F.map Y.hom)) Y✝).hom
<VAR>G : Type w<VAR>H : Type x<VAR>α : Type u<VAR>β : Type v<VAR>inst✝² : TopologicalSpace G<VAR>inst✝¹ : Group G<VAR>inst✝ : TopologicalGroup G<VAR>s✝ t : Set G<VAR>ht : IsOpen t<VAR>s : Set G<GOAL>closure s * t = s * t
<VAR>m n : ℤ<GOAL>dist m n = ↑|m - n|
<VAR>m n : ℤ<GOAL>|↑m - ↑n| = ↑|m - n|
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>(adj.homEquiv X Y').symm (f ≫ G.map g) = (adj.homEquiv X Y).symm f ≫ g
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>adj : F ⊣ G<VAR>X' X : C<VAR>Y Y' : D<VAR>f : X ⟶ G.obj Y<VAR>g : Y ⟶ Y'<GOAL>f ≫ G.map g = (adj.homEquiv X Y') ((adj.homEquiv X Y).symm f ≫ g)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ S : Set G<VAR>s : G<VAR>hs : s ∈ S⁻¹<GOAL>s ∈ ↑(closure S)
<VAR>α : Type u_1<VAR>G : Type u_2<VAR>A : Type u_3<VAR>S✝ : Type u_4<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s✝ S : Set G<VAR>s : G<VAR>hs : s ∈ S⁻¹<GOAL>s⁻¹ ∈ closure S
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hle : q ≤ p<GOAL>LiouvilleWith q x
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hle : q ≤ p<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>LiouvilleWith q x
<VAR>p q x y : ℝ<VAR>r : ℚ<VAR>m : ℤ<VAR>n : ℕ<VAR>h : LiouvilleWith p x<VAR>hle : q ≤ p<VAR>C : ℝ<VAR>hC₀ : 0 < C<VAR>hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p<GOAL>∀ (x_1 : ℕ), (1 ≤ x_1 ∧ ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ p) → ∃ m, x ≠ ↑m / ↑x_1 ∧ |x - ↑m / ↑x_1| < C / ↑x_1 ^ q
<VAR>n m : ℕ<GOAL>m ∈ n.smoothNumbers ↔ m ≠ 0 ∧ ∀ p ≤ m, Prime p → p ∣ m → p < n
<VAR>R✝ : Type u_1<VAR>A✝¹ : Type u_2<VAR>inst✝²⁷ : CommSemiring R✝<VAR>inst✝²⁶ : NonUnitalRing A✝¹<VAR>inst✝²⁵ : Module R✝ A✝¹<VAR>inst✝²⁴ : IsScalarTower R✝ A✝¹ A✝¹<VAR>inst✝²³ : SMulCommClass R✝ A✝¹ A✝¹<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : Field S<VAR>inst✝²⁰ : NonUnitalRing A✝<VAR>inst✝¹⁹ : Module R A✝<VAR>inst✝¹⁸ : Module S A✝<VAR>inst✝¹⁷ : IsScalarTower S A✝ A✝<VAR>inst✝¹⁶ : SMulCommClass S A✝ A✝<VAR>inst✝¹⁵ : Algebra R S<VAR>a✝ : A✝<VAR>f✝ : S → R<VAR>inst✝¹⁴ : IsScalarTower R S A✝<VAR>h : QuasispectrumRestricts a✝ f✝<VAR>R₁ : Type u_6<VAR>R₂ : Type u_7<VAR>R₃ : Type u_8<VAR>A : Type u_9<VAR>inst✝¹³ : Semifield R₁<VAR>inst✝¹² : Field R₂<VAR>inst✝¹¹ : Field R₃<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : Module R₁ A<VAR>inst✝⁸ : Module R₂ A<VAR>inst✝⁷ : Module R₃ A<VAR>inst✝⁶ : Algebra R₁ R₂<VAR>inst✝⁵ : Algebra R₂ R₃<VAR>inst✝⁴ : Algebra R₁ R₃<VAR>inst✝³ : IsScalarTower R₁ R₂ R₃<VAR>inst✝² : IsScalarTower R₂ R₃ A<VAR>inst✝¹ : IsScalarTower R₃ A A<VAR>inst✝ : SMulCommClass R₃ A A<VAR>a : A<VAR>f : R₃ → R₂<VAR>g : R₂ → R₁<VAR>e : R₃ → R₁<VAR>hfge : g ∘ f = e<VAR>hf : QuasispectrumRestricts a f<VAR>hg : QuasispectrumRestricts a g<GOAL>Function.LeftInverse e ⇑(algebraMap R₁ R₃)
<VAR>R✝ : Type u_1<VAR>A✝¹ : Type u_2<VAR>inst✝²⁷ : CommSemiring R✝<VAR>inst✝²⁶ : NonUnitalRing A✝¹<VAR>inst✝²⁵ : Module R✝ A✝¹<VAR>inst✝²⁴ : IsScalarTower R✝ A✝¹ A✝¹<VAR>inst✝²³ : SMulCommClass R✝ A✝¹ A✝¹<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : Field S<VAR>inst✝²⁰ : NonUnitalRing A✝<VAR>inst✝¹⁹ : Module R A✝<VAR>inst✝¹⁸ : Module S A✝<VAR>inst✝¹⁷ : IsScalarTower S A✝ A✝<VAR>inst✝¹⁶ : SMulCommClass S A✝ A✝<VAR>inst✝¹⁵ : Algebra R S<VAR>a✝ : A✝<VAR>f✝ : S → R<VAR>inst✝¹⁴ : IsScalarTower R S A✝<VAR>h : QuasispectrumRestricts a✝ f✝<VAR>R₁ : Type u_6<VAR>R₂ : Type u_7<VAR>R₃ : Type u_8<VAR>A : Type u_9<VAR>inst✝¹³ : Semifield R₁<VAR>inst✝¹² : Field R₂<VAR>inst✝¹¹ : Field R₃<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : Module R₁ A<VAR>inst✝⁸ : Module R₂ A<VAR>inst✝⁷ : Module R₃ A<VAR>inst✝⁶ : Algebra R₁ R₂<VAR>inst✝⁵ : Algebra R₂ R₃<VAR>inst✝⁴ : Algebra R₁ R₃<VAR>inst✝³ : IsScalarTower R₁ R₂ R₃<VAR>inst✝² : IsScalarTower R₂ R₃ A<VAR>inst✝¹ : IsScalarTower R₃ A A<VAR>inst✝ : SMulCommClass R₃ A A<VAR>a : A<VAR>f : R₃ → R₂<VAR>g : R₂ → R₁<VAR>e : R₃ → R₁<VAR>hfge : g ∘ f = e<VAR>hf : QuasispectrumRestricts a f<VAR>hg : QuasispectrumRestricts a g<GOAL>⇑(algebraMap R₁ R₃) = ⇑(algebraMap R₂ R₃) ∘ ⇑(algebraMap R₁ R₂)
<VAR>R✝ : Type u_1<VAR>A✝¹ : Type u_2<VAR>inst✝²⁷ : CommSemiring R✝<VAR>inst✝²⁶ : NonUnitalRing A✝¹<VAR>inst✝²⁵ : Module R✝ A✝¹<VAR>inst✝²⁴ : IsScalarTower R✝ A✝¹ A✝¹<VAR>inst✝²³ : SMulCommClass R✝ A✝¹ A✝¹<VAR>R : Type u_3<VAR>S : Type u_4<VAR>A✝ : Type u_5<VAR>inst✝²² : Semifield R<VAR>inst✝²¹ : Field S<VAR>inst✝²⁰ : NonUnitalRing A✝<VAR>inst✝¹⁹ : Module R A✝<VAR>inst✝¹⁸ : Module S A✝<VAR>inst✝¹⁷ : IsScalarTower S A✝ A✝<VAR>inst✝¹⁶ : SMulCommClass S A✝ A✝<VAR>inst✝¹⁵ : Algebra R S<VAR>a✝ : A✝<VAR>f✝ : S → R<VAR>inst✝¹⁴ : IsScalarTower R S A✝<VAR>h : QuasispectrumRestricts a✝ f✝<VAR>R₁ : Type u_6<VAR>R₂ : Type u_7<VAR>R₃ : Type u_8<VAR>A : Type u_9<VAR>inst✝¹³ : Semifield R₁<VAR>inst✝¹² : Field R₂<VAR>inst✝¹¹ : Field R₃<VAR>inst✝¹⁰ : NonUnitalRing A<VAR>inst✝⁹ : Module R₁ A<VAR>inst✝⁸ : Module R₂ A<VAR>inst✝⁷ : Module R₃ A<VAR>inst✝⁶ : Algebra R₁ R₂<VAR>inst✝⁵ : Algebra R₂ R₃<VAR>inst✝⁴ : Algebra R₁ R₃<VAR>inst✝³ : IsScalarTower R₁ R₂ R₃<VAR>inst✝² : IsScalarTower R₂ R₃ A<VAR>inst✝¹ : IsScalarTower R₃ A A<VAR>inst✝ : SMulCommClass R₃ A A<VAR>a : A<VAR>f : R₃ → R₂<VAR>g : R₂ → R₁<VAR>e : R₃ → R₁<VAR>hfge : g ∘ f = e<VAR>hf : QuasispectrumRestricts a f<VAR>hg : QuasispectrumRestricts a g<GOAL>Set.RightInvOn e (⇑(algebraMap R₁ R₃)) (quasispectrum R₃ a)
<VAR>a : EReal<VAR>h : a < 0<VAR>h' : a ≠ ⊥<GOAL>a⁻¹ < 0
<VAR>R : Type u_1<VAR>inst✝ : LinearOrderedRing R<VAR>a b n : ℤ<VAR>x : R<GOAL>↑|a| = |↑a|
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : CommSemiring S<VAR>s : Set (Set R)<GOAL>zeroLocus (⋃ s' ∈ s, s') = ⋂ s' ∈ s, zeroLocus s'
<VAR>C : Type u₁<VAR>D : Type u₂<VAR>E : Type u₃<VAR>inst✝³ : Category.{v₁, u₁} C<VAR>inst✝² : Category.{v₂, u₂} D<VAR>inst✝¹ : Category.{v₃, u₃} E<VAR>i : D ⥤ C<VAR>j : C ⥤ D<VAR>inst✝ : Coreflective j<VAR>A : D<VAR>h : A ∈ j.essImage<GOAL>IsIso ((coreflectorAdjunction j).counit.app A)
<VAR>𝕜 : Type u_1<VAR>inst✝¹⁰ : NontriviallyNormedField 𝕜<VAR>D : Type uD<VAR>inst✝⁹ : NormedAddCommGroup D<VAR>inst✝⁸ : NormedSpace 𝕜 D<VAR>E : Type uE<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace 𝕜 E<VAR>F : Type uF<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace 𝕜 F<VAR>G : Type uG<VAR>inst✝³ : NormedAddCommGroup G<VAR>inst✝² : NormedSpace 𝕜 G<VAR>X : Type u_2<VAR>inst✝¹ : NormedAddCommGroup X<VAR>inst✝ : NormedSpace 𝕜 X<VAR>s✝ s₁ t u✝ : Set E<VAR>f f₁ : E → F<VAR>g : F → G<VAR>x✝ x₀ : E<VAR>c✝ : F<VAR>b : E × F → G<VAR>m✝ n✝ : ℕ∞<VAR>p : E → FormalMultilinearSeries 𝕜 E F<VAR>s : Set E<VAR>hs : UniqueDiffOn 𝕜 s<VAR>n : ℕ∞<VAR>c : E → F →L[𝕜] G<VAR>hc : ContDiffOn 𝕜 n c s<VAR>i : ℕ<VAR>hi : ↑i ≤ n<VAR>x : E<VAR>hx : x ∈ s<VAR>u : F<VAR>m : Fin i → E<GOAL>(iteratedFDerivWithin 𝕜 i (fun y => (c y) u) s x) m = ((iteratedFDerivWithin 𝕜 i c s x) m) u
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommSemiring R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>t : Set (ProjectiveSpectrum 𝒜)<VAR>f : A<GOAL>f ∈ vanishingIdeal t ↔ ∀ x ∈ t, f ∈ x.asHomogeneousIdeal
<VAR>S : Type u_1<VAR>T : Type u_2<VAR>R : Type u_3<VAR>M : Type u_4<VAR>N : Type u_5<VAR>P : Type u_6<VAR>A : Type u_7<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : AddCommGroup M<VAR>inst✝² : AddCommGroup N<VAR>inst✝¹ : Module R M<VAR>inst✝ : Module R N<VAR>Q : QuadraticMap R M N<VAR>x y : M<GOAL>polar (⇑Q) (-x) y = -polar (⇑Q) x y
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝³ : CommRing R<VAR>inst✝² : Ring S<VAR>f : R[X]<VAR>inst✝¹ : Algebra R S<VAR>T : Type u_1<VAR>inst✝ : CommRing T<VAR>i : R →+* T<VAR>x : T<VAR>hx : eval₂ i x f = 0<VAR>h : IsAdjoinRoot S f<VAR>a : R<GOAL>(lift i x hx h) ((algebraMap R S) a) = i a
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>A : Type u_3<VAR>a a₁ a₂ b c : G<VAR>inst✝¹ : Group G<VAR>inst✝ : AddGroup A<VAR>s : Set G<VAR>hs : IsSubgroup s<VAR>x y : G<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x / y ∈ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Computation α<VAR>a : α<VAR>n : ℕ<VAR>h : s.Results a n<VAR>this : s.Terminates<GOAL>s.think.length = n + 1
<VAR>α : Type u_1<VAR>inst✝¹ : Ring α<VAR>inst✝ : LinearOrder α<VAR>a✝ b✝ a b : α<GOAL>a ∣ |b| ↔ a ∣ b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>x : α<GOAL>Tendsto (fun n => ↑((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 ((fun x => (f x, g x)) x))
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>inst✝² : Countable ι<VAR>f✝ g✝ : α → β<VAR>m : MeasurableSpace α<VAR>inst✝¹ : TopologicalSpace β<VAR>inst✝ : TopologicalSpace γ<VAR>f : α → β<VAR>g : α → γ<VAR>hf : StronglyMeasurable f<VAR>hg : StronglyMeasurable g<VAR>x : α<GOAL>Tendsto (fun n => ↑((fun n => (hf.approx n).pair (hg.approx n)) n) x) atTop (𝓝 (f x) ×ˢ 𝓝 (g x))
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<GOAL>I.radical = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<GOAL>InfSet.sInf {J | I ≤ J ∧ J.IsPrime} = InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<GOAL>InfSet.sInf {J | I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime}
<VAR>ι : Type u_1<VAR>σ : Type u_2<VAR>A : Type u_3<VAR>inst✝⁴ : CommRing A<VAR>inst✝³ : LinearOrderedCancelAddCommMonoid ι<VAR>inst✝² : SetLike σ A<VAR>inst✝¹ : AddSubmonoidClass σ A<VAR>𝒜 : ι → σ<VAR>inst✝ : GradedRing 𝒜<VAR>I : Ideal A<VAR>hI : IsHomogeneous 𝒜 I<GOAL>InfSet.sInf {J | IsHomogeneous 𝒜 J ∧ I ≤ J ∧ J.IsPrime} ≤ InfSet.sInf {J | I ≤ J ∧ J.IsPrime}
<VAR>C : Type u₁<VAR>inst✝² : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝¹ : Category.{v₂, u₂} D<VAR>E : Type u₃<VAR>inst✝ : Category.{v₃, u₃} E<VAR>F G : C ⥤ D<VAR>α : F ≅ G<VAR>W X X' : D<VAR>Y : C<VAR>f : W ⟶ X<VAR>g : X ⟶ F.obj Y<VAR>f' : W ⟶ X'<VAR>g' : X' ⟶ F.obj Y<GOAL>f ≫ g ≫ α.hom.app Y = f' ≫ g' ≫ α.hom.app Y ↔ f ≫ g = f' ≫ g'
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<GOAL>fp.IsEquipartition
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>hn : ¬fp.IsEquipartition<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>hn : ∃ a ∈ fp.parts, ∃ b ∈ fp.parts, b.card + 1 < a.card<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<GOAL>False
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<GOAL>∃ H inst, H.CliqueFree (r + 1) ∧ G.edgeFinset.card < H.edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<GOAL>G.edgeFinset.card < (G.replaceVertex v w).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<VAR>large_eq : fp.part w = large<GOAL>G.edgeFinset.card < (G.replaceVertex v w).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<VAR>large_eq : fp.part w = large<VAR>small_eq : fp.part v = small<GOAL>G.edgeFinset.card < (G.replaceVertex v w).edgeFinset.card
<VAR>V : Type u_1<VAR>inst✝² : Fintype V<VAR>inst✝¹ : DecidableEq V<VAR>G : SimpleGraph V<VAR>inst✝ : DecidableRel G.Adj<VAR>n r : ℕ<VAR>s t u : V<VAR>h : G.IsTuranMaximal r<VAR>fp : Finpartition univ := h.finpartition<VAR>large : Finset V<VAR>hl : large ∈ fp.parts<VAR>small : Finset V<VAR>hs : small ∈ fp.parts<VAR>ineq : small.card + 1 < large.card<VAR>w : V<VAR>hw : w ∈ large<VAR>v : V<VAR>hv : v ∈ small<VAR>cf : G.CliqueFree (r + 1)<VAR>large_eq : fp.part w = large<VAR>small_eq : fp.part v = small<VAR>ha : G.Adj v w<GOAL>G.edgeFinset.card < (G.replaceVertex v w).edgeFinset.card