ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) (∑ x : ↑(Basis.ofVectorSpaceIndex K V), ((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x) ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∑ x : ↑(Basis.ofVectorSpaceIndex K V), (LinearMap.rTensor (Module.Dual K V) (contractLeft K V)) (((Basis.ofVectorSpace K V).dualBasis j ⊗ₜ[K] (Basis.ofVectorSpace K V) x) ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>∑ x : ↑(Basis.ofVectorSpaceIndex K V), ((Basis.ofVectorSpace K V).dualBasis j) ((Basis.ofVectorSpace K V) x) ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).dualBasis j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(∑ x : ↑(Basis.ofVectorSpaceIndex K V), if x = j then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord x else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j
<VAR>K : Type u<VAR>inst✝³ : Field K<VAR>V : Type v<VAR>inst✝² : AddCommGroup V<VAR>inst✝¹ : Module K V<VAR>inst✝ : FiniteDimensional K V<VAR>this : DecidableEq ↑(Basis.ofVectorSpaceIndex K V) := Classical.decEq ↑(Basis.ofVectorSpaceIndex K V)<VAR>j : ↑(Basis.ofVectorSpaceIndex K V)<GOAL>(if j ∈ Finset.univ then 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j else 0) = 1 ⊗ₜ[K] (Basis.ofVectorSpace K V).coord j
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, a.get i ∈ FP a
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)<VAR>hs : s.Nonempty<GOAL>∏ i ∈ s, a.get i ∈ FP (Stream'.drop (s.min' hs) a)
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)<VAR>hs : s.Nonempty<GOAL>(Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)<VAR>hs : s.Nonempty<VAR>h : s.erase (s.min' hs) = ∅<GOAL>(Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
<VAR>M : Type u_1<VAR>inst✝ : CommMonoid M<VAR>a : Stream' M<VAR>s : Finset ℕ<VAR>ih : ∀ t ⊂ s, ∀ (hs : t.Nonempty), ∏ i ∈ t, a.get i ∈ FP (Stream'.drop (t.min' hs) a)<VAR>hs : s.Nonempty<VAR>h : (s.erase (s.min' hs)).Nonempty<GOAL>(Stream'.drop (s.min' hs) a).head * ∏ x ∈ s.erase (s.min' hs), a.get x ∈ FP (Stream'.drop (s.min' hs) a)
<VAR>a x✝ z x : ℂ<GOAL>↑x⁻¹.arg = -↑x.arg
<VAR>𝓕 : Type u_1<VAR>𝕜 : Type u_2<VAR>α : Type u_3<VAR>ι : Type u_4<VAR>κ : Type u_5<VAR>E : Type u_6<VAR>F : Type u_7<VAR>G : Type u_8<VAR>inst✝¹ : SeminormedCommGroup E<VAR>inst✝ : SeminormedCommGroup F<VAR>a✝ a₁ a₂ b✝ b₁ b₂ : E<VAR>r✝ r₁ r₂ : ℝ<VAR>a b : E<VAR>r : ℝ<VAR>c : E<GOAL>c ∈ (fun x => b * x) ⁻¹' sphere a r ↔ c ∈ sphere (a / b) r
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<VAR>f : F[X]<VAR>h : Splits (algebraMap F E) f<GOAL>f.natSepDegree = (f.aroots E).toFinset.card
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (F.leftDerivedToHomotopyCategory.map f) ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (Q.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) = ((HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ) ⋙ HomotopyCategory.quotient D (ComplexShape.down ℕ)).map φ) ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) = (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n
<VAR>C : Type u<VAR>inst✝⁵ : Category.{v, u} C<VAR>D : Type u_1<VAR>inst✝⁴ : Category.{u_2, u_1} D<VAR>inst✝³ : Abelian C<VAR>inst✝² : HasProjectiveResolutions C<VAR>inst✝¹ : Abelian D<VAR>X Y : C<VAR>f : X ⟶ Y<VAR>P : ProjectiveResolution X<VAR>Q : ProjectiveResolution Y<VAR>φ : P.complex ⟶ Q.complex<VAR>comm : φ.f 0 ≫ Q.π.f 0 = P.π.f 0 ≫ f<VAR>F : C ⥤ D<VAR>inst✝ : F.Additive<VAR>n : ℕ<GOAL>(HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) = (HomotopyCategory.homologyFunctor D (ComplexShape.down ℕ) n).map (P.isoLeftDerivedToHomotopyCategoryObj F).hom ≫ (HomotopyCategory.homologyFunctorFactors D (ComplexShape.down ℕ) n).hom.app ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex) ≫ HomologicalComplex.homologyMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) n
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : 0 < r<GOAL>⟪x, r • x⟫_ℝ / (‖x‖ * ‖r • x‖) = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>inst✝⁴ : _root_.RCLike 𝕜<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : InnerProductSpace 𝕜 E<VAR>inst✝¹ : NormedAddCommGroup F<VAR>inst✝ : InnerProductSpace ℝ F<VAR>x : F<VAR>r : ℝ<VAR>hx : x ≠ 0<VAR>hr : 0 < r<GOAL>r * (‖x‖ * ‖x‖) ≠ 0
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x ε : ℝ<VAR>hx : 0 ≤ x<VAR>hε : 0 < ε<VAR>h : 0 < x<GOAL>log x ≤ x ^ ε / ε
<VAR>x✝ y z : ℝ<VAR>n : ℕ<VAR>x ε : ℝ<VAR>hx : 0 ≤ x<VAR>hε : 0 < ε<VAR>h : 0 < x<GOAL>ε * log x ≤ x ^ ε
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : M<VAR>r : R<GOAL>∃ a, (eval IM I M R x) a = r
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : M<VAR>y : (smoothSheaf IM I M R).presheaf.stalk x<GOAL>∃ a, (eval IM I M R x) a = smoothSheaf.eval IM I R x y
<VAR>𝕜 : Type u_1<VAR>inst✝²¹ : NontriviallyNormedField 𝕜<VAR>EM : Type u_2<VAR>inst✝²⁰ : NormedAddCommGroup EM<VAR>inst✝¹⁹ : NormedSpace 𝕜 EM<VAR>HM : Type u_3<VAR>inst✝¹⁸ : TopologicalSpace HM<VAR>IM : ModelWithCorners 𝕜 EM HM<VAR>E : Type u_4<VAR>inst✝¹⁷ : NormedAddCommGroup E<VAR>inst✝¹⁶ : NormedSpace 𝕜 E<VAR>H : Type u_5<VAR>inst✝¹⁵ : TopologicalSpace H<VAR>I : ModelWithCorners 𝕜 E H<VAR>H' : Type u_6<VAR>inst✝¹⁴ : TopologicalSpace H'<VAR>I' : ModelWithCorners 𝕜 E H'<VAR>M : Type u<VAR>inst✝¹³ : TopologicalSpace M<VAR>inst✝¹² : ChartedSpace HM M<VAR>N G A A' R : Type u<VAR>inst✝¹¹ : TopologicalSpace N<VAR>inst✝¹⁰ : ChartedSpace H N<VAR>inst✝⁹ : TopologicalSpace G<VAR>inst✝⁸ : ChartedSpace H G<VAR>inst✝⁷ : TopologicalSpace A<VAR>inst✝⁶ : ChartedSpace H A<VAR>inst✝⁵ : TopologicalSpace A'<VAR>inst✝⁴ : ChartedSpace H' A'<VAR>inst✝³ : TopologicalSpace R<VAR>inst✝² : ChartedSpace H R<VAR>inst✝¹ : CommRing R<VAR>inst✝ : SmoothRing I R<VAR>x : M<VAR>y : (smoothSheaf IM I M R).presheaf.stalk x<GOAL>(eval IM I M R x) ((forgetStalk IM I M R x).inv y) = smoothSheaf.eval IM I R x y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<GOAL>x = y
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>z : E := 2⁻¹ • x + 2⁻¹ • y<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>z : E := 2⁻¹ • x + 2⁻¹ • y<VAR>hz : z ∈ s<GOAL>False
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>α : Type u_4<VAR>β : Type u_5<VAR>ι : Type u_6<VAR>inst✝⁵ : LinearOrderedField 𝕜<VAR>inst✝⁴ : OrderedAddCommMonoid β<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : SMul 𝕜 E<VAR>inst✝¹ : Module 𝕜 β<VAR>inst✝ : OrderedSMul 𝕜 β<VAR>f : E → β<VAR>s : Set E<VAR>x y : E<VAR>hf : StrictConvexOn 𝕜 s f<VAR>hfx : IsMinOn f s x<VAR>hfy : IsMinOn f s y<VAR>hx : x ∈ s<VAR>hy : y ∈ s<VAR>hxy : ¬x = y<VAR>z : E := 2⁻¹ • x + 2⁻¹ • y<VAR>hz : z ∈ s<GOAL>f z < f z
<VAR>α : Type u_1<VAR>p : α → Bool<VAR>l : List α<VAR>n : ℕ<VAR>x : α<VAR>h : p x = true<GOAL>rdropWhile p (l ++ [x]) = rdropWhile p l
<VAR>R : Type u1<VAR>inst✝² : CommRing R<VAR>M : Type u2<VAR>inst✝¹ : AddCommGroup M<VAR>inst✝ : Module R M<VAR>Q : QuadraticForm R M<VAR>d d' : Module.Dual R M<GOAL>(contractLeft d) 1 = 0
<VAR>S : Type u_1<VAR>M : Type u_2<VAR>G : Type u_3<VAR>inst✝ : Group G<VAR>a✝ x✝ y a x : G<GOAL>a * x = a * x * a⁻¹ * a
<VAR>J : Type v'<VAR>inst✝⁴ : Category.{u', v'} J<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>K : Type u_1<VAR>inst✝² : Category.{?u.333125, u_1} K<VAR>D : Type u_2<VAR>inst✝¹ : Category.{?u.333132, u_2} D<VAR>inst✝ : HasInitial C<VAR>ι : Type u_3<VAR>F : Discrete ι ⥤ C<VAR>c : Cocone F<VAR>hc : IsVanKampenColimit c<VAR>i j : Discrete ι<VAR>hi : i ≠ j<GOAL>IsPullback (initial.to (F.obj i)) (initial.to (F.obj j)) (c.ι.app i) (c.ι.app j)
<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✝⁵ : AddCommMonoid M₁<VAR>inst✝⁴ : Module R M₁<VAR>inst✝³ : AddCommMonoid M₂<VAR>inst✝² : Module R M₂<VAR>inst✝¹ : AddCommMonoid M₃<VAR>inst✝ : Module R M₃<VAR>I : R →+* R<VAR>B F : M →ₗ[R] M →ₛₗ[I] M₃<VAR>B' : M₁ →ₗ[R] M₁ →ₛₗ[I] M₃<VAR>B'' : M₂ →ₗ[R] M₂ →ₛₗ[I] M₃<VAR>f f' : M →ₗ[R] M₁<VAR>g g' : M₁ →ₗ[R] M<VAR>x✝¹ : M<VAR>x✝ : M₁<GOAL>(B' (0 x✝¹)) x✝ = (B x✝¹) (0 x✝)
<VAR>a b : Ordinal.{u_1}<VAR>ha : a < 2<VAR>hb : b < 2<VAR>h₂ : succ 1 = 2<GOAL>a * b < 2
<VAR>a b : Ordinal.{u_1}<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>h₂ : succ 1 = 2<GOAL>a * b ≤ 1
<VAR>a b : Ordinal.{u_1}<VAR>ha : a ≤ 1<VAR>hb : b ≤ 1<VAR>h₂ : succ 1 = 2<GOAL>1 = 1 * 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>inst✝³ : MulOneClass α<VAR>inst✝² : LE α<VAR>inst✝¹ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>inst✝ : ContravariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1<VAR>a b : α<GOAL>a ≤ b * a ↔ 1 * a ≤ b * a
<VAR>α : Type u<VAR>β : Type u_1<VAR>w x✝ y✝ z : α<VAR>inst✝ : GeneralizedBooleanAlgebra α<VAR>x y : α<GOAL>x \ y ⊓ (x ⊓ y) = ⊥
<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 : Set G<VAR>A B C : Subgroup G<VAR>h : C ≤ A<VAR>x✝ : G<GOAL>x✝ ∈ ↑(A ⊓ B) * ↑C ↔ x✝ ∈ ↑A ∩ (↑B * ↑C)
<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 : Set G<VAR>A B C : Subgroup G<VAR>h : C ≤ A<VAR>x✝ : G<GOAL>(∃ x, (x ∈ ↑A ∧ x ∈ ↑B) ∧ ∃ y ∈ ↑C, x * y = x✝) ↔ x✝ ∈ ↑A ∧ ∃ x ∈ ↑B, ∃ y ∈ ↑C, x * y = x✝
<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 : Set G<VAR>A B C : Subgroup G<VAR>h : C ≤ A<VAR>y : G<VAR>hy : y ∈ ↑B<VAR>z : G<VAR>hz : z ∈ ↑C<VAR>hyz : y * z ∈ ↑A<GOAL>y * z * z⁻¹ ∈ A
<VAR>X : LocallyRingedSpace<GOAL>Continuous X.toΓSpecFun
<VAR>X : LocallyRingedSpace<GOAL>∀ s ∈ Set.range fun r => ↑(basicOpen r), IsOpen (X.toΓSpecFun ⁻¹' s)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>IsOpen (X.toΓSpecFun ⁻¹' (fun r => ↑(basicOpen r)) r)
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<GOAL>IsOpen (X.toRingedSpace.basicOpen r).carrier
<VAR>α : Type u<VAR>inst✝¹ : CommMonoid α<VAR>inst✝ : Subsingleton αˣ<GOAL>1 * 1 = 1
<VAR>C : Type u<VAR>inst✝³ : Category.{v, u} C<VAR>f✝ : Arrow C<VAR>inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x => f✝.right) fun x => f✝.hom<VAR>f g : Arrow C<VAR>inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x => f.right) fun x => f.hom<VAR>inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x => g.right) fun x => g.hom<VAR>F : f ⟶ g<VAR>n : SimplexCategory<VAR>i : Fin (n.len + 1)<GOAL>f.hom ≫ (fun i => F.right ≫ WidePushout.ι (fun x => g.hom) i) i = F.left ≫ WidePushout.head fun x => g.hom
<VAR>α : Type u_1<VAR>inst✝¹ : LinearOrder α<VAR>inst✝ : LocallyFiniteOrder α<VAR>a✝ b✝ c✝ d a b c : α<GOAL>Ico a b - Ico a c = Ico (max a c) b
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>x : idx × ℕ<VAR>hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<GOAL>x ∈ Finset.univ ×ˢ Finset.range (n + 1)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>x : idx × ℕ<VAR>hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<GOAL>x.2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>x : idx × ℕ<VAR>hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>k : ℕ<VAR>hk : k ∈ (xInTermsOfW p ℚ n).vars<VAR>hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<GOAL>x.2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n : ℕ<VAR>x : idx × ℕ<VAR>hx : x ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>k : ℕ<VAR>hk : k ∈ (xInTermsOfW p ℚ n).vars<VAR>hx' : x ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<VAR>i : idx<VAR>hx'' : x ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars<GOAL>x.2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n k : ℕ<VAR>hk : k ∈ (xInTermsOfW p ℚ n).vars<VAR>i : idx<VAR>j : ℕ<VAR>hj : j ∈ (W_ ℚ k).vars<VAR>hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<VAR>hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars<GOAL>(i, j).2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n k : ℕ<VAR>hk : k ∈ (xInTermsOfW p ℚ n).vars<VAR>i : idx<VAR>j : ℕ<VAR>hj : j < k + 1<VAR>hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<VAR>hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars<GOAL>(i, j).2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n k : ℕ<VAR>i : idx<VAR>j : ℕ<VAR>hj : j < k + 1<VAR>hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<VAR>hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars<VAR>hk : k ∈ Finset.range (n + 1)<GOAL>(i, j).2 < n + 1
<VAR>p : ℕ<VAR>R : Type u_1<VAR>idx : Type u_2<VAR>inst✝¹ : CommRing R<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝ : Fintype idx<VAR>Φ : MvPolynomial idx ℚ<VAR>n k : ℕ<VAR>i : idx<VAR>j : ℕ<VAR>hj : j < k + 1<VAR>hx : (i, j) ∈ ((bind₁ fun k => (bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ) (xInTermsOfW p ℚ n)).vars<VAR>hx' : (i, j) ∈ ((bind₁ fun i => (rename (Prod.mk i)) (W_ ℚ k)) Φ).vars<VAR>hx'' : (i, j) ∈ ((rename (Prod.mk i)) (W_ ℚ k)).vars<VAR>hk : k < n + 1<GOAL>(i, j).2 < n + 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<GOAL>s.erase a = s ↔ a ∉ s
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>κ : ι → Sort u_5<VAR>inst✝ : Preorder α<VAR>s : LowerSet α<VAR>t : Set α<VAR>a : α<GOAL>s.sdiff {a} = s ↔ a ∉ s
<VAR>α : Type u_1<VAR>m m0 : MeasurableSpace α<VAR>μ : Measure α<VAR>s : Set α<VAR>hm : m ≤ m0<VAR>hs : (μ.trim hm) s = 0<GOAL>(μ.trim hm) (toMeasurable (μ.trim hm) s) = 0
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<GOAL>o.bmex f ∉ o.brange f
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_4}<VAR>f : (a : Ordinal.{u_4}) → a < o → Ordinal.{max u_4 u_5}<GOAL>o.bmex f ∉ range (o.familyOfBFamily f)
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<GOAL>IsIntegral F (gen F α) ↔ IsIntegral F α
<VAR>F : Type u_1<VAR>inst✝² : Field F<VAR>E : Type u_2<VAR>inst✝¹ : Field E<VAR>inst✝ : Algebra F E<VAR>S : Set E<VAR>α : E<GOAL>IsIntegral F (gen F α) ↔ IsIntegral F ((algebraMap (↥F⟮α⟯) E) (gen F α))
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝³ : Finite ι<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>μ (fundamentalDomain b) ≠ 0
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝³ : Finite ι<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Countable ↥(span ℤ (Set.range ⇑b)).toAddSubgroup
<VAR>E : Type u_1<VAR>ι : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace ℝ E<VAR>b : Basis ι ℝ E<VAR>inst✝³ : Finite ι<VAR>inst✝² : MeasurableSpace E<VAR>inst✝¹ : BorelSpace E<VAR>μ : Measure E<VAR>inst✝ : μ.IsAddHaarMeasure<GOAL>Countable ↥(span ℤ (Set.range ⇑b))