bump to nightly-2023-06-23-07

mathlib commit leanprover-community/mathlib@d30d312
leanprover-community · Jun 23, 2023 · 70450a3 · 70450a3
1 parent 3548bec
commit 70450a3
Show file tree

Hide file tree

Showing 6 changed files with 136 additions and 6 deletions.
diff --git a/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean b/Mathbin/AlgebraicGeometry/PresheafedSpace/Gluing.lean
@@ -75,6 +75,7 @@ variable (C : Type u) [Category.{v} C]
 
 namespace PresheafedSpace
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData /-
 /-- A family of gluing data consists of
 1. An index type `J`
 2. A presheafed space `U i` for each `i : J`.
@@ -97,6 +98,7 @@ that the `U i`'s are open subspaces of the glued space.
 structure GlueData extends GlueData (PresheafedSpace.{v} C) where
   f_open : ∀ i j, IsOpenImmersion (f i j)
 #align algebraic_geometry.PresheafedSpace.glue_data AlgebraicGeometry.PresheafedSpace.GlueData
+-/
 
 attribute [instance] glue_data.f_open
 
@@ -116,12 +118,15 @@ local notation "π₁⁻¹ " i ", " j ", " k =>
 local notation "π₂⁻¹ " i ", " j ", " k =>
   (PresheafedSpace.IsOpenImmersion.pullbackSndOfLeft (D.f i j) (D.f i k)).invApp
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData /-
 /-- The glue data of topological spaces associated to a family of glue data of PresheafedSpaces. -/
 abbrev toTopGlueData : TopCat.GlueData :=
   { f_open := fun i j => (D.f_open i j).base_open
     toGlueData := 𝖣.mapGlueData (forget C) }
 #align algebraic_geometry.PresheafedSpace.glue_data.to_Top_glue_data AlgebraicGeometry.PresheafedSpace.GlueData.toTopGlueData
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding /-
 theorem ι_openEmbedding [HasLimits C] (i : D.J) : OpenEmbedding (𝖣.ι i).base :=
   by
   rw [← show _ = (𝖣.ι i).base from 𝖣.ι_gluedIso_inv (PresheafedSpace.forget _) _]
@@ -130,7 +135,9 @@ theorem ι_openEmbedding [HasLimits C] (i : D.J) : OpenEmbedding (𝖣.ι i).bas
       (TopCat.homeoOfIso (𝖣.gluedIso (PresheafedSpace.forget _)).symm).OpenEmbedding
       (D.to_Top_glue_data.ι_open_embedding i)
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_open_embedding AlgebraicGeometry.PresheafedSpace.GlueData.ι_openEmbedding
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base /-
 theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) :
     (π₂ i, j, k) '' ((π₁ i, j, k) ⁻¹' S) = D.f i k ⁻¹' (D.f i j '' S) :=
   by
@@ -142,7 +149,9 @@ theorem pullback_base (i j k : D.J) (S : Set (D.V (i, j)).carrier) :
   rw [← TopCat.epi_iff_surjective]
   infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.pullback_base AlgebraicGeometry.PresheafedSpace.GlueData.pullback_base
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app /-
 /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/0GiBUh6.png) commute. -/
 @[simp, reassoc]
 theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
@@ -169,7 +178,9 @@ theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
   erw [(D.V (i, k)).Presheaf.map_id]
   rfl
 #align algebraic_geometry.PresheafedSpace.glue_data.f_inv_app_f_app AlgebraicGeometry.PresheafedSpace.GlueData.f_invApp_f_app
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app' /-
 /-- We can prove the `eq` along with the lemma. Thus this is bundled together here, and the
 lemma itself is separated below.
 -/
@@ -199,7 +210,9 @@ theorem snd_invApp_t_app' (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)
   congr 2
   rw [is_iso.inv_comp_eq, 𝖣.t_fac_assoc, 𝖣.t_inv, category.comp_id]
 #align algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app' AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app'
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app /-
 /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/q6X1GJ9.png) commute. -/
 @[simp, reassoc]
 theorem snd_invApp_t_app (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k)).carrier) :
