mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Geometry.RingedSpace.Stalks

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
U : TopCat
X : PresheafedSpace C
f : U ⟶ ↑X
h : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
x : ↑U
⊢ IsIso (Hom.stalkMap (X.ofRestrict h) x)

Tactic:
rw [← restrictStalkIso_inv_eq_ofRestrict]; infer_instance

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_1
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ (Opens.map (s.ι.app (unop j)).base).op.obj U =
    (Opens.map (colimit.ι (F ⋙ forget C) (unop j))).op.obj
      ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)

Tactic:
dsimp

Goal state after:
case refine_1
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j : Jᵒᵖ
⊢ op ((Opens.map (s.ι.app (unop j)).base).obj (unop U)) =
    op
      ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
        ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑Y
⊢ (ConcreteCategory.hom
        ({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).base)
      x✝ =
    (ConcreteCategory.hom (𝟙 Y).base) x✝

Tactic:
dsimp

Goal state after:
case w
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
x✝ : ↑↑Y
⊢ (Hom.hom H.hom) ((Hom.hom H.inv) x✝) = x✝
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ (({ base := H.inv, c := Presheaf.toPushforwardOfIso H α.hom } ≫ { base := H.hom, c := α.inv }).c ≫
          whiskerRight (eqToHom ⋯) Y.presheaf).app
      (op U✝) =
    (𝟙 Y).c.app (op U✝)

Tactic:
dsimp

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : ↑X ≅ ↑Y
α : (Presheaf.pushforward C H.hom).obj X.presheaf ≅ Y.presheaf
U✝ : Opens ↑↑Y
⊢ (α.inv.app (op U✝) ≫ (Presheaf.toPushforwardOfIso H α.hom).app (op ((Opens.map H.hom).obj U✝))) ≫
      Y.presheaf.map ((eqToHom ⋯).app (op U✝)) =
    (𝟙 Y).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ ((Functor.const Jᵒᵖ).obj (s.pt.presheaf.obj U)).map f ≫
      (s.ι.app (unop j')).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      ((pushforwardDiagramToColimit F).leftOp ⋙
            (evaluation (Opens ↑(Limits.colimit (F ⋙ forget C)))ᵒᵖ C).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).op.obj U)).map
        f

Tactic:
dsimp

Goal state after:
case refine_2
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
U : (Opens ↑↑s.pt)ᵒᵖ
j j' : Jᵒᵖ
f : j ⟶ j'
⊢ 𝟙 (s.pt.presheaf.obj U) ≫ (s.ι.app (unop j')).c.app U ≫ (F.obj (unop j')).presheaf.map (eqToHom ⋯) =
    ((s.ι.app (unop j)).c.app U ≫ (F.obj (unop j)).presheaf.map (eqToHom ⋯)) ≫
      (F.map f.unop).c.app
          (op
            ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
              ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))) ≫
        𝟙
            ((F.obj (unop j')).presheaf.obj
              (op
                ((Opens.map (F.map f.unop).base).obj
                  ((Opens.map (colimit.ι (F ⋙ forget C) (unop j))).obj
                    ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))))) ≫
          (pushforwardEq ⋯ (F.obj (unop j')).presheaf).hom.app
            (op ((Opens.map (colimit.desc (F ⋙ forget C) ((forget C).mapCocone s))).obj (unop U)))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))

Tactic:
dsimp

Goal state after:
X✝ X : LocallyRingedSpace
x : ↑↑X.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (𝟙 X.toPresheafedSpace) x))
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.hom ≫ homOfSheafedSpaceHomOfIsIso f.inv).toHom = (𝟙 X).toHom

