ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>Z : Type u_4<VAR>T : Type u_5<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : TopologicalSpace T<VAR>K : Set X<VAR>U : Set Y<VAR>f g : C(X, Y)<GOAL>Inseparable ⇑f ⇑g ↔ Inseparable f g
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B B₁ B₂ : Set α<VAR>M : Matroid α<VAR>inst✝ : M.InfiniteRk<VAR>h : M.FiniteRk<GOAL>False
<VAR>α : Type u_1<VAR>M✝ : Matroid α<VAR>B✝ B₁ B₂ : Set α<VAR>M : Matroid α<VAR>inst✝ : M.InfiniteRk<VAR>h : M.FiniteRk<VAR>B : Set α<VAR>hB : M.Base B<GOAL>False
<VAR>V : Type u_1<VAR>V' : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup V<VAR>inst✝⁴ : NormedAddCommGroup V'<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : InnerProductSpace ℝ V'<VAR>inst✝¹ : Fact (finrank ℝ V = 2)<VAR>inst✝ : Fact (finrank ℝ V' = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>o.oangle x (r • y) = o.oangle x y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : PartialOrder α<VAR>inst✝ : PredOrder α<VAR>a b : α<VAR>ha : ¬IsMin a<VAR>hb : ¬IsMin b<GOAL>pred a = pred b ↔ a = b
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>inst✝¹ : DecidableEq β<VAR>f✝ g : α → β<VAR>s✝ : Finset α<VAR>t : Finset β<VAR>a✝ : α<VAR>b c : β<VAR>inst✝ : DecidableEq α<VAR>f : α → β<VAR>a : α<VAR>s : Finset α<GOAL>image f (insert a s) = insert (f a) (image f s)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} K L<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} K L<VAR>hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))<GOAL>discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis = (-1) ^ ((↑p - 1) / 2) * ↑↑p ^ (↑p - 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} K L<VAR>hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))<GOAL>(-1) ^ ((↑p - 1) / 2) = (-1) ^ (φ (↑p ^ (0 + 1)) / 2)
<VAR>p : ℕ+<VAR>k : ℕ<VAR>K : Type u<VAR>L : Type v<VAR>ζ : L<VAR>inst✝³ : Field K<VAR>inst✝² : Field L<VAR>inst✝¹ : Algebra K L<VAR>inst✝ : IsCyclotomicExtension {p} K L<VAR>hp : Fact (Nat.Prime ↑p)<VAR>hζ : IsPrimitiveRoot ζ ↑p<VAR>hirr : Irreducible (cyclotomic (↑p) K)<VAR>hodd : p ≠ 2<VAR>this : IsCyclotomicExtension {p ^ (0 + 1)} K L<VAR>hζ' : IsPrimitiveRoot ζ ↑(p ^ (0 + 1))<GOAL>↑↑p ^ (↑p - 2) = ↑↑p ^ (↑p ^ 0 * ((↑p - 1) * (0 + 1) - 1))
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>W✝ : Projective R<VAR>F : Type u<VAR>inst✝ : Field F<VAR>W : Projective F<VAR>P : Fin 3 → F<VAR>hPz : P 2 ≠ 0<GOAL>(fun m => m • ![P 0 / P 2, P 1 / P 2, 1]) (Units.mk0 (P 2) hPz) = P
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<GOAL>xn a1 m < xn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : xn a1 m ≤ xn a1 n<GOAL>xn a1 m < xn a1 (n + 1)
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : xn a1 m ≤ xn a1 n<GOAL>xn a1 m < xn a1 n * a + Pell.d a1 * yn a1 n
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : xn a1 m ≤ xn a1 n<GOAL>xn a1 n < xn a1 n * a
<VAR>a : ℕ<VAR>a1 : 1 < a<VAR>m n : ℕ<VAR>h : m < n + 1<VAR>this : xn a1 m ≤ xn a1 n<VAR>t : xn a1 n * 1 < xn a1 n * a<GOAL>xn a1 n < xn a1 n * a
<VAR>R : Type u<VAR>S : Type v<VAR>T : Type w<VAR>a b : R<VAR>n✝ : ℕ<VAR>inst✝¹ : CommRing R<VAR>inst✝ : IsDomain R<VAR>p q : R[X]<VAR>ha : a ≠ 0<VAR>n : ℕ<GOAL>((monomial n) a).roots = n • {0}
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>vectorSpan k (range p) = Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<GOAL>Submodule.span k ((fun x => p i₀ -ᵥ x) '' (p '' (univ \ {i₀}))) = Submodule.span k (range fun i => p i₀ -ᵥ p ↑i)
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<VAR>v : V<GOAL>v ∈ (fun x => p i₀ -ᵥ x) '' (p '' (univ \ {i₀})) ↔ v ∈ range fun i => p i₀ -ᵥ p ↑i
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>inst✝ : AffineSpace V P<VAR>ι : Type u_4<VAR>p : ι → P<VAR>i₀ : ι<VAR>v : V<GOAL>(∃ x, (∃ x_1, (x_1 ∈ univ ∧ ¬x_1 = i₀) ∧ p x_1 = x) ∧ p i₀ -ᵥ x = v) ↔ ∃ a, ∃ (_ : a ≠ i₀), p i₀ -ᵥ p a = v
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<GOAL>∃ x, (engel K x).IsCartanSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<GOAL>∃ x, (engel K x).IsCartanSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<GOAL>(engel K x).IsCartanSubalgebra
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<GOAL>IsNilpotent K ↥(engel K x)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<GOAL>∀ x_1 ∈ engel K x, engel K x ≤ engel K x_1
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y : L<VAR>hy : y ∈ engel K x<GOAL>engel K x ≤ engel K y
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<GOAL>engel K x ≤ engel K y
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<GOAL>IsBot Ex
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<GOAL>IsMin Ex
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y✝ : L<VAR>hy✝ : y✝ ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>hyx : ⟨engel K y, ⋯⟩ ≤ Ex<GOAL>Ex ≤ ⟨engel K y, ⋯⟩
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y✝ : L<VAR>hy✝ : y✝ ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>hyx : ⟨engel K y, ⋯⟩ ≤ Ex<GOAL>finrank K ↥(engel K x) ≤ finrank K ↥(engel K y)
<VAR>K : Type u_1<VAR>L : Type u_2<VAR>inst✝³ : Field K<VAR>inst✝² : LieRing L<VAR>inst✝¹ : LieAlgebra K L<VAR>inst✝ : Module.Finite K L<VAR>h : ↑(finrank K L) ≤ #K<VAR>x : L<VAR>hx : IsRegular K x<VAR>y✝ : L<VAR>hy✝ : y✝ ∈ engel K x<VAR>Ex : ↑{x_1 | ∃ z ∈ engel K x, engel K z = x_1} := ⟨engel K x, ⋯⟩<VAR>y : L<VAR>hy : y ∈ engel K x<VAR>hyx : ⟨engel K y, ⋯⟩ ≤ Ex<GOAL>rank K L ≤ finrank K ↥(engel K y)
<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>r : R<VAR>f : R → R<GOAL>cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)
<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>r : R<VAR>f : R → R<VAR>h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))<GOAL>cfc f ((algebraMap R A) r) = (algebraMap R A) (f r)
<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>r : R<VAR>f : R → R<VAR>h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))<GOAL>(cfcHom ⋯) { toFun := (spectrum R ((algebraMap R A) r)).restrict f, continuous_toFun := ⋯ } = (cfcHom ⋯) ((algebraMap R C(↑(spectrum R ((algebraMap R A) r)), R)) (f r))
<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>r : R<VAR>f : R → R<VAR>h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))<VAR>x : R<VAR>hx : x ∈ spectrum R ((algebraMap R A) r)<GOAL>(spectrum R ((algebraMap R A) r)).restrict f ⟨x, hx⟩ = (algebraMap R R) (f r)
<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>r : R<VAR>f : R → R<VAR>h₁ : ContinuousOn f (spectrum R ((algebraMap R A) r))<VAR>x : R<VAR>hx✝ : x ∈ spectrum R ((algebraMap R A) r)<VAR>hx : x ∈ {r}<GOAL>(spectrum R ((algebraMap R A) r)).restrict f ⟨x, hx✝⟩ = (algebraMap R R) (f r)
<VAR>ι : Sort u_1<VAR>α : Type u_2<VAR>β : Type u_3<VAR>inst✝³ : PartialOrder α<VAR>inst✝² : PartialOrder β<VAR>inst✝¹ : OrderBot α<VAR>inst✝ : OrderBot β<VAR>f : α ≃o β<GOAL>IsAtomic α ↔ IsAtomic β
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<GOAL>‖lsmul 𝕜 𝕜'‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<VAR>x : 𝕜'<GOAL>‖(lsmul 𝕜 𝕜') x‖ ≤ 1 * ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>inst✝⁵ : SeminormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>inst✝³ : NormedField 𝕜'<VAR>inst✝² : NormedAlgebra 𝕜 𝕜'<VAR>inst✝¹ : NormedSpace 𝕜' E<VAR>inst✝ : IsScalarTower 𝕜 𝕜' E<VAR>x : 𝕜'<GOAL>‖(lsmul 𝕜 𝕜') x‖ ≤ ‖x‖
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type u_1<VAR>f✝ : Filter α<VAR>s : Set α<VAR>a : α<VAR>g : Filter α<VAR>p : Filter α → Prop<VAR>hp : Monotone p<VAR>H : ∀ (f : Ultrafilter α), ↑f ≤ g → p ↑f<VAR>f : Filter α<VAR>hf : f.NeBot<VAR>hfg : f ≤ g<GOAL>p f
<VAR>R : Type u<VAR>S : Type v<VAR>F : Type u_1<VAR>inst✝³ : Semiring R<VAR>inst✝² : Semiring S<VAR>inst✝¹ : FunLike F R S<VAR>rc : RingHomClass F R S<VAR>f : F<VAR>I✝ J : Ideal R<VAR>K L : Ideal S<VAR>G : Type u_2<VAR>inst✝ : FunLike G S R<VAR>rcg : RingHomClass G S R<VAR>I : Ideal S<VAR>h : I = ⊤<GOAL>comap f I = ⊤
<VAR>R : Type u<VAR>inst✝¹ : CommRing R<VAR>S : Type v<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>p : Ideal R<VAR>P : Ideal S<VAR>e : ℕ<VAR>he : e ≠ 0<VAR>hle : map f p ≤ P ^ e<VAR>hnle : ¬map f p ≤ P ^ (e + 1)<GOAL>ramificationIdx f p P ≠ 0
<VAR>R : Type u_1<VAR>inst✝¹ : Semiring R<VAR>S : Type u_2<VAR>inst✝ : Semiring S<VAR>s : S<VAR>G : R →+* S<VAR>n : ℕ<VAR>f : R⟦X⟧<GOAL>eval₂ G s (trunc n f) = ∑ i ∈ range n, G ((coeff R i) f) * s ^ i
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsNoetherianRing R<GOAL>IsNoetherianRing (MvPolynomial (Fin 0) R)
<VAR>R : Type u<VAR>S : Type u_1<VAR>σ : Type v<VAR>M : Type w<VAR>inst✝⁴ : CommRing R<VAR>inst✝³ : CommRing S<VAR>inst✝² : AddCommGroup M<VAR>inst✝¹ : Module R M<VAR>inst✝ : IsNoetherianRing R<GOAL>R ≃+* MvPolynomial (Fin 0) R
<VAR>R : Type u<VAR>S : Type v<VAR>a b c d : R<VAR>n m : ℕ<VAR>inst✝¹ : Ring R<VAR>inst✝ : Nontrivial R<VAR>x : R<GOAL>(X - C x).natDegree = 1
<VAR>𝕜 : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : NormedField 𝕜<VAR>inst✝² : NormedRing A<VAR>inst✝¹ : NormedAlgebra 𝕜 A<VAR>inst✝ : CompleteSpace A<VAR>a : A<VAR>k : 𝕜<VAR>hk : k ∈ σ a<GOAL>k ∈ Metric.closedBall 0 (‖a‖ * ‖1‖)
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<VAR>huc : CauchySeq u<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<VAR>huc : CauchySeq u<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : Tendsto u atTop (𝓝 x)<GOAL>∃ x ∈ s, l ≤ 𝓝 x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<VAR>huc : CauchySeq u<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>N : ℕ<VAR>x✝ : True<GOAL>ball x (V N) ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<VAR>huc : CauchySeq u<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>N : ℕ<VAR>x✝ : True<VAR>n : ℕ<VAR>hNn : N ≤ n<VAR>hn : u n ∈ ball x (W N)<GOAL>ball x (V N) ∈ l
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : UniformSpace X<VAR>s : Set X<VAR>inst✝ : (𝓤 X).IsCountablyGenerated<VAR>hs : IsSeqCompact s<VAR>l : Filter X<VAR>hl : Cauchy l<VAR>hls : l ≤ 𝓟 s<VAR>this : l.NeBot<VAR>V : ℕ → Set (X × X)<VAR>hV : (𝓤 X).HasAntitoneBasis V<VAR>W : ℕ → Set (X × X)<VAR>hW : ∀ (n : ℕ), W n ∈ 𝓤 X<VAR>hWV : ∀ (n : ℕ), W n ○ W n ⊆ V n<VAR>hWV' : ∀ (n : ℕ), W n ⊆ V n<VAR>t : ℕ → Set X<VAR>ht_anti : Antitone t<VAR>htl : ∀ (n : ℕ), t n ∈ l<VAR>htW : ∀ (n : ℕ), t n ×ˢ t n ⊆ W n<VAR>hts : ∀ (n : ℕ), t n ⊆ s<VAR>u : ℕ → X<VAR>hu : ∀ (n : ℕ), u n ∈ t n<VAR>huc : CauchySeq u<VAR>x : X<VAR>hxs : x ∈ s<VAR>hx : Tendsto u atTop (𝓝 x)<VAR>N : ℕ<VAR>x✝ : True<VAR>n : ℕ<VAR>hNn : N ≤ n<VAR>hn : u n ∈ ball x (W N)<VAR>y : X<VAR>hy : y ∈ t n<GOAL>(u n, (x, y).2) ∈ t N ×ˢ t N
<VAR>x : ℝ*<VAR>r : ℝ<GOAL>x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ
<VAR>k : Type u_1<VAR>V : Type u_2<VAR>P : Type u_3<VAR>inst✝³ : Ring k<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module k V<VAR>S : AffineSpace V P<VAR>ι : Type u_4<VAR>s : Finset ι<VAR>ι₂ : Type u_5<VAR>s₂ : Finset ι₂<VAR>inst✝ : DecidableEq ι<VAR>i j : ι<VAR>h : i ≠ j<GOAL>weightedVSubVSubWeights k i j j = -1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>B : Set ι<VAR>Bcbl : B.Countable<VAR>f : ι → α<VAR>i₀ : ι<VAR>h : f i₀ = ⊤<GOAL>∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>B : Set ι<VAR>Bcbl : B.Countable<VAR>f : ι → α<VAR>i₀ : ι<VAR>h : f i₀ = ⊤<VAR>hB : B = ∅<GOAL>∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Type u_4<VAR>ι' : Sort u_5<VAR>inst✝ : CompleteLattice α<VAR>B : Set ι<VAR>Bcbl : B.Countable<VAR>f : ι → α<VAR>i₀ : ι<VAR>h : f i₀ = ⊤<VAR>Bnonempty : B.Nonempty<GOAL>∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ ≠ 0<GOAL>p₁ ≠ p₂
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>inst✝⁴ : NormedAddCommGroup V<VAR>inst✝³ : InnerProductSpace ℝ V<VAR>inst✝² : MetricSpace P<VAR>inst✝¹ : NormedAddTorsor V P<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>inst✝ : Module.Oriented ℝ V (Fin 2)<VAR>p₁ p₂ p₃ : P<VAR>h : ∡ p₁ p₂ p₃ ≠ 0<GOAL>p₁ -ᵥ p₂ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Group α<VAR>a : α<VAR>ha : 1 < a⁺ᵐ<GOAL>a⁺ᵐ = a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : Group α<VAR>a : α<VAR>ha : 1 < a<GOAL>a⁺ᵐ = a