ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤})<VAR>x : α<VAR>hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ<VAR>hx : x ∉ {x | f x = ⊤}<GOAL>x ∈ {a | f a ≤ ⨍⁻ (a : α) in s, f a ∂μ}
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤})<VAR>x : α<VAR>hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ<VAR>hx : x ∉ {x | f x = ⊤}<GOAL>∀ᵐ (x : α) ∂μ.restrict s, f x ≠ ⊤
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>m0 : MeasurableSpace α<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>inst✝³ : CompleteSpace E<VAR>inst✝² : NormedAddCommGroup F<VAR>inst✝¹ : NormedSpace ℝ F<VAR>inst✝ : CompleteSpace F<VAR>μ ν : Measure α<VAR>s t N : Set α<VAR>f : α → ℝ≥0∞<VAR>hμ : μ s ≠ 0<VAR>hμ₁ : μ s ≠ ⊤<VAR>hf : AEMeasurable f (μ.restrict s)<VAR>h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤<VAR>this : 0 < (μ.restrict s) ({a | (f a).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ} \ {x | f x = ⊤})<VAR>x : α<VAR>hfx : (f x).toReal ≤ ⨍ (a : α) in s, (f a).toReal ∂μ<VAR>hx : x ∉ {x | f x = ⊤}<GOAL>(μ.restrict s) {a | f a = ⊤} = 0
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>Continuous transReflReparamAux
<VAR>X : Type u<VAR>Y : Type v<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x₀ x₁ : X<GOAL>∀ (x : ↑I), ↑x = 1 / 2 → 2 * ↑x = 1
<VAR>a b m n✝ p n d : ℕ<GOAL>d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
<VAR>a b m n p d : ℕ<GOAL>d ∣ 0 ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ 0
<VAR>a b m n✝ p n d : ℕ<VAR>hn : n ≠ 0<GOAL>d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
<VAR>a b m n✝ p n : ℕ<VAR>hn : n ≠ 0<GOAL>0 ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ 0 → p ^ k ∣ n
<VAR>a b m n✝ p n d : ℕ<VAR>hn : n ≠ 0<VAR>hd : d ≠ 0<GOAL>d ∣ n ↔ ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n
<VAR>a b m n✝ p n d : ℕ<VAR>hn : n ≠ 0<VAR>hd : d ≠ 0<GOAL>(∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → d ∣ n
<VAR>a b m n✝ p n d : ℕ<VAR>hn : n ≠ 0<VAR>hd : d ≠ 0<GOAL>(∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n) → ∀ (p : ℕ), Prime p → d.factorization p ≤ n.factorization p
<VAR>a b m n✝ p✝ n d : ℕ<VAR>hn : n ≠ 0<VAR>hd : d ≠ 0<VAR>h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n<VAR>p : ℕ<VAR>pp : Prime p<GOAL>d.factorization p ≤ n.factorization p
<VAR>a b m n✝ p✝ n d : ℕ<VAR>hn : n ≠ 0<VAR>hd : d ≠ 0<VAR>h : ∀ (p k : ℕ), Prime p → p ^ k ∣ d → p ^ k ∣ n<VAR>p : ℕ<VAR>pp : Prime p<GOAL>p ^ d.factorization p ∣ n
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>Injective fun a => b / a
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>G : Type u_3<VAR>M : Type u_4<VAR>inst✝ : Group G<VAR>a b c d : G<VAR>n : ℤ<GOAL>Injective fun a => b * a⁻¹
<VAR>a b : Ordinal.{u_1}<GOAL>a ⨳ succ b = a ⨳ b ♯ a
<GOAL>schnirelmannDensity (setOf Odd) = 2⁻¹
<VAR>h : setOf Odd = {n | n % 2 = 1}<GOAL>schnirelmannDensity (setOf Odd) = 2⁻¹
<VAR>h : setOf Odd = {n | n % 2 = 1}<GOAL>schnirelmannDensity {n | n % 2 = 1} = 2⁻¹
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ≅ b<VAR>inst✝ : p.IsHomLift f φ.hom<GOAL>f ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 R
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ≅ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsHomLift (p.map φ.hom) φ.hom<GOAL>p.map φ.hom ≫ eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯ = 𝟙 (p.obj a✝)
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>f : R ⟶ S<VAR>φ : a ≅ b<VAR>inst✝ : p.IsHomLift f φ.hom<GOAL>(eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ f = 𝟙 S
<VAR>𝒮 : Type u₁<VAR>𝒳 : Type u₂<VAR>inst✝² : Category.{v₁, u₂} 𝒳<VAR>inst✝¹ : Category.{v₂, u₁} 𝒮<VAR>p : 𝒳 ⥤ 𝒮<VAR>a✝ b✝ : 𝒳<VAR>φ : a✝ ≅ b✝<VAR>R S : 𝒮<VAR>a b : 𝒳<VAR>inst✝ : p.IsHomLift (p.map φ.hom) φ.hom<GOAL>(eqToHom ⋯ ≫ (p.mapIso φ).inv ≫ eqToHom ⋯) ≫ p.map φ.hom = 𝟙 (p.obj b✝)
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>f x = f y
<VAR>E : Type u_1<VAR>inst✝⁷ : NormedAddCommGroup E<VAR>inst✝⁶ : NormedSpace ℝ E<VAR>F : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup F<VAR>inst✝⁴ : NormedSpace ℝ F<VAR>𝕜 : Type u_3<VAR>G : Type u_4<VAR>inst✝³ : RCLike 𝕜<VAR>inst✝² : NormedSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace 𝕜 G<VAR>f g : E → G<VAR>C : ℝ<VAR>s : Set E<VAR>x y : E<VAR>f' g' : E → E →L[𝕜] G<VAR>φ : E →L[𝕜] G<VAR>hs : Convex ℝ s<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hf' : ∀ x ∈ s, fderivWithin 𝕜 f s x = 0<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>bound : ∀ x ∈ s, ‖fderivWithin 𝕜 f s x‖ ≤ 0<GOAL>f x = f y
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>x : M<VAR>h : f.HasEigenvector μ x<GOAL>f.HasEigenvalue μ
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>x : M<VAR>h : f.HasEigenvector μ x<GOAL>∃ x ∈ f.eigenspace μ, x ≠ 0
<VAR>K R : Type v<VAR>V M : Type w<VAR>inst✝⁵ : CommRing R<VAR>inst✝⁴ : AddCommGroup M<VAR>inst✝³ : Module R M<VAR>inst✝² : Field K<VAR>inst✝¹ : AddCommGroup V<VAR>inst✝ : Module K V<VAR>f : End R M<VAR>μ : R<VAR>x : M<VAR>h : f.HasEigenvector μ x<GOAL>x ∈ f.eigenspace μ ∧ x ≠ 0
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n i j : ℤ<VAR>h : n + i = j<GOAL>QuasiIsoAt ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i ↔ QuasiIsoAt φ j
<VAR>C : Type u_1<VAR>inst✝² : Category.{u_2, u_1} C<VAR>inst✝¹ : Preadditive C<VAR>inst✝ : CategoryWithHomology C<VAR>K L : CochainComplex C ℤ<VAR>φ : K ⟶ L<VAR>n i j : ℤ<VAR>h : n + i = j<GOAL>IsIso (homologyMap ((CategoryTheory.shiftFunctor (HomologicalComplex C (up ℤ)) n).map φ) i) ↔ IsIso (homologyMap φ j)
<VAR>α : Type u_1<VAR>s t : Multiset α<GOAL>∀ (a b : List α), ⟦a⟧ ∈ powerset ⟦b⟧ ↔ ⟦a⟧ ≤ ⟦b⟧
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>A.mul.unop ≫ A.one.unop ▷ unop A.X = (λ_ (unop A.X)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>(λ_ A.X).hom.unop = (λ_ (unop A.X)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>A.mul.unop ≫ unop A.X ◁ A.one.unop = (ρ_ (unop A.X)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>(ρ_ A.X).hom.unop = (ρ_ (unop A.X)).inv
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>A.mul.unop ≫ unop A.X ◁ A.mul.unop = A.mul.unop ≫ A.mul.unop ▷ unop A.X ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom
<VAR>C : Type u₁<VAR>inst✝¹ : Category.{v₁, u₁} C<VAR>inst✝ : MonoidalCategory C<VAR>M : Comon_ C<VAR>A : Mon_ Cᵒᵖ<GOAL>((α_ A.X A.X A.X).inv ≫ A.mul ▷ A.X ≫ A.mul).unop = (A.mul ▷ A.X ≫ A.mul).unop ≫ (α_ (unop A.X) (unop A.X) (unop A.X)).hom
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<GOAL>I.IsMaximal ↔ ∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<GOAL>I.IsMaximal ↔ ∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<GOAL>∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<GOAL>∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<GOAL>∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<GOAL>∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<VAR>x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))<VAR>hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)<GOAL>∃ x, I = vanishingIdeal {x}
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<VAR>x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))<VAR>hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)<GOAL>vanishingIdeal {x} ≤ I
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<VAR>x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))<VAR>hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ vanishingIdeal {x}<GOAL>p ∈ I
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<VAR>x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))<VAR>hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)<VAR>p : MvPolynomial σ k<VAR>hp : p ∈ vanishingIdeal {x}<GOAL>∑ d ∈ p.support, ((Ideal.Quotient.mk I).comp C) (coeff d p) * ∏ i : σ, (Ideal.Quotient.mk I) (X i) ^ d i = 0
<VAR>k : Type u_1<VAR>inst✝² : Field k<VAR>σ : Type u_2<VAR>inst✝¹ : IsAlgClosed k<VAR>inst✝ : Finite σ<VAR>I : Ideal (MvPolynomial σ k)<VAR>val✝ : Fintype σ<VAR>hI : I.IsMaximal<VAR>this✝ : I.IsMaximal := hI<VAR>this : Field (MvPolynomial σ k ⧸ I) := Quotient.field I<VAR>ϕ : k →+* MvPolynomial σ k ⧸ I := (Ideal.Quotient.mk I).comp C<VAR>hϕ : Function.Bijective ⇑ϕ<VAR>φ : MvPolynomial σ k ⧸ I → k<VAR>hφ : Function.RightInverse φ ⇑ϕ<VAR>x : σ → k := fun s => φ ((Ideal.Quotient.mk I) (X s))<VAR>hx : ∀ (s : σ), ϕ (x s) = (Ideal.Quotient.mk I) (X s)<VAR>p : MvPolynomial σ k<VAR>hp : ∑ d ∈ p.support, coeff d p * ∏ i : σ, x i ^ d i = 0<GOAL>∑ d ∈ p.support, ((Ideal.Quotient.mk I).comp C) (coeff d p) * ∏ i : σ, (Ideal.Quotient.mk I) (X i) ^ d i = 0
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ y = 0<GOAL>‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>x y : V<VAR>h : ⟪x, -y⟫_ℝ = 0<VAR>h0 : x ≠ 0 ∨ -y = 0<GOAL>‖x‖ / Real.cos (angle x (x - y)) = ‖x - y‖
<VAR>p : ℕ<VAR>hp : 1 < p<GOAL>padicValNat p p = 1
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>neq_one : ¬p = 1 ↔ True<GOAL>padicValNat p p = 1
<VAR>p : ℕ<VAR>hp : 1 < p<VAR>neq_one : ¬p = 1 ↔ True<VAR>eq_zero_false : p = 0 ↔ False<GOAL>padicValNat p p = 1
<VAR>t : ↑I<GOAL>↑(qRight (t, 0)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
<VAR>t : ↑I<GOAL>↑(Set.projIcc 0 1 qRight.proof_1 (2 * ↑t)) = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<GOAL>I.ringCon x y ↔ x - y ∈ I
<VAR>R : Type u_1<VAR>inst✝ : NonUnitalNonAssocRing R<VAR>I : TwoSidedIdeal R<VAR>x y : R<GOAL>I.ringCon x y ↔ I.ringCon (x - y) 0
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>α : Type u_3<VAR>inst✝² : Group G<VAR>inst✝¹ : Group H<VAR>inst✝ : MulAction G α<VAR>a : G<VAR>s : Finset α<GOAL>a ∈ stabilizer G ↑s ↔ ↑s ⊆ a • ↑s
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>p✝ : R[X]<VAR>inst✝ : Semiring S<VAR>p : S[X]<VAR>f : S →+* R<GOAL>Continuous fun x => eval₂ f x p
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝³ : Semiring R<VAR>inst✝² : TopologicalSpace R<VAR>inst✝¹ : TopologicalSemiring R<VAR>p✝ : R[X]<VAR>inst✝ : Semiring S<VAR>p : S[X]<VAR>f : S →+* R<GOAL>Continuous fun x => p.sum fun e a => f a * x ^ e
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hg : S.g = 0<GOAL>𝟙 S.X₂ ≫ S.g = 0
<VAR>C : Type u_1<VAR>inst✝¹ : Category.{u_2, u_1} C<VAR>inst✝ : HasZeroMorphisms C<VAR>S S₁ S₂ S₃ : ShortComplex C<VAR>h : S.LeftHomologyData<VAR>A : C<VAR>hg : S.g = 0<GOAL>h.i ≫ h.liftK (𝟙 S.X₂) ⋯ = 𝟙 h.K
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>c : ℝ≥0<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<GOAL>Summable f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>c : ℝ≥0<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<VAR>H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop<GOAL>False
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>f : ℕ → ℝ≥0<VAR>c : ℝ≥0<VAR>h : ∀ (n : ℕ), ∑ i ∈ Finset.range n, f i ≤ c<VAR>H : Tendsto (fun n => ∑ i ∈ Finset.range n, f i) atTop atTop<VAR>n : ℕ<VAR>hn : c < ∑ i ∈ Finset.range n, f i<GOAL>False
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>a.cof.ord ≤ o
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>a o : Ordinal.{u}<VAR>f : (b : Ordinal.{u}) → b < o → Ordinal.{u}<VAR>hf : a.IsFundamentalSequence o f<GOAL>(o.blsub f).cof.ord ≤ o
<VAR>α : Type u_1<VAR>a b c d : α<VAR>inst✝³ : Mul α<VAR>inst✝² : IsSymmOp α α fun x x_1 => x * x_1<VAR>inst✝¹ : Zero α<VAR>inst✝ : Preorder α<GOAL>PosMulReflectLE α ↔ MulPosReflectLE α
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>f : R[M]<GOAL>f ∈ adjoin R (of' R M '' ↑f.support)
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>f : R[M]<GOAL>span R (of' R M '' ↑f.support) ≤ Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support))
<VAR>R : Type u_1<VAR>M : Type u_2<VAR>inst✝¹ : CommSemiring R<VAR>inst✝ : AddMonoid M<VAR>f : R[M]<GOAL>of' R M '' ↑f.support ⊆ ↑(Subalgebra.toSubmodule (adjoin R (of' R M '' ↑f.support)))
<VAR>k : Type u_1<VAR>inst✝⁷ : Field k<VAR>K : Type u_2<VAR>inst✝⁶ : Field K<VAR>F : Type u_3<VAR>inst✝⁵ : Field F<VAR>inst✝⁴ : NumberField K<VAR>inst✝³ : Algebra k K<VAR>inst✝² : Algebra k F<VAR>inst✝¹ : Algebra K F<VAR>inst✝ : IsScalarTower k K F<VAR>σ : K ≃ₐ[k] K<VAR>w : InfinitePlace K<VAR>φ : K →+* ℂ<VAR>h : ComplexEmbedding.IsConj φ σ<VAR>x✝ : K ≃ₐ[k] K<GOAL>x✝ ∈ ↑(Stab (mk φ)) ↔ x✝ ∈ {1, σ}
<VAR>R : Type u_1<VAR>R₁ : Type u_2<VAR>R₂ : Type u_3<VAR>R₃ : Type u_4<VAR>M : Type u_5<VAR>M₁ : Type u_6<VAR>M₂ : Type u_7<VAR>M₃ : Type u_8<VAR>Mₗ₁ : Type u_9<VAR>Mₗ₁' : Type u_10<VAR>Mₗ₂ : Type u_11<VAR>Mₗ₂' : Type u_12<VAR>K : Type u_13<VAR>K₁ : Type u_14<VAR>K₂ : Type u_15<VAR>V : Type u_16<VAR>V₁ : Type u_17<VAR>V₂ : Type u_18<VAR>n : Type u_19<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : AddCommMonoid M<VAR>inst✝⁶ : Module R M<VAR>inst✝⁵ : CommSemiring R₁<VAR>inst✝⁴ : AddCommMonoid M₁<VAR>inst✝³ : Module R₁ M₁<VAR>inst✝² : CommSemiring R₂<VAR>inst✝¹ : AddCommMonoid M₂<VAR>inst✝ : Module R₂ M₂<VAR>I₁ : R₁ →+* R<VAR>I₂ : R₂ →+* R<VAR>I₁' : R₁ →+* R<VAR>B : M₁ →ₛₗ[I₁] M₂ →ₛₗ[I₂] M<GOAL>B.flip.SeparatingLeft ↔ B.SeparatingRight
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝¹ : TopologicalSpace X<VAR>inst✝ : TopologicalSpace Y<VAR>x y✝ z : X<VAR>ι : Type u_3<VAR>F : Set X<VAR>y : X<GOAL>JoinedIn {y} y y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<GOAL>IsLeast {t | s ⊆ ↑t} (Convex.toCone ((convexHull 𝕜) s) ⋯)
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<GOAL>{t | s ⊆ ↑t} = {t | (convexHull 𝕜) s ⊆ ↑t}
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>inst✝² : LinearOrderedField 𝕜<VAR>inst✝¹ : AddCommGroup E<VAR>inst✝ : Module 𝕜 E<VAR>s : Set E<VAR>t : ConvexCone 𝕜 E<GOAL>t ∈ {t | s ⊆ ↑t} ↔ t ∈ {t | (convexHull 𝕜) s ⊆ ↑t}
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<GOAL>0 < dValue N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<VAR>hN₀ : 0 < ↑N<GOAL>0 < dValue N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<VAR>hN₀ : 0 < ↑N<GOAL>log 2 * ↑(nValue N) ≤ log ↑N
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<VAR>hN₀ : 0 < ↑N<GOAL>0 < ↑(nValue N)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<VAR>hN₀ : 0 < ↑N<GOAL>↑N ^ (↑(nValue N))⁻¹ ≠ 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>n d k N : ℕ<VAR>x : Fin n → ℕ<VAR>hN₃ : 8 ≤ N<VAR>hN₀ : 0 < ↑N<GOAL>0 < ↑N ^ (↑(nValue N))⁻¹ / 2
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → α ⊕ β<VAR>b b' : β<VAR>h : f b = Sum.inr b'<GOAL>tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩ = ⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → α ⊕ β<VAR>b b' : β<VAR>h : f b = Sum.inr b'<GOAL>↑(tail ⟨Stream'.corec' (Corec.f f) (Sum.inr b), ⋯⟩) = ↑⟨Stream'.corec' (Corec.f f) (Sum.inr b'), ⋯⟩
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → α ⊕ β<VAR>b b' : β<VAR>h : f b = Sum.inr b'<GOAL>(Stream'.corec' (Corec.f f) (Sum.inr b)).tail = Stream'.corec' (Corec.f f) (Sum.inr b')
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>f : β → α ⊕ β<VAR>b b' : β<VAR>h : f b = Sum.inr b'<GOAL>Stream'.corec' (Corec.f f) (Corec.f f (Sum.inr b)).2 = Stream'.corec' (Corec.f f) (Sum.inr b')
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>hJI : J ⊆ I<GOAL>M.closure J ∩ I = J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>hJI : J ⊆ I<VAR>hJ : M.Indep J<GOAL>M.closure J ∩ I = J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>hJI : J ⊆ I<VAR>hJ : M.Indep J<GOAL>M.closure J ∩ I ⊆ J
<VAR>ι✝ : Type u_1<VAR>α : Type u_2<VAR>M : Matroid α<VAR>F X Y : Set α<VAR>e✝ : α<VAR>ι : Sort u_3<VAR>I J B : Set α<VAR>f x y : α<VAR>hI : M.Indep I<VAR>hJI : J ⊆ I<VAR>hJ : M.Indep J<VAR>e : α<VAR>heJ : e ∈ M.closure J<VAR>heI : e ∈ I<GOAL>e ∈ J
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ico a₁ b₁ ∩ Ico a₂ b₂ = Ico (a₁ ⊔ a₂) (b₁ ⊓ b₂)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LinearOrder β<VAR>f : α → β<VAR>a a₁ a₂ b b₁ b₂ c d : α<GOAL>Ici a₁ ∩ Iio b₁ ∩ (Ici a₂ ∩ Iio b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iio b₁ ∩ Iio b₂)
<VAR>α : Type u<VAR>l✝ l' l : List α<VAR>h : l' ∈ l.cyclicPermutations<GOAL>l'.length = l.length
<VAR>α : Type u<VAR>l✝ l : List α<VAR>k : Fin l.cyclicPermutations.length<VAR>h : l.cyclicPermutations.get k ∈ l.cyclicPermutations<GOAL>(l.cyclicPermutations.get k).length = l.length
<VAR>n : ℕ<GOAL>1 ∈ n.properDivisors ↔ 1 < n
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : NormalSpace X<VAR>inst✝³ : ParacompactSpace X<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>t : X → Set E<VAR>ht : ∀ (x : X), Convex ℝ (t x)<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>g : X → X → E<VAR>hgc : ∀ (x : X), ContinuousOn (g x) (U x)<VAR>hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y<GOAL>∃ g, ∀ (x : X), g x ∈ t x
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>E : Type u_3<VAR>inst✝⁷ : TopologicalSpace X<VAR>inst✝⁶ : AddCommGroup E<VAR>inst✝⁵ : Module ℝ E<VAR>inst✝⁴ : NormalSpace X<VAR>inst✝³ : ParacompactSpace X<VAR>inst✝² : TopologicalSpace E<VAR>inst✝¹ : ContinuousAdd E<VAR>inst✝ : ContinuousSMul ℝ E<VAR>t : X → Set E<VAR>ht : ∀ (x : X), Convex ℝ (t x)<VAR>U : X → Set X<VAR>hU : ∀ (x : X), U x ∈ 𝓝 x<VAR>g : X → X → E<VAR>hgc : ∀ (x : X), ContinuousOn (g x) (U x)<VAR>hgt : ∀ (x y : X), y ∈ U x → g x y ∈ t y<VAR>f : PartitionOfUnity X X<VAR>hf : f.IsSubordinate fun x => interior (U x)<GOAL>∃ g, ∀ (x : X), g x ∈ t x