@@ -213,9 +226,11 @@ theorem snd_invApp_t_app (i j k : D.J) (U : Opens (pullback (D.f i j) (D.f i k))
   rw [← e]
   simp [eq_to_hom_map]
 #align algebraic_geometry.PresheafedSpace.glue_data.snd_inv_app_t_app AlgebraicGeometry.PresheafedSpace.GlueData.snd_invApp_t_app
+-/
 
 variable [HasLimits C]
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq /-
 theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
     (Opens.map (𝖣.ι j).base).obj ((D.ι_openEmbedding i).IsOpenMap.Functor.obj U) =
       (D.f_open j i).openFunctor.obj
@@ -240,7 +255,9 @@ theorem ι_image_preimage_eq (i j : D.J) (U : Opens (D.U i).carrier) :
   · rw [← TopCat.mono_iff_injective]
     infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_image_preimage_eq AlgebraicGeometry.PresheafedSpace.GlueData.ι_image_preimage_eq
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap /-
 /-- (Implementation). The map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_{U_j}, 𝖣.ι j ⁻¹' (𝖣.ι i '' U))` -/
 def opensImagePreimageMap (i j : D.J) (U : Opens (D.U i).carrier) :
     (D.U i).Presheaf.obj (op U) ⟶ (D.U j).Presheaf.obj _ :=
@@ -249,7 +266,9 @@ def opensImagePreimageMap (i j : D.J) (U : Opens (D.U i).carrier) :
       (D.f_open j i).invApp (unop _) ≫
         (𝖣.U j).Presheaf.map (eqToHom (D.ι_image_preimage_eq i j U)).op
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' /-
 theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) :
     ∃ eq,
       D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ =
