ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝² : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝¹ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<GOAL>Nonempty (IsColimit c')
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝³ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝² : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝¹ : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this✝ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<VAR>this : cf.hom ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫ pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt = 𝟙 ((Cocones.precompose β.hom).obj c').pt<GOAL>Nonempty (IsColimit c')
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝⁴ : PreservesLimitsOfSize.{?u.164955, ?u.164954, u_3, v, u_2, u} Gr<VAR>this✝³ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<VAR>this✝ : cf.hom ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫ pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt = 𝟙 ((Cocones.precompose β.hom).obj c').pt<VAR>this : IsIso cf<GOAL>Nonempty (IsColimit c')
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝⁴ : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr<VAR>this✝³ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<VAR>this✝ : cf.hom ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫ pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt = 𝟙 ((Cocones.precompose β.hom).obj c').pt<VAR>this : IsIso cf<VAR>Hc'' : IsColimit c''<GOAL>Nonempty (IsColimit c')
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝⁴ : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr<VAR>this✝³ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<VAR>this✝ : cf.hom ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫ pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt = 𝟙 ((Cocones.precompose β.hom).obj c').pt<VAR>this : IsIso cf<GOAL>whiskerRight α' Gr ≫ c.ι = c''.ι ≫ (Functor.const J).map (pullback.snd (Gr.map f) (adj.unit.app c.pt))
<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.162150, u_1} K<VAR>D : Type u_2<VAR>inst✝⁴ : Category.{u_3, u_2} D<VAR>Gl : C ⥤ D<VAR>Gr : D ⥤ C<VAR>adj : Gl ⊣ Gr<VAR>inst✝³ : Gr.Full<VAR>inst✝² : Gr.Faithful<VAR>F : J ⥤ D<VAR>c : Cocone (F ⋙ Gr)<VAR>H : IsUniversalColimit c<VAR>inst✝¹ : ∀ (X : D) (f : X ⟶ Gl.obj c.pt), HasPullback (Gr.map f) (adj.unit.app c.pt)<VAR>inst✝ : (X : D) → (f : X ⟶ Gl.obj c.pt) → PreservesLimit (cospan (Gr.map f) (adj.unit.app c.pt)) Gl<VAR>this✝⁴ : PreservesLimitsOfSize.{0, 0, u_3, v, u_2, u} Gr<VAR>this✝³ : PreservesColimitsOfSize.{u', v', v, u_3, u, u_2} Gl<VAR>F' : J ⥤ D<VAR>c' : Cocone F'<VAR>α : F' ⟶ (F ⋙ Gr) ⋙ Gl<VAR>f : c'.pt ⟶ (Gl.mapCocone c).pt<VAR>h : α ≫ (Gl.mapCocone c).ι = c'.ι ≫ (Functor.const J).map f<VAR>hα : NatTrans.Equifibered α<VAR>hc' : ∀ (j : J), IsPullback (c'.ι.app j) (α.app j) f ((Gl.mapCocone c).ι.app j)<VAR>this✝² : HasPullback (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt))<VAR>α' : F' ⟶ F := α ≫ (F.associator Gr Gl).hom ≫ whiskerLeft F adj.counit ≫ F.rightUnitor.hom<VAR>hα' : NatTrans.Equifibered α'<VAR>hadj : ∀ (X : C), Gl.map (adj.unit.app X) = inv (adj.counit.app (Gl.toPrefunctor.1 ((𝟭 C).obj X)))<VAR>this✝¹ : ∀ (X : C), IsIso (Gl.map (adj.unit.app X))<VAR>hα'' : ∀ (j : J), Gl.map (Gr.map (α'.app j)) = adj.counit.app (F'.toPrefunctor.1 j) ≫ α.app j<VAR>hc'' : ∀ (j : J), α.app j ≫ Gl.map (c.ι.app j) = c'.ι.app j ≫ f<VAR>β : F' ⋙ Gr ⋙ Gl ≅ F' := isoWhiskerLeft F' (asIso adj.counit) ≪≫ F'.rightUnitor<VAR>c'' : Cocone (F' ⋙ Gr) := { pt := pullback (Gr.map f) (adj.unit.app c.pt), ι := { app := fun j => pullback.lift (Gr.map (c'.ι.app j)) (Gr.map (α'.app j) ≫ c.ι.app j) ⋯, naturality := ⋯ } }<VAR>cf : (Cocones.precompose β.hom).obj c' ⟶ Gl.mapCocone c'' := { hom := pullback.lift (inv (adj.counit.app c'.pt)) f ⋯ ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).inv, w := ⋯ }<VAR>this✝ : cf.hom ≫ (PreservesPullback.iso Gl (Gr.map f) (adj.unit.app c.pt)).hom ≫ pullback.fst (Gl.map (Gr.map f)) (Gl.map (adj.unit.app c.pt)) ≫ adj.counit.app c'.pt = 𝟙 ((Cocones.precompose β.hom).obj c').pt<VAR>this : IsIso cf<GOAL>∀ (j : J), IsPullback (c''.ι.app j) ((whiskerRight α' Gr).app j) (pullback.snd (Gr.map f) (adj.unit.app c.pt)) (c.ι.app j)
<VAR>n : ℕ<GOAL>11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
<VAR>n : ℕ<VAR>t : 11 ∣ n ↔ ↑11 ∣ ofDigits (-1) (digits 10 n)<GOAL>11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
<VAR>n : ℕ<VAR>t : 11 ∣ n ↔ ↑11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum<GOAL>11 ∣ n ↔ 11 ∣ (List.map (fun n => ↑n) (digits 10 n)).alternatingSum
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Proj.restrict ⋯).toPresheafedSpace<GOAL>FromSpec.toFun f_deg hm ((toSpec 𝒜 f) x) = x
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Proj.restrict ⋯).toPresheafedSpace<GOAL>∀ (i : ℕ), ∀ x_1 ∈ 𝒜 i, x_1 ∈ (↑(FromSpec.toFun f_deg hm ((toSpec 𝒜 f) x))).asHomogeneousIdeal ↔ x_1 ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Proj.restrict ⋯).toPresheafedSpace<VAR>i : ℕ<VAR>z : A<VAR>hzi : z ∈ 𝒜 i<GOAL>z ∈ (↑(FromSpec.toFun f_deg hm ((toSpec 𝒜 f) x))).asHomogeneousIdeal ↔ z ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>A : Type u_2<VAR>inst✝³ : CommRing R<VAR>inst✝² : CommRing A<VAR>inst✝¹ : Algebra R A<VAR>𝒜 : ℕ → Submodule R A<VAR>inst✝ : GradedAlgebra 𝒜<VAR>f : A<VAR>m : ℕ<VAR>f_deg : f ∈ 𝒜 m<VAR>hm : 0 < m<VAR>x : ↑↑(Proj.restrict ⋯).toPresheafedSpace<VAR>i : ℕ<VAR>z : A<VAR>hzi : z ∈ 𝒜 i<GOAL>HomogeneousLocalization.mk { deg := m * i, num := ⟨z ^ m, ⋯⟩, den := ⟨f ^ i, ⋯⟩, den_mem := ⋯ } ∈ ((toSpec 𝒜 f) x).asIdeal ↔ z ∈ (↑x).asHomogeneousIdeal
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : DecidableEq R<GOAL>∑ a : R, 1 a = ↑(Fintype.card Rˣ)
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : DecidableEq R<VAR>a : R<VAR>x✝ : a ∈ Finset.univ<GOAL>1 a = if IsUnit a then 1 else 0
<VAR>R : Type u_1<VAR>inst✝³ : CommMonoid R<VAR>inst✝² : Fintype R<VAR>R' : Type u_2<VAR>inst✝¹ : CommRing R'<VAR>inst✝ : DecidableEq R<GOAL>↑(Finset.filter IsUnit Finset.univ).card = ↑(Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ).card
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x<GOAL>Icc a b ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x<GOAL>∀ x ∈ s ∩ Ico a b, ∀ y ∈ Ioi x, (s ∩ Ioc x y).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxab : x ∈ Ico a b<VAR>y : α<VAR>hyxb : y ∈ Ioi x<GOAL>(s ∩ Ioc x y).Nonempty
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a✝ b✝ a b : α<VAR>s : Set α<VAR>hs : IsClosed (s ∩ Icc a b)<VAR>ha : a ∈ s<VAR>hgt : ∀ x ∈ s ∩ Ico a b, s ∈ 𝓝[>] x<VAR>x : α<VAR>hxs : x ∈ s<VAR>hxab : x ∈ Ico a b<VAR>y : α<VAR>hyxb : y ∈ Ioi x<VAR>this : s ∩ Ioc x y ∈ 𝓝[>] x<GOAL>(s ∩ Ioc x y).Nonempty
<VAR>ι : Sort u_1<VAR>f g : ι → ℝ≥0∞<VAR>a b c d : ℝ≥0∞<VAR>r p q : ℝ≥0<VAR>s : Set ℝ≥0∞<GOAL>sInf s + a = ⨅ b ∈ s, b + a
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>0 ⧏ x ↔ ∃ i, 0 ≤ x.moveLeft i
<VAR>xl xr : Type u<VAR>x : PGame<GOAL>((∃ i, 0 ≤ x.moveLeft i) ∨ ∃ j, moveRight 0 j ≤ x) ↔ ∃ i, 0 ≤ x.moveLeft i
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq G<VAR>ha0 : a0 ∈ A<VAR>hb0 : b0 ∈ B<GOAL>UniqueMul A B a0 b0 ↔ (filter (fun p => p.1 * p.2 = a0 * b0) (A ×ˢ B)).card ≤ 1
<VAR>G : Type u_1<VAR>H : Type u_2<VAR>inst✝² : Mul G<VAR>inst✝¹ : Mul H<VAR>A B : Finset G<VAR>a0 b0 : G<VAR>inst✝ : DecidableEq G<VAR>ha0 : a0 ∈ A<VAR>hb0 : b0 ∈ B<GOAL>UniqueMul A B a0 b0 ↔ ∀ {a b : G × G}, (a.1 ∈ A ∧ a.2 ∈ B) ∧ a.1 * a.2 = a0 * b0 → (b.1 ∈ A ∧ b.2 ∈ B) ∧ b.1 * b.2 = a0 * b0 → a = b
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<GOAL>adjoin S ↑(adjoin R s) = adjoin S s
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<GOAL>adjoin S s ≤ adjoin S ↑(adjoin R s)
<VAR>R : Type uR<VAR>S : Type uS<VAR>A : Type uA<VAR>B : Type uB<VAR>inst✝⁸ : CommSemiring R<VAR>inst✝⁷ : CommSemiring S<VAR>inst✝⁶ : Semiring A<VAR>inst✝⁵ : Semiring B<VAR>inst✝⁴ : Algebra R S<VAR>inst✝³ : Algebra R A<VAR>inst✝² : Algebra S A<VAR>inst✝¹ : Algebra R B<VAR>inst✝ : IsScalarTower R S A<VAR>s✝ t s : Set A<GOAL>↑(adjoin R s) ⊆ ↑(adjoin S s)
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G.neighborSet v)<VAR>inst✝ : DecidableEq V<GOAL>Fintype.card ↑(G.incidenceSet v) = G.degree v
<VAR>V : Type u_1<VAR>G : SimpleGraph V<VAR>e : Sym2 V<VAR>v : V<VAR>inst✝¹ : Fintype ↑(G.neighborSet v)<VAR>inst✝ : DecidableEq V<GOAL>Fintype.card ↑(G.neighborSet v) = G.degree v
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<GOAL>∃ φ, ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<VAR>c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) := { pt := F.obj (op Y), π := { app := fun x_1 => match x_1 with | op { obj := Z, property := hZ } => F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op ((𝟭 C).obj Z.left)))))), naturality := ⋯ } }<GOAL>∃ φ, ∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), φ ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<VAR>c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) := { pt := F.obj (op Y), π := { app := fun x_1 => match x_1 with | op { obj := Z, property := hZ } => F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op ((𝟭 C).obj Z.left)))))), naturality := ⋯ } }<GOAL>∀ {Z : C} (p : Z ⟶ Y) (hp : S.arrows (p ≫ g)), (hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
<VAR>C : Type u<VAR>inst✝¹ : Category.{v, u} C<VAR>J : GrothendieckTopology C<VAR>A : Type u'<VAR>inst✝ : Category.{v', u'} A<VAR>F G : Cᵒᵖ ⥤ A<VAR>X : C<VAR>S : Sieve X<VAR>hG : ⦃Y : C⦄ → (f : Y ⟶ X) → IsLimit (G.mapCone (Sieve.pullback f S).arrows.cocone.op)<VAR>x : Presieve.FamilyOfElements (presheafHom F G) S.arrows<VAR>hx : x.Compatible<VAR>Y : C<VAR>g : Y ⟶ X<VAR>c : Cone ((Sieve.pullback g S).arrows.diagram.op ⋙ G) := { pt := F.obj (op Y), π := { app := fun x_1 => match x_1 with | op { obj := Z, property := hZ } => F.map Z.hom.op ≫ (x (Z.hom ≫ g) hZ).app (op (Over.mk (𝟙 (unop (op ((𝟭 C).obj Z.left)))))), naturality := ⋯ } }<VAR>Z : C<VAR>p : Z ⟶ Y<VAR>hp : S.arrows (p ≫ g)<GOAL>(hG g).lift c ≫ G.map p.op = F.map p.op ≫ (x (p ≫ g) hp).app (op (Over.mk (𝟙 Z)))
<VAR>α : Type u_1<VAR>x : ℂ<VAR>h : x ∈ slitPlane<GOAL>ContinuousAt log x
<VAR>α : Type u_1<VAR>x : ℂ<VAR>h : x ∈ slitPlane<GOAL>ContinuousAt (fun x => ↑(Real.log (Complex.abs x))) x
<VAR>α : Type u_1<VAR>x : ℂ<VAR>h : x ∈ slitPlane<GOAL>ContinuousAt (fun x => ↑x.arg * I) x
<GOAL>Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)
<VAR>h : Tendsto (fun x => log x * x ^ 1) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<GOAL>Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<GOAL>Tendsto (fun x => log x * x) (𝓝[<] 0) (𝓝 0)
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<GOAL>Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 0)
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<GOAL>Tendsto (-(fun x => log x * x) ∘ fun x => |x|) (𝓝[<] 0) (𝓝 (-0))
<VAR>h : Tendsto (fun x => log x * x) (𝓝[>] 0) (𝓝 0)<VAR>h_eq : ∀ x ∈ Set.Iio 0, (-(fun x => log x * x) ∘ fun x => |x|) x = log x * x<GOAL>𝓝[<] 0 ≤ 𝓝[≠] 0