ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>C : Type u<VAR>inst✝⁴ : Category.{v, u} C<VAR>I : C<VAR>F : Cᵒᵖ ⥤ Type w<VAR>hF : IsSheafFor F (ofArrows Empty.elim fun a => instIsEmptyEmpty.elim a)<VAR>hI : IsInitial I<VAR>α : Type<VAR>X : α → C<VAR>c : Cofan X<VAR>hc : IsColimit c<VAR>inst✝³ : (ofArrows X c.inj).hasPullbacks<VAR>inst✝² : HasInitial C<VAR>inst✝¹ : ∀ (i : α), Mono (c.inj i)<VAR>hd : Pairwise fun i j => IsPullback (initial.to (X i)) (initial.to (X j)) (c.inj i) (c.inj j)<VAR>inst✝ : PreservesLimit (Discrete.functor fun x => op (X x)) F<VAR>this : HasCoproduct X<VAR>hi : ∀ (b : ∏ᶜ fun b => F.obj (op (X b))), ∃! a, (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b<VAR>b : Equalizer.Presieve.Arrows.FirstObj F X<VAR>a✝ : Equalizer.Presieve.Arrows.firstMap F X c.inj b = Equalizer.Presieve.Arrows.secondMap F X c.inj b<VAR>t : F.obj (∏ᶜ fun x => op (X x))<VAR>ht₁ : (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) t = b<VAR>ht₂ : ∀ (y : F.obj (∏ᶜ fun x => op (X x))), (fun a => (F.map (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ Equalizer.Presieve.Arrows.forkMap F X c.inj) a = b) y → y = t<VAR>y : F.obj (op c.pt)<VAR>hy : (fun x => Equalizer.Presieve.Arrows.forkMap F X c.inj x = b) y<GOAL>𝟙 (∏ᶜ fun x => op (X x)) = (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).inv ≫ (opCoproductIsoProduct' hc (productIsProduct fun x => op (X x))).hom
<VAR>F : Type u_1<VAR>R : Type u<VAR>A : Type v<VAR>B : Type w<VAR>inst✝¹⁰ : CommSemiring R<VAR>inst✝⁹ : NonUnitalNonAssocSemiring A<VAR>inst✝⁸ : Module R A<VAR>inst✝⁷ : IsScalarTower R A A<VAR>inst✝⁶ : SMulCommClass R A A<VAR>inst✝⁵ : NonUnitalNonAssocSemiring B<VAR>inst✝⁴ : Module R B<VAR>inst✝³ : IsScalarTower R B B<VAR>inst✝² : SMulCommClass R B B<VAR>inst✝¹ : FunLike F A B<VAR>inst✝ : NonUnitalAlgHomClass F R A B<VAR>S : Set (NonUnitalSubalgebra R A)<VAR>x : A<GOAL>x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p
<VAR>p : ℕ<VAR>R : Type u_1<VAR>S : Type u_2<VAR>T : Type u_3<VAR>hp : Fact (Nat.Prime p)<VAR>inst✝² : CommRing R<VAR>inst✝¹ : CommRing S<VAR>inst✝ : CommRing T<VAR>α : Type u_4<VAR>β : Type u_5<VAR>x✝ y : 𝕎 R<VAR>m : ℤ<VAR>x : 𝕎 R<GOAL>WittVector.ghostFun (m • x) = m • WittVector.ghostFun x
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v, u₁} C<VAR>inst✝⁷ : Preadditive C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v, u₂} D<VAR>inst✝⁵ : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>inst✝³ : HasCokernels C<VAR>inst✝² : HasKernels C<VAR>inst✝¹ : PreservesFiniteLimits G<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>(coimageIsoImage F G i adj f).hom = Abelian.coimageImageComparison f
<VAR>C : Type u₁<VAR>inst✝⁸ : Category.{v, u₁} C<VAR>inst✝⁷ : Preadditive C<VAR>D : Type u₂<VAR>inst✝⁶ : Category.{v, u₂} D<VAR>inst✝⁵ : Abelian D<VAR>F : C ⥤ D<VAR>G : D ⥤ C<VAR>inst✝⁴ : G.PreservesZeroMorphisms<VAR>i : F ⋙ G ≅ 𝟭 C<VAR>adj : G ⊣ F<VAR>inst✝³ : HasCokernels C<VAR>inst✝² : HasKernels C<VAR>inst✝¹ : PreservesFiniteLimits G<VAR>inst✝ : F.PreservesZeroMorphisms<VAR>X Y : C<VAR>f : X ⟶ Y<GOAL>((((((((𝟙 (Abelian.coimage f) ≫ cokernel.desc (kernel.ι f) (i.inv.app X ≫ cokernel.π (kernel.ι f ≫ i.inv.app X)) ⋯ ≫ cokernel.desc (kernel.ι f ≫ i.inv.app X) (cokernel.π (i.hom.app (kernel f) ≫ kernel.ι f ≫ i.inv.app X)) ⋯ ≫ (cokernelIsoOfEq ⋯).inv ≫ cokernelComparison (F.map (kernel.ι f)) G) ≫ G.map (cokernelIsoOfEq ⋯).hom) ≫ G.map (cokernel.desc (kernelComparison f F ≫ kernel.ι (F.map f)) (cokernel.π (kernel.ι (F.map f))) ⋯)) ≫ 𝟙 (G.obj (cokernel (kernel.ι (F.map f))))) ≫ G.map (Abelian.coimageImageComparison (F.map f))) ≫ 𝟙 (G.obj (Abelian.image (F.map f)))) ≫ (PreservesKernel.iso G (cokernel.π (F.map f))).hom) ≫ ((((((((kernelIsoOfEq ⋯).hom ≫ kernel.lift (cokernel.π (G.map (F.map f))) (kernel.ι (cokernel.π (G.map (F.map f)) ≫ cokernelComparison (F.map f) G)) ⋯) ≫ (kernelIsoOfEq ⋯).hom) ≫ kernel.lift (cokernel.π (i.hom.app X ≫ f ≫ i.inv.app Y)) (kernel.ι (cokernel.π (i.hom.app X ≫ f ≫ i.inv.app Y) ≫ (cokernelIsoOfEq ⋯).hom)) ⋯) ≫ (kernelIsoOfEq ⋯).hom) ≫ kernel.lift (cokernel.π (f ≫ i.inv.app Y)) (kernel.ι (cokernel.π (f ≫ i.inv.app Y) ≫ cokernel.desc (f ≫ i.inv.app Y) (cokernel.π (i.hom.app X ≫ f ≫ i.inv.app Y)) ⋯)) ⋯) ≫ (kernelIsoOfEq ⋯).hom) ≫ kernel.lift (cokernel.π f ≫ cokernel.desc f (i.inv.app Y ≫ cokernel.π (f ≫ i.inv.app Y)) ⋯) (kernel.ι (inv (i.inv.app Y) ≫ cokernel.π f ≫ cokernel.desc f (i.inv.app Y ≫ cokernel.π (f ≫ i.inv.app Y)) ⋯) ≫ inv (i.inv.app Y)) ⋯) ≫ kernel.lift (cokernel.π f) (kernel.ι (cokernel.π f ≫ cokernel.desc f (i.inv.app Y ≫ cokernel.π (f ≫ i.inv.app Y)) ⋯)) ⋯) ≫ 𝟙 (kernel (cokernel.π f)) = Abelian.coimageImageComparison f
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsCofiltered D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<GOAL>Nonempty C
<VAR>C : Type u₁<VAR>inst✝⁴ : Category.{v₁, u₁} C<VAR>D : Type u₂<VAR>inst✝³ : Category.{v₂, u₂} D<VAR>F : C ⥤ D<VAR>inst✝² : IsCofiltered D<VAR>inst✝¹ : F.Full<VAR>inst✝ : F.Faithful<VAR>h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)<VAR>this : Nonempty D<GOAL>Nonempty C
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet<GOAL>(cs.simple i * cs.simple i') ^ M.M i i' = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet<VAR>this : ↑((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1<GOAL>(cs.simple i * cs.simple i') ^ M.M i i' = 1
<VAR>B : Type u_1<VAR>B' : Type u_2<VAR>e : B ≃ B'<VAR>W : Type u_3<VAR>H : Type u_4<VAR>inst✝¹ : Group W<VAR>inst✝ : Group H<VAR>M : CoxeterMatrix B<VAR>cs : CoxeterSystem M W<VAR>i i' : B<VAR>this✝ : (FreeGroup.of i * FreeGroup.of i') ^ M.M i i' ∈ M.relationsSet<VAR>this : ↑((FreeGroup.of i * FreeGroup.of i') ^ M.M i i') = 1<GOAL>(cs.mulEquiv.symm (PresentedGroup.of i) * cs.mulEquiv.symm (PresentedGroup.of i')) ^ M.M i i' = 1
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>γ : Type u_3<VAR>ι : Sort u_4<VAR>ι' : Sort u_5<VAR>ι₂ : Sort u_6<VAR>κ : ι → Sort u_7<VAR>κ₁ : ι → Sort u_8<VAR>κ₂ : ι → Sort u_9<VAR>κ' : ι' → Sort u_10<VAR>f : α → β → γ<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ b ∈ t, (fun x => f x b) '' s = image2 f s t
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>x ≤ y ↔ (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧ ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j
<VAR>xl xr : Type u<VAR>x y : PGame<GOAL>((∀ (i : x.LeftMoves), x.moveLeft i ⧏ y) ∧ ∀ (j : y.RightMoves), x ⧏ y.moveRight j) ↔ (∀ (i : x.LeftMoves), (∃ i', x.moveLeft i ≤ y.moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ y) ∧ ∀ (j : y.RightMoves), (∃ i, x ≤ (y.moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ y.moveRight j
<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✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Fintype ι<GOAL>LinearIndependent R v ↔ ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 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✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Fintype ι<VAR>H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∀ i ∉ s, g i = 0<VAR>hs : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<GOAL>∑ i : ι, g i • v i = 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✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Fintype ι<VAR>H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∀ i ∉ s, g i = 0<VAR>hs : ∑ i ∈ s, g i • v i = 0<VAR>i : ι<GOAL>∑ i : ι, g i • v i = ∑ i ∈ s, g i • v i
<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✝⁷ : Semiring R<VAR>inst✝⁶ : AddCommMonoid M<VAR>inst✝⁵ : AddCommMonoid M'<VAR>inst✝⁴ : AddCommMonoid M''<VAR>inst✝³ : Module R M<VAR>inst✝² : Module R M'<VAR>inst✝¹ : Module R M''<VAR>a b : R<VAR>x y : M<VAR>inst✝ : Fintype ι<VAR>H : ∀ (g : ι → R), ∑ i : ι, g i • v i = 0 → ∀ (i : ι), g i = 0<VAR>s : Finset ι<VAR>g : ι → R<VAR>hg : ∀ i ∉ s, g i = 0<VAR>hs : ∑ i ∈ s, g i • v i = 0<VAR>i✝ i : ι<VAR>x✝ : i ∈ Finset.univ<VAR>hi : i ∉ s<GOAL>g i • v i = 0
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>r : R<VAR>hp : p ∈ lifts f<GOAL>C (f r) * p ∈ lifts f
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>p : S[X]<VAR>r : R<VAR>hp : ∃ x, (mapRingHom f) x = p<GOAL>∃ x, (mapRingHom f) x = C (f r) * p
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>r : R<VAR>p₁ : R[X]<GOAL>∃ x, (mapRingHom f) x = C (f r) * (mapRingHom f) p₁
<VAR>R : Type u<VAR>inst✝¹ : Semiring R<VAR>S : Type v<VAR>inst✝ : Semiring S<VAR>f : R →+* S<VAR>r : R<VAR>p₁ : R[X]<GOAL>(mapRingHom f) (C r * p₁) = C (f r) * (mapRingHom f) p₁
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H : IsNilpotent (e₁ - e₂)<VAR>H' : Commute e₁ e₂<GOAL>e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H : IsNilpotent (e₁ - e₂)<VAR>H' : Commute e₁ e₂<VAR>this : (e₁ - e₂) ^ 3 = e₁ - e₂<GOAL>e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H' : Commute e₁ e₂<VAR>this : (e₁ - e₂) ^ 3 = e₁ - e₂<VAR>n : ℕ<VAR>hn : (e₁ - e₂) ^ n = 0<GOAL>e₁ = e₂
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝² : Ring R<VAR>inst✝¹ : Ring S<VAR>f : R →+* S<VAR>I : Type u_3<VAR>e : I → R<VAR>he✝ : OrthogonalIdempotents e<VAR>inst✝ : Fintype I<VAR>he : CompleteOrthogonalIdempotents e<VAR>e₁ e₂ : R<VAR>he₁ : IsIdempotentElem e₁<VAR>he₂ : IsIdempotentElem e₂<VAR>H' : Commute e₁ e₂<VAR>this✝ : (e₁ - e₂) ^ 3 = e₁ - e₂<VAR>n : ℕ<VAR>hn : (e₁ - e₂) ^ n = 0<VAR>this : (e₁ - e₂) ^ (2 * n + 1) = e₁ - e₂<GOAL>e₁ = e₂
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : (o.kahler x) y = 0<GOAL>x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : (o.kahler x) y = 0<VAR>this : ‖x‖ * ‖y‖ = 0<GOAL>x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : (o.kahler x) y = 0<VAR>this : ‖x‖ * ‖y‖ = 0<VAR>h : ‖x‖ = 0<GOAL>x = 0 ∨ y = 0
<VAR>E : Type u_1<VAR>inst✝² : NormedAddCommGroup E<VAR>inst✝¹ : InnerProductSpace ℝ E<VAR>inst✝ : Fact (finrank ℝ E = 2)<VAR>o : Orientation ℝ E (Fin 2)<VAR>x y : E<VAR>hx : (o.kahler x) y = 0<VAR>this : ‖x‖ * ‖y‖ = 0<VAR>h : ‖y‖ = 0<GOAL>x = 0 ∨ y = 0
<VAR>α : Type u<VAR>β : Type u_1<VAR>γ : Type u_2<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>t : γ → γ → Prop<VAR>o : Ordinal.{u_3}<GOAL>1 ≤ o ↔ o ≠ 0
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>c : ℝ≥0∞<VAR>U : Set α<VAR>hU : q U<VAR>r : ℝ≥0∞<VAR>hr : r < (c • μ) U<GOAL>∃ K ⊆ U, p K ∧ r < (c • μ) K
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : Measure α<VAR>p q : Set α → Prop<VAR>U✝ : Set α<VAR>ε : ℝ≥0∞<VAR>H : μ.InnerRegularWRT p q<VAR>c : ℝ≥0∞<VAR>U : Set α<VAR>hU : q U<VAR>r : ℝ≥0∞<VAR>hr : r < c * ⨆ K, ⨆ (_ : K ⊆ U), ⨆ (_ : p K), μ K<GOAL>∃ K ⊆ U, p K ∧ r < (c • μ) K
<VAR>ι : Type u_1<VAR>X : Type u_2<VAR>Y : Type u_3<VAR>inst✝⁹ : EMetricSpace X<VAR>inst✝⁸ : EMetricSpace Y<VAR>inst✝⁷ : MeasurableSpace X<VAR>inst✝⁶ : BorelSpace X<VAR>inst✝⁵ : MeasurableSpace Y<VAR>inst✝⁴ : BorelSpace Y<VAR>𝕜 : Type u_4<VAR>E✝ : Type u_5<VAR>P : Type u_6<VAR>E : Type u_7<VAR>inst✝³ : NormedAddCommGroup E<VAR>inst✝² : NormedSpace ℝ E<VAR>inst✝¹ : MeasurableSpace E<VAR>inst✝ : BorelSpace E<VAR>x y : E<GOAL>μH[1] (segment ℝ x y) = edist x y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>x y : G<VAR>h : openSegment ℝ x y ⊆ s<GOAL>y - x ∈ tangentConeAt ℝ s x
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>x y : G<VAR>h : openSegment ℝ x y ⊆ s<GOAL>∀ᶠ (n : ℕ) in atTop, x + (1 / 2) ^ n • (y - x) ∈ s
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>x y : G<VAR>h : openSegment ℝ x y ⊆ s<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x + (1 / 2) ^ n • (y - x) ∈ openSegment ℝ x y
<VAR>𝕜 : Type u_1<VAR>inst✝⁶ : NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>G : Type u_4<VAR>inst✝¹ : NormedAddCommGroup G<VAR>inst✝ : NormedSpace ℝ G<VAR>x✝ y✝ : E<VAR>s✝ t : Set E<VAR>s : Set G<VAR>x y : G<VAR>h : openSegment ℝ x y ⊆ s<VAR>n : ℕ<VAR>hn : n ≠ 0<GOAL>x + (1 / 2) ^ n • (y - x) ∈ (fun θ => (1 - θ) • x + θ • y) '' Ioo 0 1
<VAR>R : Type u_1<VAR>inst✝¹³ : Ring R<VAR>R₂ : Type u_2<VAR>inst✝¹² : Ring R₂<VAR>R₃ : Type u_3<VAR>inst✝¹¹ : Ring R₃<VAR>M : Type u_4<VAR>inst✝¹⁰ : TopologicalSpace M<VAR>inst✝⁹ : AddCommGroup M<VAR>M₂ : Type u_5<VAR>inst✝⁸ : TopologicalSpace M₂<VAR>inst✝⁷ : AddCommGroup M₂<VAR>M₃ : Type u_6<VAR>inst✝⁶ : TopologicalSpace M₃<VAR>inst✝⁵ : AddCommGroup M₃<VAR>M₄ : Type u_7<VAR>inst✝⁴ : TopologicalSpace M₄<VAR>inst✝³ : AddCommGroup M₄<VAR>inst✝² : Module R M<VAR>inst✝¹ : Module R₂ M₂<VAR>inst✝ : Module R₃ M₃<VAR>σ₁₂ : R →+* R₂<VAR>σ₂₃ : R₂ →+* R₃<VAR>σ₁₃ : R →+* R₃<VAR>f : M →SL[σ₁₂] M₂<VAR>x y : M<GOAL>f (x - y) = f x - f y
<VAR>w x✝ y✝ z✝ : ℝ<VAR>x y : ℝ≥0<VAR>z : ℝ<VAR>hz : 0 < z<GOAL>x ≤ y ^ z⁻¹ ↔ x ^ z ≤ y
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<GOAL>⇑f '' minimals r x = minimals s (⇑f '' x)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>r✝ r₁ r₂ : α → α → Prop<VAR>s✝ t : Set α<VAR>a b x✝ : α<VAR>f✝ : α → β<VAR>r : α → α → Prop<VAR>s : β → β → Prop<VAR>f : r ↪r s<VAR>x : Set α<GOAL>∀ ⦃a a' : α⦄, a ∈ x → a' ∈ x → (r a a' ↔ s (f a) (f a'))
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>(map f) (W_ R n) = W_ S n
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>n : ℕ<GOAL>∑ x ∈ range (n + 1), (map f) ((monomial (single x (p ^ (n - x)))) (↑p ^ x)) = ∑ i ∈ range (n + 1), (monomial (single i (p ^ (n - i)))) (↑p ^ i)
<VAR>p : ℕ<VAR>R : Type u_1<VAR>inst✝² : CommRing R<VAR>inst✝¹ : DecidableEq R<VAR>S : Type u_2<VAR>inst✝ : CommRing S<VAR>f : R →+* S<VAR>n i : ℕ<VAR>x✝ : i ∈ range (n + 1)<GOAL>(map f) ((monomial (single i (p ^ (n - i)))) (↑p ^ i)) = (monomial (single i (p ^ (n - i)))) (↑p ^ i)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : SetLike S R<VAR>hSR : NonUnitalSubringClass S R<VAR>s : S<GOAL>(unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
<VAR>R : Type u_1<VAR>S : Type u_2<VAR>inst✝¹ : Ring R<VAR>inst✝ : SetLike S R<VAR>hSR : NonUnitalSubringClass S R<VAR>s : S<VAR>this : SMulMemClass S ℤ R<GOAL>(unitization s).range = subalgebraOfSubring (Subring.closure ↑s)
<VAR>R : Type u_1<VAR>inst✝ : Semiring R<VAR>f✝ f : R[X]<GOAL>f.eraseLead.support = f.support.erase f.natDegree
<VAR>n : ℕ+<GOAL>1 ∣ n
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<VAR>hpq : p • 1 + q • (mk W) Y = 0<GOAL>p = 0 ∧ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<VAR>hpq : p • 1 + q • (mk W) Y = 0<VAR>h : ∑ i : Fin 2, ![p, q] i • (CoordinateRing.basis W) i = 0 → ∀ (i : Fin 2), ![p, q] i = 0<GOAL>p = 0 ∧ q = 0
<VAR>R : Type u<VAR>S : Type v<VAR>inst✝¹ : CommRing R<VAR>inst✝ : CommRing S<VAR>W : Affine R<VAR>f : R →+* S<VAR>p q : R[X]<VAR>hpq : p • 1 + q • (mk W) Y = 0<VAR>h : ![p, q] 0 • 1 + ![p, q] (Fin.succ 0) • (mk W) Y = 0 → ∀ (i : Fin 2), ![p, q] i = 0<GOAL>p = 0 ∧ q = 0
<VAR>C : Type u₁<VAR>inst✝ : Category.{v₁, u₁} C<VAR>Z X Y P : C<VAR>f✝ : Z ⟶ X<VAR>g : Z ⟶ Y<VAR>inl : X ⟶ P<VAR>inr : Y ⟶ P<VAR>f : X ⟶ Z<GOAL>𝟙 X ≫ f = f ≫ 𝟙 Z
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>i : ι<GOAL>∀ {x : M}, x ∈ S i → x ∈ iSup S
<VAR>M : Type u_1<VAR>A : Type u_2<VAR>B : Type u_3<VAR>inst✝ : MulOneClass M<VAR>ι : Sort u_4<VAR>S : ι → Submonoid M<VAR>i : ι<GOAL>S i ≤ iSup S
<VAR>X : LocallyRingedSpace<VAR>r : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<GOAL>IsUnit t
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>he : t * (algebraMap ↑(Γ.obj (op X)) ↑S) ↑(r, s).2 = (algebraMap ↑(Γ.obj (op X)) ↑S) (r, s).1<GOAL>IsUnit t
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit t
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit (t * t')
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit ((algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r)
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>r ∈ p.asIdeal.primeCompl
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit ((X.presheaf.Γgerm x) r)
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit ((toStalk (↑(unop (op (Γ.obj (op X))))) (X.toΓSpecSheafedSpace.base x) ≫ PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) r)
<VAR>X : LocallyRingedSpace<VAR>r✝ : ↑(Γ.obj (op X))<VAR>x : ↑↑X.toPresheafedSpace<VAR>p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x<VAR>S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p<VAR>t : ↑S<VAR>ht : IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) t)<VAR>r : ↑(Γ.obj (op X))<VAR>s : ↥p.asIdeal.primeCompl<VAR>t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s<VAR>he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r<GOAL>IsUnit ((PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace x) (t * t'))