ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>m n a✝ b✝ c d a b : ℤ<VAR>hb : 0 < b<VAR>z : ℤ<VAR>hz1 : 0 ≤ z<VAR>hz2 : z < b<VAR>hz3 : z ≡ a [ZMOD b]<GOAL>↑z.natAbs < b ∧ ↑z.natAbs ≡ a [ZMOD b]
<VAR>R : Type u<VAR>a b : R<VAR>m n : ℕ<VAR>inst✝¹ : Semiring R<VAR>p✝ q : R[X]<VAR>S : Type u_1<VAR>inst✝ : AddCommMonoid S<VAR>p : R[X]<VAR>f g : ℕ → R → S<GOAL>p.sum (f + g) = p.sum f + p.sum g
<VAR>n b : ℕ<VAR>h : 1 < b<VAR>x y : ℕ<VAR>hxb : x < b<VAR>hxy : x ≠ 0 ∨ y ≠ 0<GOAL>b.digits (x + b * y) = x :: b.digits y
<VAR>n x y : ℕ<VAR>hxy : x ≠ 0 ∨ y ≠ 0<VAR>b : ℕ<VAR>h : 1 < b + 2<VAR>hxb : x < b + 2<GOAL>(b + 2).digits (x + (b + 2) * y) = x :: (b + 2).digits y
<VAR>n x b : ℕ<VAR>h : 1 < b + 2<VAR>hxb : x < b + 2<VAR>n✝ : ℕ<VAR>hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0<GOAL>(b + 2).digitsAux ⋯ (x + (b + 2) * (n✝ + 1)) = x :: (b + 2).digitsAux ⋯ (n✝ + 1)
<VAR>n x b : ℕ<VAR>h : 1 < b + 2<VAR>hxb : x < b + 2<VAR>n✝ : ℕ<VAR>hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0<GOAL>(x + (b + 2) * (n✝ + 1)) % (b + 2) :: (b + 2).digitsAux ⋯ ((x + (b + 2) * (n✝ + 1)) / (b + 2)) = x :: (b + 2).digitsAux ⋯ (n✝ + 1)
<VAR>n x b : ℕ<VAR>h : 1 < b + 2<VAR>hxb : x < b + 2<VAR>n✝ : ℕ<VAR>hxy : x ≠ 0 ∨ n✝ + 1 ≠ 0<GOAL>0 < x + (b + 2) * (n✝ + 1)
<VAR>ι : Type u_1<VAR>ι' : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>inst✝¹ : LinearOrderedField α<VAR>l : Filter β<VAR>f : β → α<VAR>r : α<VAR>inst✝ : l.NeBot<VAR>h : Tendsto f l atTop<GOAL>Tendsto (fun x => f x * r) l atBot ↔ r < 0
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>n : ℕ<VAR>a : R<VAR>m : ℕ<GOAL>(coeff R m) ((monomial R n) a) = (coeff R m) (mk fun m => if m = n then a else 0)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.28063, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f<GOAL>LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.28063, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f<VAR>z₄ : W.LeftFraction z₃.Y' z₃'.Y'<VAR>fac : (RightFraction.mk z₃.s ⋯ z₃'.s).f ≫ z₄.s = (RightFraction.mk z₃.s ⋯ z₃'.s).s ≫ z₄.f<GOAL>LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.28063, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y Z : C<VAR>z₁ : W.LeftFraction X Y<VAR>z₂ : W.LeftFraction Y Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f<VAR>z₄ : W.LeftFraction z₃.Y' z₃'.Y'<VAR>fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f<VAR>eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s<GOAL>LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.28063, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y✝ Z : C<VAR>z₁ : W.LeftFraction X Y✝<VAR>z₂ : W.LeftFraction Y✝ Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f<VAR>z₄ : W.LeftFraction z₃.Y' z₃'.Y'<VAR>fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f<VAR>eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s<VAR>Y : C<VAR>t : z₄.Y' ⟶ Y<VAR>ht : W t<VAR>fac' : (z₃.f ≫ z₄.f) ≫ t = (z₃'.f ≫ z₄.s) ≫ t<GOAL>LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝² : Category.{u_3, u_1} C<VAR>inst✝¹ : Category.{?u.28063, u_2} D<VAR>W : MorphismProperty C<VAR>inst✝ : W.HasLeftCalculusOfFractions<VAR>X Y✝ Z : C<VAR>z₁ : W.LeftFraction X Y✝<VAR>z₂ : W.LeftFraction Y✝ Z<VAR>z₃ z₃' : W.LeftFraction z₁.Y' z₂.Y'<VAR>h₃ : z₂.f ≫ z₃.s = z₁.s ≫ z₃.f<VAR>h₃' : z₂.f ≫ z₃'.s = z₁.s ≫ z₃'.f<VAR>z₄ : W.LeftFraction z₃.Y' z₃'.Y'<VAR>fac : z₃'.s ≫ z₄.s = z₃.s ≫ z₄.f<VAR>eq : z₁.s ≫ z₃.f ≫ z₄.f = z₁.s ≫ z₃'.f ≫ z₄.s<VAR>Y : C<VAR>t : z₄.Y' ⟶ Y<VAR>ht : W t<VAR>fac' : z₃.f ≫ z₄.f ≫ t = z₃'.f ≫ z₄.s ≫ t<GOAL>LeftFractionRel (z₁.comp₀ z₂ z₃) (z₁.comp₀ z₂ z₃')
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<GOAL>Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.6235) (N : Type ?u.6234) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<GOAL>Ioc a b * Ico c d ⊆ Ioo (a * c) (b * d)
<VAR>α : Type u_1<VAR>inst✝³ : Mul α<VAR>inst✝² : PartialOrder α<VAR>inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1<VAR>inst✝ : CovariantClass α α (Function.swap HMul.hMul) LT.lt<VAR>a b c d : α<VAR>this : ∀ (M : Type ?u.6235) (N : Type ?u.6234) (μ : M → N → N) [inst : PartialOrder N] [inst_1 : CovariantClass M N μ fun x x_1 => x < x_1], CovariantClass M N μ fun x x_1 => x ≤ x_1<VAR>y : α<VAR>hya : a < y<VAR>hyb : y ≤ b<VAR>z : α<VAR>hzc : c ≤ z<VAR>hzd : z < d<GOAL>(fun x x_1 => x * x_1) y z ∈ Ioo (a * c) (b * d)
<VAR>k : Type u<VAR>inst✝¹¹ : CommRing k<VAR>G : Type u<VAR>inst✝¹⁰ : Group G<VAR>V : Type v<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module k V<VAR>inst✝⁷ : Module (MonoidAlgebra k G) V<VAR>inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>inst✝⁵ : AddCommGroup W<VAR>inst✝⁴ : Module k W<VAR>inst✝³ : Module (MonoidAlgebra k G) W<VAR>inst✝² : IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<GOAL>(equivariantProjection G π) (i v) = v
<VAR>k : Type u<VAR>inst✝¹¹ : CommRing k<VAR>G : Type u<VAR>inst✝¹⁰ : Group G<VAR>V : Type v<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module k V<VAR>inst✝⁷ : Module (MonoidAlgebra k G) V<VAR>inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>inst✝⁵ : AddCommGroup W<VAR>inst✝⁴ : Module k W<VAR>inst✝³ : Module (MonoidAlgebra k G) W<VAR>inst✝² : IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<GOAL>⅟↑(Fintype.card G) • ∑ g : G, (π.conjugate g) (i v) = v
<VAR>k : Type u<VAR>inst✝¹¹ : CommRing k<VAR>G : Type u<VAR>inst✝¹⁰ : Group G<VAR>V : Type v<VAR>inst✝⁹ : AddCommGroup V<VAR>inst✝⁸ : Module k V<VAR>inst✝⁷ : Module (MonoidAlgebra k G) V<VAR>inst✝⁶ : IsScalarTower k (MonoidAlgebra k G) V<VAR>W : Type w<VAR>inst✝⁵ : AddCommGroup W<VAR>inst✝⁴ : Module k W<VAR>inst✝³ : Module (MonoidAlgebra k G) W<VAR>inst✝² : IsScalarTower k (MonoidAlgebra k G) W<VAR>π : W →ₗ[k] V<VAR>i : V →ₗ[MonoidAlgebra k G] W<VAR>h : ∀ (v : V), π (i v) = v<VAR>inst✝¹ : Fintype G<VAR>inst✝ : Invertible ↑(Fintype.card G)<VAR>v : V<GOAL>⅟↑(Fintype.card G) • ∑ x : G, v = v
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : o.oangle x y = ↑(π / 2)<GOAL>‖y‖ / (o.oangle (x - y) x).sin = ‖x - y‖
<VAR>V : Type u_1<VAR>inst✝¹ : NormedAddCommGroup V<VAR>inst✝ : InnerProductSpace ℝ V<VAR>hd2 : Fact (finrank ℝ V = 2)<VAR>o : Orientation ℝ V (Fin 2)<VAR>x y : V<VAR>h : (-o).oangle y x = ↑(π / 2)<GOAL>‖y‖ / ((-o).oangle x (x - y)).sin = ‖x - y‖
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x = t • y<GOAL>s = 0 ∧ t = 0
<VAR>ι : Type u'<VAR>ι' : Type u_1<VAR>R : Type u_2<VAR>K : Type u_3<VAR>M : Type u_4<VAR>M' : Type u_5<VAR>M'' : Type u_6<VAR>V : Type u<VAR>V' : Type u_7<VAR>v : ι → M<VAR>inst✝⁶ : Ring R<VAR>inst✝⁵ : AddCommGroup M<VAR>inst✝⁴ : AddCommGroup M'<VAR>inst✝³ : AddCommGroup M''<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R M'<VAR>inst✝ : Module R M''<VAR>a b : R<VAR>x✝ y✝ x y : M<VAR>h : LinearIndependent R ![x, y]<VAR>s t : R<VAR>h' : s • x = t • y<GOAL>s = 0 ∧ 0 = t
<VAR>R : Type u_1<VAR>inst✝⁴ : CommSemiring R<VAR>M : Submonoid R<VAR>S : Type u_2<VAR>inst✝³ : CommSemiring S<VAR>inst✝² : Algebra R S<VAR>P : Type u_3<VAR>inst✝¹ : CommSemiring P<VAR>inst✝ : IsLocalization M S<VAR>x : R<VAR>y : ↥M<GOAL>(algEquiv M S).symm (mk' S x y) = mk x y
<VAR>k : Type u_1<VAR>V1 : Type u_2<VAR>P1 : Type u_3<VAR>V2 : Type u_4<VAR>P2 : Type u_5<VAR>V3 : Type u_6<VAR>P3 : Type u_7<VAR>V4 : Type u_8<VAR>P4 : Type u_9<VAR>inst✝¹² : Ring k<VAR>inst✝¹¹ : AddCommGroup V1<VAR>inst✝¹⁰ : Module k V1<VAR>inst✝⁹ : AffineSpace V1 P1<VAR>inst✝⁸ : AddCommGroup V2<VAR>inst✝⁷ : Module k V2<VAR>inst✝⁶ : AffineSpace V2 P2<VAR>inst✝⁵ : AddCommGroup V3<VAR>inst✝⁴ : Module k V3<VAR>inst✝³ : AffineSpace V3 P3<VAR>inst✝² : AddCommGroup V4<VAR>inst✝¹ : Module k V4<VAR>inst✝ : AffineSpace V4 P4<VAR>p : P1<VAR>v : V1<VAR>c : k<GOAL>(lineMap p (v +ᵥ p)) c = c • v +ᵥ p
<VAR>P : MorphismProperty Scheme<VAR>inst✝¹ : IsLocalAtSource P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : X.OpenCover<VAR>H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)<GOAL>P f
<VAR>P : MorphismProperty Scheme<VAR>inst✝¹ : IsLocalAtSource P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : X.OpenCover<VAR>H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)<VAR>i : 𝒰.J<GOAL>P (((fun i => Scheme.Hom.opensRange (𝒰.map i)) i).ι ≫ f)
<VAR>P : MorphismProperty Scheme<VAR>inst✝¹ : IsLocalAtSource P<VAR>X Y U V : Scheme<VAR>f : X ⟶ Y<VAR>g : U ⟶ Y<VAR>inst✝ : IsOpenImmersion g<VAR>𝒰 : X.OpenCover<VAR>H : ∀ (i : 𝒰.J), P (𝒰.map i ≫ f)<VAR>i : 𝒰.J<GOAL>P (𝒰.map i ≫ f)
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h<GOAL>g = h
<VAR>C : Type u_1<VAR>inst✝⁵ : Category.{u_2, u_1} C<VAR>inst✝⁴ : Preadditive C<VAR>inst✝³ : MonoidalCategory C<VAR>inst✝² : MonoidalPreadditive C<VAR>inst✝¹ : HasFiniteBiproducts C<VAR>J : Type<VAR>inst✝ : Fintype J<VAR>f : J → C<VAR>X Y Z : C<VAR>g h : ((⨁ f) ⊗ X) ⊗ Y ⟶ Z<VAR>w : ∀ (j : J), biproduct.ι f j ▷ X ▷ Y ≫ g = biproduct.ι f j ▷ X ▷ Y ≫ h<GOAL>(α_ (⨁ f) X Y).inv ≫ g = (α_ (⨁ f) X Y).inv ≫ h
<VAR>R : Type u<VAR>inst✝ : CommSemiring R<VAR>x y z : R<GOAL>IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z
<VAR>xl xr : Type u<VAR>s : Set PGame<VAR>inst✝ : Small.{u, u + 1} ↑s<GOAL>BddAbove s
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).prod % n = (∏ i ∈ s, f i % n) % n
<VAR>ι : Type u_1<VAR>κ : Type u_2<VAR>α : Type u_3<VAR>β : Type u_4<VAR>γ : Type u_5<VAR>s✝ s₁ s₂ : Finset α<VAR>a : α<VAR>f✝ g : α → β<VAR>s : Finset α<VAR>n : ℕ<VAR>f : α → ℕ<GOAL>(Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).prod % n = (Multiset.map (fun i => f i % n) s.val).prod % n
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>Z : Type u_3<VAR>α : Type u_4<VAR>ι : Type u_5<VAR>π : ι → Type u_6<VAR>inst✝³ : TopologicalSpace X<VAR>inst✝² : TopologicalSpace Y<VAR>inst✝¹ : TopologicalSpace Z<VAR>inst✝ : (i : ι) → TopologicalSpace (π i)<VAR>x✝ y✝ z : X<VAR>s : Set X<VAR>f g : X → Y<VAR>t : Set (SeparationQuotient X)<VAR>x : X<VAR>y : Y<GOAL>Filter.map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>beq1 beq2 : α → α → Bool<VAR>h : ∀ (x y : α), (x == y) = (x == y)<GOAL>beq1 = beq2
<VAR>α : Type u_1<VAR>inst1 inst2 : BEq α<VAR>beq1 beq2 : α → α → Bool<VAR>h : ∀ (x y : α), (x == y) = (x == y)<VAR>x y : α<GOAL>beq1 x y = beq2 x y
<VAR>R : Type r<VAR>S : Type s<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : WeierstrassCurve R<VAR>n : ℤ<GOAL>(mk W) (W.φ n) = (mk W) (C (W.Φ n))
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>β : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : AddCommMonoid F<VAR>inst✝¹ : Module 𝕜 E<VAR>inst✝ : Module 𝕜 F<VAR>s : Set E<VAR>x✝ : E<VAR>hs : Convex 𝕜 s<VAR>f : E →ₗ[𝕜] F<VAR>x : E<VAR>hx : x ∈ s<VAR>y : E<VAR>hy : y ∈ s<VAR>a b : 𝕜<VAR>ha : 0 ≤ a<VAR>hb : 0 ≤ b<VAR>hab : a + b = 1<GOAL>a • f x + b • f y ∈ ⇑f '' s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>P✝ : Generators R S<VAR>T : Type ?u.37168<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>Q : Generators S T<VAR>P : Generators R S<VAR>s : T<GOAL>(aeval (Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val))) ((fun x => Finsupp.sum (Q.σ x) fun n r => (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>P✝ : Generators R S<VAR>T : Type ?u.37168<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>Q : Generators S T<VAR>P : Generators R S<VAR>s : T<VAR>this : ∀ (x : P.Ring), (aeval (⇑(algebraMap S T) ∘ P.val)) x = (algebraMap S T) ((aeval P.val) x)<GOAL>(aeval (Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val))) ((fun x => Finsupp.sum (Q.σ x) fun n r => (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) s) = s
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝⁶ : CommRing R<VAR>inst✝⁵ : CommRing S<VAR>inst✝⁴ : Algebra R S<VAR>P✝ : Generators R S<VAR>T : Type ?u.37168<VAR>inst✝³ : CommRing T<VAR>inst✝² : Algebra R T<VAR>inst✝¹ : Algebra S T<VAR>inst✝ : IsScalarTower R S T<VAR>Q : Generators S T<VAR>P : Generators R S<VAR>s : T<VAR>this : ∀ (x : P.Ring), (aeval (⇑(algebraMap S T) ∘ P.val)) x = (algebraMap S T) ((aeval P.val) x)<GOAL>(aeval (Sum.elim Q.val (⇑(algebraMap S T) ∘ P.val))) ((fun x => Finsupp.sum (Q.σ x) fun n r => (rename Sum.inr) (P.σ r) * (monomial (Finsupp.mapDomain Sum.inl n)) 1) s) = (aeval Q.val) (Finsupp.sum (Q.σ s) AddMonoidAlgebra.single)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>X✝ Y : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>J J₂ : GrothendieckTopology C<VAR>hJ : Subcanonical J<VAR>X : C<GOAL>Presheaf.IsSheaf J (CategoryTheory.yoneda.obj X)
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>P : Cᵒᵖ ⥤ Type v<VAR>X✝ Y : C<VAR>S : Sieve X✝<VAR>R : Presieve X✝<VAR>J J₂ : GrothendieckTopology C<VAR>hJ : Subcanonical J<VAR>X : C<GOAL>Presieve.IsSheaf J (CategoryTheory.yoneda.obj X)
<VAR>C : Type u_1<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_1} C<VAR>inst✝³ : Category.{?u.244988, u_2} D<VAR>inst✝² : Preadditive C<VAR>inst✝¹ : Preadditive D<VAR>F G : CochainComplex C ℤ<VAR>φ : F ⟶ G<VAR>inst✝ : HasHomotopyCofiber φ<VAR>K L : CochainComplex C ℤ<VAR>n m : ℤ<VAR>α : Cochain K F m<VAR>β : Cochain K G n<VAR>n' m' : ℤ<VAR>α' : Cochain F L m'<VAR>β' : Cochain G L n'<VAR>h : n + 1 = m<VAR>h' : m' + 1 = n'<VAR>p : ℤ<VAR>hp : n + n' = p<GOAL>(liftCochain φ α β h).comp (descCochain φ α' β' h') hp = α.comp α' ⋯ + β.comp β' ⋯
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, f x ∈ 𝓝[s] x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x<VAR>t : ℕ → Finset X<VAR>ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s<VAR>hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}<GOAL>∃ t ⊆ s, t.Countable ∧ s ⊆ ⋃ x ∈ t, f x
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x<VAR>t : ℕ → Finset X<VAR>ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s<VAR>hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}<VAR>x : X<VAR>hx : x ∈ s<GOAL>∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x<VAR>t : ℕ → Finset X<VAR>ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s<VAR>hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}<VAR>x : X<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : x ∈ compactCovering X n<GOAL>∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>ι : Type u_3<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : TopologicalSpace Y<VAR>s✝ t✝ : Set X<VAR>inst✝ : SigmaCompactSpace X<VAR>f : X → Set X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>hf : ∀ x ∈ s, {x_1 | x_1 ∈ s → x_1 ∈ f x} ∈ 𝓝 x<VAR>t : ℕ → Finset X<VAR>ht : ∀ (n : ℕ), ∀ x ∈ t n, x ∈ compactCovering X n ∩ s<VAR>hsub : ∀ (n : ℕ), compactCovering X n ∩ s ⊆ ⋃ x ∈ t n, {x_1 | x_1 ∈ s → x_1 ∈ f x}<VAR>x : X<VAR>hx : x ∈ s<VAR>n : ℕ<VAR>hn : x ∈ compactCovering X n<VAR>y : X<VAR>hyt : y ∈ t n<VAR>hyf : x ∈ s → x ∈ f y<GOAL>∃ i, ∃ (_ : i ∈ ⋃ n, ↑(t n)), x ∈ f i
<VAR>E : Type u_1<VAR>inst✝ : SeminormedCommGroup E<VAR>ε δ : ℝ<VAR>s t : Set E<VAR>x y : E<GOAL>closedBall x δ / {y} = closedBall (x / y) δ
<VAR>α : Type u_1<VAR>inst✝ : OrderedAddCommGroup α<VAR>a b c : α<GOAL>(fun x => a - x) ⁻¹' Ico b c = Ioc (a - c) (a - b)
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<GOAL>boundedBy ⊤ = ⊤
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<GOAL>∀ (s : Set α), s.Nonempty → ⊤ s ≤ ⊤ s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>⊤ s ≤ ⊤ s
<VAR>α : Type u_1<VAR>m : Set α → ℝ≥0∞<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>⊤ ≤ ⊤ s
<VAR>C : Type u<VAR>inst✝ : Category.{v, u} C<VAR>X : SimplicialObject C<VAR>n : ℕ<VAR>i : Fin (n + 1)<GOAL>X.map (SimplexCategory.σ i).op ≫ X.map (SimplexCategory.δ i.succ).op = 𝟙 (X _[n])
<VAR>n : ℤ<VAR>d : ℕ<GOAL>mkRat n d = ↑n / ↑d
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁴ : CommSemiring k<VAR>inst✝³ : Group G<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Module k V<VAR>ρ : Representation k G V<VAR>H : Type u_4<VAR>inst✝ : MulAction G H<VAR>g : G<VAR>f : H →₀ k<VAR>h : H<GOAL>(((ofMulAction k G H) g) f) h = f (g⁻¹ • h)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁴ : CommSemiring k<VAR>inst✝³ : Group G<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Module k V<VAR>ρ : Representation k G V<VAR>H : Type u_4<VAR>inst✝ : MulAction G H<VAR>g : G<VAR>f : H →₀ k<VAR>h : H<GOAL>(((ofMulAction k G H) g) f) (g • g⁻¹ • h) = f (g⁻¹ • h)
<VAR>k : Type u_1<VAR>G : Type u_2<VAR>V : Type u_3<VAR>inst✝⁴ : CommSemiring k<VAR>inst✝³ : Group G<VAR>inst✝² : AddCommMonoid V<VAR>inst✝¹ : Module k V<VAR>ρ : Representation k G V<VAR>H : Type u_4<VAR>inst✝ : MulAction G H<VAR>g : G<VAR>f : H →₀ k<VAR>h : H<VAR>h' : H := g⁻¹ • h<VAR>hg : Function.Injective fun x => g • x<GOAL>(((ofMulAction k G H) g) f) (g • h') = f h'
<VAR>x✝ y✝ x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>log y < log x
<VAR>x✝ y✝ x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>log |y| < log |x|
<VAR>x✝ y✝ x : ℝ<VAR>hx : x < 0<VAR>y : ℝ<VAR>hy : y < 0<VAR>hxy : x < y<GOAL>|y| < |x|
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c✝ u : αˣ<VAR>a c : α<VAR>h : a = ↑b⁻¹ * c<GOAL>↑b * a = c
<VAR>α : Type u<VAR>inst✝ : Monoid α<VAR>a✝ b c✝ u : αˣ<VAR>a c : α<VAR>h : ↑b * a = c<GOAL>a = ↑b⁻¹ * c
<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>ι : Type u_4<VAR>v : ι → E<VAR>hv : Orthonormal 𝕜 v<VAR>l : ι →₀ 𝕜<VAR>i : ι<GOAL>⟪(Finsupp.total ι E 𝕜 v) l, v i⟫_𝕜 = (starRingEnd 𝕜) (l i)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x y : FreeCommRing α<VAR>s✝ t : Set α<VAR>i✝ : ℤ<VAR>s : Set α<VAR>i : ℕ<VAR>hi : (↑↑i).IsSupported s<GOAL>(↑(↑i + 1)).IsSupported s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x y : FreeCommRing α<VAR>s✝ t : Set α<VAR>i✝ : ℤ<VAR>s : Set α<VAR>i : ℕ<VAR>hi : (↑↑i).IsSupported s<GOAL>(↑↑i + 1).IsSupported s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x y : FreeCommRing α<VAR>s✝ t : Set α<VAR>i✝ : ℤ<VAR>s : Set α<VAR>i : ℕ<VAR>hi : (↑(-↑i)).IsSupported s<GOAL>(↑(-↑i - 1)).IsSupported s
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>x y : FreeCommRing α<VAR>s✝ t : Set α<VAR>i✝ : ℤ<VAR>s : Set α<VAR>i : ℕ<VAR>hi : (↑(-↑i)).IsSupported s<GOAL>(↑(-↑i) - 1).IsSupported s
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>H : Type u_3<VAR>inst✝³ : _root_.RCLike 𝕜<VAR>inst✝² : NormedAddCommGroup H<VAR>inst✝¹ : NormedSpace 𝕜 H<VAR>inst✝ : Fintype ι<VAR>f : H → EuclideanSpace 𝕜 ι<VAR>f' : H →L[𝕜] EuclideanSpace 𝕜 ι<VAR>t : Set H<VAR>y : H<GOAL>(∀ (i : ι), DifferentiableOn 𝕜 (fun x => (⇑(EuclideanSpace.equiv ι 𝕜) ∘ f) x i) t) ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : ContinuousConstSMul M α<GOAL>(∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ) → IsMinimal M α
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : ContinuousConstSMul M α<VAR>H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ<VAR>x✝ : α<GOAL>IsClosed (closure (orbit M x✝))
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : ContinuousConstSMul M α<VAR>H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ<VAR>x✝ : α<GOAL>∀ (c : M), c • closure (orbit M x✝) ⊆ closure (orbit M x✝)
<VAR>M : Type u_1<VAR>G : Type u_2<VAR>α : Type u_3<VAR>inst✝⁵ : Monoid M<VAR>inst✝⁴ : Group G<VAR>inst✝³ : TopologicalSpace α<VAR>inst✝² : MulAction M α<VAR>inst✝¹ : MulAction G α<VAR>inst✝ : ContinuousConstSMul M α<VAR>H : ∀ (s : Set α), IsClosed s → (∀ (c : M), c • s ⊆ s) → s = ∅ ∨ s = univ<VAR>x✝ : α<GOAL>¬closure (orbit M x✝) = ∅