Tactic:
dsimp

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ f.hom.hom ≫ f.inv.hom = 𝟙 X.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c ≫ H.hom.c).app (op U) =
    (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
H : X ≅ Y
U : Opens ↑↑Y
⊢ (Presheaf.pushforwardToOfIso ((forget C).mapIso H).symm H.inv.c).app (op U) ≫ H.hom.c.app (op U) =
    (𝟙 ((Presheaf.pushforward C H.hom.base).obj X.presheaf)).app (op U)
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ (homOfSheafedSpaceHomOfIsIso f.inv ≫ homOfSheafedSpaceHomOfIsIso f.hom).toHom = (𝟙 Y).toHom

Tactic:
dsimp

Goal state after:
X✝ X Y : LocallyRingedSpace
f : X.toSheafedSpace ≅ Y.toSheafedSpace
⊢ f.inv.hom ≫ f.hom.hom = 𝟙 Y.toPresheafedSpace
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rw [SetLike.mem_coe, X.toRingedSpace.mem_basicOpen _ _ hxU]

Goal state after:
case mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ IsUnit
    ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ (X.restrict ⋯).presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf

Tactic:
dsimp

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
⊢ ⋯.functor.op ⋙ X.presheaf = (Presheaf.pushforward C (Opens.inclusionTopIso ↑X).inv).obj X.presheaf
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)

Tactic:
dsimp

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
s : Cocone F
m : (colimitCocone F).pt ⟶ s.pt
w : ∀ (j : J), (colimitCocone F).ι.app j ≫ m = s.ι.app j
⊢ m.base = colimit.desc (F ⋙ forget C) ((forget C).mapCocone s)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case a
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
inst✝ : IsIso i
f : ↑(X.presheaf.obj U)
⊢ X.basicOpen f ≤ X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)

Tactic:
have := X.basicOpen_res (inv i) (X.presheaf.map i f)
    rw [← CommRingCat.comp_apply, ← X.presheaf.map_comp, IsIso.hom_inv_id, X.presheaf.map_id,
        CommRingCat.id_apply] at this
    rw [this]
    exact inf_le_right

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits

Goal state before:
pp: J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ (((lim.mapIso (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯)).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              ((Opens.map
                      (colimit.isoColimitCocone
                              { cocone := colimitCocone F,
                                isColimit := colimitCoconeIsColimit F }).symm.hom.base).op.obj
                (op U))).inv) ≫
        ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
              (op
                ((Opens.map
                      ((forget C).mapIso
                            (colimit.isoColimitCocone
                                { cocone := colimitCocone F,
                                  isColimit := colimitCoconeIsColimit F }).symm).symm.inv).obj
                  (unop (op U)))) ≫
            (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
dsimp

Goal state after:
J : Type u'
inst✝⁴ : Category.{v', u'} J
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasColimitsOfShape J TopCat
inst✝¹ : ∀ (X : TopCat), HasLimitsOfShape Jᵒᵖ (Presheaf C X)
inst✝ : HasLimitsOfShape Jᵒᵖ C
F : J ⥤ PresheafedSpace C
U : Opens ↑↑(Limits.colimit F)
j : J
⊢ ((limMap (NatIso.ofComponents (fun X ↦ mapIso (F.obj (unop X)).presheaf (eqToIso ⋯)) ⋯).inv ≫
          (limitObjIsoLimitCompEvaluation (pushforwardDiagramToColimit F).leftOp
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U))).inv) ≫
        ((colimit.isoColimitCocone { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.c.app
              (op
                ((Opens.map
                      (colimit.isoColimitCocone
                            { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                  U)) ≫
            (Limits.colimit F).presheaf.map
              (𝟙
                (op
                  ((Opens.map
                        (colimit.isoColimitCocone
                              { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).hom.base).obj
                    ((Opens.map
                          (colimit.isoColimitCocone
                                { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).inv.base).obj
                      U))))) ≫
          (Limits.colimit F).presheaf.map (eqToHom ⋯)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case h
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom
        (((sheafedSpaceMap (𝟙 R)).hom.c ≫ Functor.whiskerRight (eqToHom ⋯) (sheafedSpaceObj R).presheaf).app (op U✝)))
      x✝ =
    (CommRingCat.Hom.hom ((𝟙 (sheafedSpaceObj R)).hom.c.app (op U✝))) x✝

Tactic:
dsimp

Goal state after:
case h
R : CommRingCat
U✝ : TopologicalSpace.Opens ↑↑(sheafedSpaceObj R).toPresheafedSpace
x✝ : ↑((sheafedSpaceObj R).presheaf.obj (op U✝))
⊢ (CommRingCat.Hom.hom ((structureSheaf ↑R).obj.map (𝟙 (op ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝)))))
      ((comap (RingHom.id ↑R) U✝ ((TopologicalSpace.Opens.map (𝟙 (topObj R))).obj U✝) ⋯) x✝) =
    (CommRingCat.Hom.hom ((𝟙 (sheafedSpaceObj R).toPresheafedSpace).c.app (op U✝))) x✝
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 R).unop = 𝟙 (locallyRingedSpaceObj (unop R))

Tactic:
dsimp

Goal state after:
R : CommRingCatᵒᵖ
⊢ locallyRingedSpaceMap (𝟙 (unop R)) = 𝟙 (locallyRingedSpaceObj (unop R))
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (f ≫ g).unop = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop

Tactic:
dsimp

Goal state after:
X✝ Y✝ Z✝ : CommRingCatᵒᵖ
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ locallyRingedSpaceMap (g.unop ≫ f.unop) = locallyRingedSpaceMap f.unop ≫ locallyRingedSpaceMap g.unop
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
x✝ : ↑R
x' : ↥(unop (op ⊤))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x').asIdeal (↑x').asIdeal
        (CommRingCat.Hom.hom f.op.unop) ⋯)
      (↑((toSpecΓ R).hom' x✝) ⟨PrimeSpectrum.comap (CommRingCat.Hom.hom f.op.unop) ↑x', ⋯⟩) =
    ↑((CommRingCat.Hom.hom (f ≫ toSpecΓ S)) x✝) x'

Tactic:
apply Localization.localRingHom_to_map

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom
        (CommRingCat.ofHom
            (stalkIso (↑(CommRingCat.of ↑R))
                    (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                      x)).symm.toRingEquiv.toRingHom ≫
          CommRingCat.ofHom
              (Localization.localRingHom
                (PrimeSpectrum.comap (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M))))
                    x).asIdeal
                x.asIdeal (CommRingCat.Hom.hom (CommRingCat.ofHom (algebraMap (↑R) (Localization M)))) ⋯) ≫
            CommRingCat.ofHom (stalkIso (↑(CommRingCat.of (Localization M))) x).toRingEquiv.toRingHom))