@@ -268,7 +287,9 @@ theorem opensImagePreimageMap_app' (i j k : D.J) (U : Opens (D.U i).carrier) :
   rw [eq_to_hom_map (opens.map _), eq_to_hom_op, eq_to_hom_trans]
   congr
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app' AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app'
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app /-
 /-- The red and the blue arrows in ![this diagram](https://i.imgur.com/mBzV1Rx.png) commute. -/
 theorem opensImagePreimageMap_app (i j k : D.J) (U : Opens (D.U i).carrier) :
     D.opensImagePreimageMap i j U ≫ (D.f j k).c.app _ =
@@ -277,7 +298,9 @@ theorem opensImagePreimageMap_app (i j k : D.J) (U : Opens (D.U i).carrier) :
           (D.V (j, k)).Presheaf.map (eqToHom (opensImagePreimageMap_app' D i j k U).some) :=
   (opensImagePreimageMap_app' D i j k U).choose_spec
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc /-
 -- This is proved separately since `reassoc` somehow timeouts.
 theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier) {X' : C}
     (f' : _ ⟶ X') :
@@ -289,19 +312,25 @@ theorem opensImagePreimageMap_app_assoc (i j k : D.J) (U : Opens (D.U i).carrier
   simpa only [category.assoc] using
     congr_arg (fun g => g ≫ f') (opens_image_preimage_map_app D i j k U)
 #align algebraic_geometry.PresheafedSpace.glue_data.opens_image_preimage_map_app_assoc AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app_assoc
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen /-
 /-- (Implementation) Given an open subset of one of the spaces `U ⊆ Uᵢ`, the sheaf component of
 the image `ι '' U` in the glued space is the limit of this diagram. -/
 abbrev diagramOverOpen {i : D.J} (U : Opens (D.U i).carrier) : (WalkingMultispan _ _)ᵒᵖ ⥤ C :=
   componentwiseDiagram 𝖣.diagram.multispan ((D.ι_openEmbedding i).IsOpenMap.Functor.obj U)
 #align algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpen
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ /-
 /-- (Implementation)
 The projection from the limit of `diagram_over_open` to a component of `D.U j`. -/
 abbrev diagramOverOpenπ {i : D.J} (U : Opens (D.U i).carrier) (j : D.J) :=
   limit.π (D.diagramOverOpen U) (op (WalkingMultispan.right j))
 #align algebraic_geometry.PresheafedSpace.glue_data.diagram_over_open_π AlgebraicGeometry.PresheafedSpace.GlueData.diagramOverOpenπ
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp /-
 /-- (Implementation) We construct the map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_V, U_V)` for each `V` in the gluing
 diagram. We will lift these maps into `ι_inv_app`. -/
 def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
@@ -319,7 +348,9 @@ def ιInvAppπApp {i : D.J} (U : Opens (D.U i).carrier) (j) :
     exact colimit.w 𝖣.diagram.multispan (walking_multispan.hom.fst (j, k))
   · exact D.opens_image_preimage_map i j U
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπApp
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp /-
 /-- (Implementation) The natural map `Γ(𝒪_{U_i}, U) ⟶ Γ(𝒪_X, 𝖣.ι i '' U)`.
 This forms the inverse of `(𝖣.ι i).c.app (op U)`. -/
 def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) :
@@ -373,7 +404,9 @@ def ιInvApp {i : D.J} (U : Opens (D.U i).carrier) :
             repeat' erw [← (D.V (j, k)).Presheaf.map_comp]
             congr } }
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π /-
 /-- `ι_inv_app` is the left inverse of `D.ι i` on `U`. -/
 theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) :
     ∃ eq, D.ιInvApp U ≫ D.diagramOverOpenπ U i = (D.U i).Presheaf.map (eqToHom Eq) :=
@@ -391,12 +424,16 @@ theorem ιInvApp_π {i : D.J} (U : Opens (D.U i).carrier) :
   · rw [← TopCat.epi_iff_surjective]
     infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π AlgebraicGeometry.PresheafedSpace.GlueData.ιInvApp_π
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap /-
 /-- The `eq_to_hom` given by `ι_inv_app_π`. -/
 abbrev ιInvAppπEqMap {i : D.J} (U : Opens (D.U i).carrier) :=
   (D.U i).Presheaf.map (eqToIso (D.ιInvApp_π U).some).inv
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_inv_app_π_eq_map AlgebraicGeometry.PresheafedSpace.GlueData.ιInvAppπEqMap
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π /-
 /-- `ι_inv_app` is the right inverse of `D.ι i` on `U`. -/
 theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
     D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U ≫ D.diagramOverOpenπ U j =
@@ -430,7 +467,9 @@ theorem π_ιInvApp_π (i j : D.J) (U : Opens (D.U i).carrier) :
     erw [D.ι_image_preimage_eq i j U]
     all_goals infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_π AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_π
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id /-
 /-- `ι_inv_app` is the inverse of `D.ι i` on `U`. -/
 theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) :
     D.diagramOverOpenπ U i ≫ D.ιInvAppπEqMap U ≫ D.ιInvApp U = 𝟙 _ :=
@@ -449,7 +488,11 @@ theorem π_ιInvApp_eq_id (i : D.J) (U : Opens (D.U i).carrier) :
     rw [category.id_comp]
     apply π_ι_inv_app_π
 #align algebraic_geometry.PresheafedSpace.glue_data.π_ι_inv_app_eq_id AlgebraicGeometry.PresheafedSpace.GlueData.π_ιInvApp_eq_id
+-/
 
+/- warning: algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso clashes with algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_IsIso -> AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso
+Case conversion may be inaccurate. Consider using '#align algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIsoₓ'. -/
+#print AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso /-
 instance componentwise_diagram_π_isIso (i : D.J) (U : Opens (D.U i).carrier) :
     IsIso (D.diagramOverOpenπ U i) :=
   by
@@ -459,13 +502,19 @@ instance componentwise_diagram_π_isIso (i : D.J) (U : Opens (D.U i).carrier) :
   · rw [category.assoc, (D.ι_inv_app_π _).choose_spec]
     exact iso.inv_hom_id ((D.to_glue_data.U i).Presheaf.mapIso (eq_to_iso _))
 #align algebraic_geometry.PresheafedSpace.glue_data.componentwise_diagram_π_is_iso AlgebraicGeometry.PresheafedSpace.GlueData.componentwise_diagram_π_isIso
+-/
 
+/- warning: algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.PresheafedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion
+Case conversion may be inaccurate. Consider using '#align algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersionₓ'. -/
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion /-
 instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i)
     where
   base_open := D.ι_openEmbedding i
   c_iso U := by erw [← colimit_presheaf_obj_iso_componentwise_limit_hom_π]; infer_instance
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.PresheafedSpace.GlueData.ιIsOpenImmersion
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit /-
 /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
 
 Vᵢⱼ ⟶ Uᵢ
@@ -497,10 +546,13 @@ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
       erw [is_open_immersion.lift_fac_assoc]
     · intro m e₁ e₂; rw [← cancel_mono (D.f i j)]; erw [e₁]; rw [is_open_immersion.lift_fac]
 #align algebraic_geometry.PresheafedSpace.glue_data.V_pullback_cone_is_limit AlgebraicGeometry.PresheafedSpace.GlueData.vPullbackConeIsLimit
+-/
 
+#print AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective /-
 theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x :=
   𝖣.ι_jointly_surjective (PresheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x
 #align algebraic_geometry.PresheafedSpace.glue_data.ι_jointly_surjective AlgebraicGeometry.PresheafedSpace.GlueData.ι_jointly_surjective
+-/
 
 end GlueData
 
@@ -560,9 +612,13 @@ theorem ι_isoPresheafedSpace_inv (i : D.J) :
   𝖣.ι_gluedIso_inv _ _
 #align algebraic_geometry.SheafedSpace.glue_data.ι_iso_PresheafedSpace_inv AlgebraicGeometry.SheafedSpaceₓ.GlueData.ι_isoPresheafedSpace_inv
 
+/- warning: algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.SheafedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion
+Case conversion may be inaccurate. Consider using '#align algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersionₓ'. -/
+#print AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion /-
 instance ιIsOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) := by
   rw [← D.ι_iso_PresheafedSpace_inv]; infer_instance
 #align algebraic_geometry.SheafedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.SheafedSpaceₓ.GlueData.ιIsOpenImmersion
+-/
 
 theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).base y = x :=
   𝖣.ι_jointly_surjective (SheafedSpace.forget _ ⋙ CategoryTheory.forget TopCat) x
@@ -586,6 +642,7 @@ end SheafedSpace
 
 namespace LocallyRingedSpace
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData /-
 /-- A family of gluing data consists of
 1. An index type `J`
 2. A locally ringed space `U i` for each `i : J`.
@@ -608,6 +665,7 @@ that the `U i`'s are open subspaces of the glued space.
 structure GlueData extends GlueData LocallyRingedSpace where
   f_open : ∀ i j, LocallyRingedSpace.IsOpenImmersion (f i j)
 #align algebraic_geometry.LocallyRingedSpace.glue_data AlgebraicGeometry.LocallyRingedSpace.GlueData
+-/
 
 attribute [instance] glue_data.f_open
 
@@ -617,36 +675,49 @@ variable (D : GlueData)
 
 local notation "𝖣" => D.toGlueData
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData /-
 /-- The glue data of ringed spaces associated to a family of glue data of locally ringed spaces. -/
 abbrev toSheafedSpaceGlueData : SheafedSpace.GlueData CommRingCat :=
   { f_open := D.f_open
     toGlueData := 𝖣.mapGlueData forgetToSheafedSpace }
 #align algebraic_geometry.LocallyRingedSpace.glue_data.to_SheafedSpace_glue_data AlgebraicGeometry.LocallyRingedSpace.GlueData.toSheafedSpaceGlueData
+-/
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace /-
 /-- The gluing as locally ringed spaces is isomorphic to the gluing as ringed spaces. -/
 abbrev isoSheafedSpace : 𝖣.glued.toSheafedSpace ≅ D.toSheafedSpaceGlueData.toGlueData.glued :=
   𝖣.gluedIso forgetToSheafedSpace
 #align algebraic_geometry.LocallyRingedSpace.glue_data.iso_SheafedSpace AlgebraicGeometry.LocallyRingedSpace.GlueData.isoSheafedSpace
+-/
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv /-
 theorem ι_isoSheafedSpace_inv (i : D.J) :
     D.toSheafedSpaceGlueData.toGlueData.ι i ≫ D.isoSheafedSpace.inv = (𝖣.ι i).1 :=
   𝖣.ι_gluedIso_inv forgetToSheafedSpace i
 #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_iso_SheafedSpace_inv AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isoSheafedSpace_inv
+-/
 
+/- warning: algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion clashes with algebraic_geometry.LocallyRingedSpace.glue_data.ι_IsOpenImmersion -> AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion
+Case conversion may be inaccurate. Consider using '#align algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersionₓ'. -/
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion /-
 instance ι_isOpenImmersion (i : D.J) : IsOpenImmersion (𝖣.ι i) :=
   by
   delta is_open_immersion; rw [← D.ι_iso_SheafedSpace_inv]
   apply PresheafedSpace.is_open_immersion.comp
 #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_is_open_immersion AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_isOpenImmersion
+-/
 
 instance (i j k : D.J) : PreservesLimit (cospan (𝖣.f i j) (𝖣.f i k)) forgetToSheafedSpace :=
   inferInstance
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective /-
 theorem ι_jointly_surjective (x : 𝖣.glued) : ∃ (i : D.J) (y : D.U i), (𝖣.ι i).1.base y = x :=
   𝖣.ι_jointly_surjective
     ((LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forget _) ⋙ forget TopCat) x
 #align algebraic_geometry.LocallyRingedSpace.glue_data.ι_jointly_surjective AlgebraicGeometry.LocallyRingedSpace.GlueData.ι_jointly_surjective
+-/
 
+#print AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit /-
 /-- The following diagram is a pullback, i.e. `Vᵢⱼ` is the intersection of `Uᵢ` and `Uⱼ` in `X`.
 
 Vᵢⱼ ⟶ Uᵢ
@@ -658,6 +729,7 @@ def vPullbackConeIsLimit (i j : D.J) : IsLimit (𝖣.vPullbackCone i j) :=
   𝖣.vPullbackConeIsLimitOfMap forgetToSheafedSpace i j
     (D.toSheafedSpaceGlueData.vPullbackConeIsLimit _ _)
 #align algebraic_geometry.LocallyRingedSpace.glue_data.V_pullback_cone_is_limit AlgebraicGeometry.LocallyRingedSpace.GlueData.vPullbackConeIsLimit
+-/
 
 end GlueData