Tactic:
dsimp

Goal state after:
R : CommRingCat
M : Submonoid ↑R
x : PrimeSpectrum (Localization M)
⊢ Function.Bijective
    ((⇑↑(stalkIso (Localization M) x) ∘
        ⇑(Localization.localRingHom (Ideal.comap (algebraMap (↑R) (Localization M)) x.asIdeal) x.asIdeal
            (algebraMap (↑R) (Localization M)) ⋯)) ∘
      ⇑(stalkIso (↑R) (PrimeSpectrum.comap (algebraMap (↑R) (Localization M)) x)).symm)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ (Y.restrict ⋯).presheaf.map i ≫
      (asIso (f.c.app (op ((opensFunctor f).obj (unop V)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom =
    (asIso (f.c.app (op ((opensFunctor f).obj (unop U)))) ≪≫ Functor.mapIso X.presheaf (eqToIso ⋯)).hom ≫
      ((TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf).map i

Tactic:
dsimp

Goal state after:
case naturality
C : Type u
inst✝ : Category.{v, u} C
X Y : PresheafedSpace C
f : X ⟶ Y
H : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
U V : (Opens ↑↑(Y.restrict ⋯))ᵒᵖ
i : U ⟶ V
⊢ Y.presheaf.map (⋯.functor.map i.unop).op ≫ f.c.app (op ((opensFunctor f).obj (unop V))) ≫ X.presheaf.map (eqToHom ⋯) =
    (f.c.app (op ((opensFunctor f).obj (unop U))) ≫ X.presheaf.map (eqToHom ⋯)) ≫
      X.presheaf.map ((Opens.map (𝟙 ↑X)).map i.unop).op
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ IsIso ((Y.ofRestrict hf).c.app (op (hf.functor.obj U)))

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X✝ Y✝ : PresheafedSpace C
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
X : TopCat
Y : PresheafedSpace C
f : X ⟶ ↑Y
hf : IsOpenEmbedding ⇑(ConcreteCategory.hom f)
U : Opens ↑↑(Y.restrict hf)
⊢ IsIso (Y.presheaf.map (⋯.adjunction.counit.app (hf.functor.obj U)).op)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
U V : (Opens ↑↑X)ᵒᵖ
i : U ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) ≫ g.c.app (op (⋯.functor.obj (unop V))) ≫ Y.presheaf.map (eqToHom ⋯) =
    (invApp f (unop U) ≫ g.c.app (op (⋯.functor.obj (unop U))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map i

Tactic:
induction U

Goal state after:
case op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
V : (Opens ↑↑X)ᵒᵖ
unop✝ : Opens ↑↑X
i : op unop✝ ⟶ V
⊢ X.presheaf.map i ≫ invApp f (unop V) ≫ g.c.app (op (⋯.functor.obj (unop V))) ≫ Y.presheaf.map (eqToHom ⋯) =
    (invApp f (unop (op unop✝)) ≫ g.c.app (op (⋯.functor.obj (unop (op unop✝)))) ≫ Y.presheaf.map (eqToHom ⋯)) ≫
      ((TopCat.Presheaf.pushforward C (pullback.fst f.base g.base)).obj (Y.restrict ⋯).presheaf).map i
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case refine_2
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
U : (Opens ↑↑Z)ᵒᵖ
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ Functor.whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app U =
    (Y.ofRestrict ⋯ ≫ g).c.app U

Tactic:
induction U

Goal state after:
case refine_2.op
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
unop✝ : Opens ↑↑Z
⊢ ((pullbackConeOfLeftFst f g ≫ f).c ≫ Functor.whiskerRight (eqToHom ⋯) (Y.restrict ⋯).presheaf).app (op unop✝) =
    (Y.ofRestrict ⋯ ≫ g).c.app (op unop✝)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : CommRingCat
f : ↑R
⊢ IsOpenEmbedding
    ⇑(ConcreteCategory.hom
        (LocallyRingedSpace.Hom.toShHom
              (Hom.toLRSHom (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (Localization.Away f)))))).hom.base)

Tactic:
exact (PrimeSpectrum.localization_away_isOpenEmbedding (Localization.Away f) f :)

Goal state after:
Module: Mathlib.AlgebraicGeometry.Sites.MorphismProperty

Goal state before:
pp: P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a, (pullback.fst f g) a = x

Tactic:
rw [← show _ = (pullback.fst _ _ : pullback f g ⟶ _).base from
        PreservesPullback.iso_hom_fst Scheme.forgetToTop f g]

Goal state after:
P : MorphismProperty Scheme
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝ : HasPullback f g
hg : IsOpenImmersion g
x : ↥X
y : ↥Y
h : f x = g y
⊢ ∃ a,
    (ConcreteCategory.hom
          ((PreservesPullback.iso forgetToTop f g).hom ≫ pullback.fst (forgetToTop.map f) (forgetToTop.map g)))
        a =
      x
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m = pullbackConeOfLeftLift f g s

Tactic:
← cancel_mono (pullbackConeOfLeft f g).snd

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
g : Y ⟶ Z
s✝ s : PullbackCone f g
m : s.pt ⟶ (pullbackConeOfLeft f g).pt
a✝ : m ≫ (pullbackConeOfLeft f g).fst = s.fst
h₂ : m ≫ (pullbackConeOfLeft f g).snd = s.snd
⊢ m ≫ (pullbackConeOfLeft f g).snd = pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).snd
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan ((cospan f g ⋙ forget).map Hom.inl) ((cospan f g ⋙ forget).map Hom.inr))
    (PresheafedSpace.forget C)

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : SheafedSpace C
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f.hom g.hom) (PresheafedSpace.forget C)
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } = Set.range ⇑f ∩ Set.range ⇑g

Tactic:
Opens.coe_mk,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier = Set.range ⇑f ∩ Set.range ⇑g
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ↑{ carrier := ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier, is_open' := ⋯ } = Set.range ⇑g ∩ Set.range ⇑f

Tactic:
Opens.coe_mk,

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ ⇑g '' ⇑g ⁻¹' (Scheme.Hom.opensRange f).carrier = Set.range ⇑g ∩ Set.range ⇑f