mathlib-initiative/mathlib-tactics huggingface dataset:
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) ≫
        ((sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).app
            (op U)).inv) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)

Tactic:
Iso.app_inv,

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
⊢ (((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) ≫
        (sheafIsoOfIso
                (colimit.isoColimitCocone
                    { cocone := colimitCocone F, isColimit := colimitCoconeIsColimit F }).symm).inv.app
          (op U)) ≫
      (colimit.ι F j).c.app (op U) =
    limit.π (componentwiseDiagram F U) (op j)
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ sheafedSpaceMap (f ≫ g) = sheafedSpaceMap g ≫ sheafedSpaceMap f

Tactic:
ext : 1
  · exact Spec.topMap_comp f g
  · ext
    -- Porting note: was one liner
    -- `dsimp, rw category_theory.functor.map_id, rw category.comp_id, erw comap_comp f g, refl`
    rw [NatTrans.comp_app, sheafedSpaceMap_hom_c_app, Functor.whiskerRight_app, eqToHom_refl]
    erw [(sheafedSpaceObj T).presheaf.map_id]
    dsimp only [CommRingCat.hom_comp, RingHom.coe_comp, Function.comp_apply]
    rw [comap_comp]
    rfl

Goal state after:
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
s : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ (Opens.map s.snd.base).op.obj (⋯.functor.op.obj U) = (Opens.map (pullback.lift s.fst.base s.snd.base ⋯)).op.obj U

Tactic:
dsimp only [Opens.map_def, IsOpenMap.functor, Functor.op]

Goal state after:
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 : PullbackCone f g
U : (Opens ↑↑(pullbackConeOfLeft f g).pt)ᵒᵖ
⊢ op { carrier := ⇑(ConcreteCategory.hom s.snd.base) ⁻¹' ↑(⋯.functor.obj (unop U)), is_open' := ⋯ } =
    op { carrier := ⇑(ConcreteCategory.hom (pullback.lift s.fst.base s.snd.base ⋯)) ⁻¹' ↑(unop U), is_open' := ⋯ }
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
⊢ f ⁻¹ᵁ opensRange f = ⊤

Tactic:
by
  simp [Scheme.Hom.opensRange]

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (app f (f ''ᵁ U))

Tactic:
delta opensFunctor

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ IsIso (app f ((LocallyRingedSpace.IsOpenImmersion.opensFunctor (toLRSHom f)).obj U))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map (homOfLE ⋯).op ≫ Y.presheaf.map (homOfLE ⋯).op = Y.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Functor.map_comp]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Y.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op) = Y.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Functor.map_comp]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Cover.MorphismProperty

Goal state before:
pp: case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : { I₀ := J, X := obj, f := map }.I₀), P ({ I₀ := J, X := obj, f := map }.f i)

Tactic:
simp_rw [h, MorphismProperty.cancel_left_of_respectsIso]

Goal state after:
case refine_2
K : Precoverage Scheme
X✝ Y Z : Scheme
𝒰✝ : Cover K X✝
f : X✝ ⟶ Z
g : Y ⟶ Z
inst✝¹ : ∀ (x : 𝒰✝.I₀), HasPullback (𝒰✝.f x ≫ f) g
P Q : MorphismProperty Scheme
inst✝ : P.RespectsIso
X : Scheme
𝒰 : Cover (precoverage P) X
J : Type u_1
obj : J → Scheme
map : (i : J) → obj i ⟶ X
e₁ : J ≃ 𝒰.I₀
e₂ : (i : J) → obj i ≅ 𝒰.X (e₁ i)
h : ∀ (i : J), map i = (e₂ i).hom ≫ 𝒰.f (e₁ i)
⊢ ∀ (i : J), P (𝒰.f (e₁ i))
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
H : IsOpenImmersion f✝
P X Y Z : Scheme
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsOpenImmersion g
p : ↥P
x : ↥X
hx : fst p = x
this : IsOpenImmersion fst
⊢ x = fst p

Tactic:
rw [hx]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case hcover
X : Scheme
U : X.Opens
f g : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) f = (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) g
⊢ U ≤ ⨆ i, Hom.opensRange (𝒰.f (Cover.idx 𝒰 i)) ⊓ U

Tactic:
intro x hx
    simp only [Opens.iSup_mk, Opens.carrier_eq_coe, Opens.coe_inf, Hom.coe_opensRange, Opens.mem_mk,
      Set.mem_iUnion, Set.mem_inter_iff, Set.mem_range, SetLike.mem_coe, exists_and_right]
    refine ⟨?_, hx⟩
    simpa using ⟨_, 𝒰.covers x⟩

Goal state after:
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

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

Tactic:
change PreservesLimit _ <|
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙
    PresheafedSpace.forget _

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
⊢ PreservesLimit (cospan f g)
    ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) ⋙ PresheafedSpace.forget CommRingCat)
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
⊢ 0 ≫ (forget₂ TopCommRingCat TopCat).map φ = 0

Tactic:
ext; exact φ.1.map_zero

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away x)

Tactic:
rw [hx]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
R : CommRingCat
f g x : ↑R
hx : x = f * g
⊢ IsLocalization.Away (f * g) (Localization.Away (f * g))
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫ pullback.snd (f ≫ g) (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)

Tactic:
rw [← pullbackRightPullbackFstIso_inv_snd_snd]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
U : Opens ↥Z
⊢ (pullbackRestrictIsoRestrict (f ≫ g) U).inv ≫
      (pullbackRightPullbackFstIso g (Scheme.Opens.ι U) f).inv ≫
        pullback.snd f (pullback.fst g (Scheme.Opens.ι U)) ≫ pullback.snd g (Scheme.Opens.ι U) =
    ((pullbackRestrictIsoRestrict f (g ⁻¹ᵁ U)).inv ≫ pullback.snd f (g ⁻¹ᵁ U).ι) ≫
      (pullbackRestrictIsoRestrict g U).inv ≫ pullback.snd g (Scheme.Opens.ι U)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
hU : IsCompact ↑U
s : (structureSheafInType R M).obj.obj (op U)
g : ↥U → R
hxg : ∀ (x : ↥U), ↑x ∈ basicOpen (g x)
igU : ∀ (x : ↥U), basicOpen (g x) ≤ U
f : ↥U → M
H :
  ∀ (x : ↥U),
    const (f x) (g x) (basicOpen (g x)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
n : ↥U → ↥U → ℕ
hn : ∀ (i j : ↥U), ((g i * g j) ^ (n i j + 1) * g i) • f j = ((g i * g j) ^ (n i j + 1) * g j) • f i
t : Finset ↥U
ht : ↑U ⊆ ⋃ i ∈ t, ↑(basicOpen (g i))
N : ℕ := (t ×ˢ t).sup fun x ↦ n x.1 x.2 + 1
x : ↥t
⊢ basicOpen ((fun i ↦ g ↑i ^ (N + 1)) x) ≤ U

Tactic:
by simpa using igU x.1

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ⨆ i, ↑i = ⊤

Tactic:
apply Opens.ext
  rw [Opens.coe_iSup]
  apply IsTopologicalBasis.sUnion_eq
  rw [← Set.image_eq_range]
  exact X.isBasis_affineOpens

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_2
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
⊢ ∀ (i : 𝒰.I₀),
    𝒰.f i ∣_ U =
      (IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)

Tactic:
intro i
    rw [← cancel_mono U.ι]
    simp [morphismRestrict_ι, Equiv.refl_apply, Category.assoc, pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Function.Bijective ⇑(toOpenₗ R M ⊤)

Tactic:
by
  have : IsLocalizedModule ⊥ (toOpenₗ R M ⊤) := by
    convert! (inferInstance : IsLocalizedModule (.powers 1) (toOpenₗ R M (basicOpen 1)))
    rw [PrimeSpectrum.basicOpen_one, Submonoid.powers_one]
  refine ⟨fun x y e ↦ by simpa using (IsLocalizedModule.eq_iff_exists ⊥ _).mp e, fun x ↦ ?_⟩
  obtain ⟨⟨x, _, rfl⟩, rfl⟩ := IsLocalizedModule.mk'_surjective ⊥ (toOpenₗ R M ⊤) x
  exact ⟨x, (IsLocalizedModule.mk'_one ..).symm⟩

Goal state after:
Module: Mathlib.CategoryTheory.LocallyDirected

Goal state before:
pp: case init.init
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
F : WidePushoutShape J ⥤ Type u_2
inst✝ : ∀ (i : J), Mono (F.map (WidePushoutShape.Hom.init i))
i : J
⊢ ∀ (xi : F.obj none),
    ∃ l fli flj x, (ConcreteCategory.hom (F.map fli)) x = xi ∧ (ConcreteCategory.hom (F.map flj)) x = xi

Tactic:
exact fun x ↦ ⟨_, 𝟙 _, 𝟙 _, x, by simp⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx = toStalkₗ' R M x

Tactic:
rw [toStalkₗ', ← Presheaf.germ_res _ (homOfLE le_top) _ hx, ← Category.assoc]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
⊢ ModuleCat.ofHom (toOpenₗ R M U) ≫ (structurePresheafInModuleCat R M).germ U x hx =
    (ModuleCat.ofHom (toOpenₗ R M ⊤) ≫ (structurePresheafInModuleCat R M).map (homOfLE ⋯).op) ≫
      (structurePresheafInModuleCat R M).germ U x hx
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
⊢ Set.range ⇑(U.ι ≫ f) = Set.range ⇑(f ''ᵁ U).ι

Tactic:
by simp [Scheme.Hom.comp_base, Set.range_comp]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
x : ↑(PrimeSpectrum.Top R)
⊢ IsLocalization.AtPrime (↑((structurePresheafInCommRingCat R).stalk x)) x.asIdeal

Tactic:
by
  refine (isLocalizedModule_iff_isLocalization' _ _).mp ?_
  convert!
    IsLocalizedModule.of_linearEquiv x.asIdeal.primeCompl (toStalkₗ R R x)
      (commRingCatStalkEquivModuleStalk R x)
  let α : TopCat.Presheaf.stalk (moduleStructurePresheaf R R).presheaf x ≅
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).obj
      ((structurePresheafInCommRingCat R).stalk x) :=
    (Limits.colimit.isoColimitCocone ⟨_, Limits.isColimitOfPreserves
    (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat)
    (Limits.colimit.isColimit ((OpenNhds.inclusion x).op ⋙
      structurePresheafInCommRingCat R))⟩)
  have : (TopCat.Presheaf.germ (moduleStructurePresheaf R R).presheaf ⊤ x (by simp)) ≫ α.hom =
      (forget₂ CommRingCat RingCat ⋙ forget₂ RingCat AddCommGrpCat).map
        ((structurePresheafInCommRingCat R).germ ⊤ x (by simp)) :=
    Limits.colimit.isoColimitCocone_ι_hom ..
  ext
  dsimp [toStalkₗ]
  simp only [map_one]
  refine .trans ?_ congr($this _).symm
  exact (((structurePresheafInCommRingCat R).germ ⊤ x (by simp)).hom.comp
    (algebraMap R Γ(R, _))).map_one.symm

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Coequalizers

Goal state before:
pp: case mp
X Y Z : Type u
f g : X ⟶ Y
π : Y ⟶ Z
e : f ≫ π = g ≫ π
h : IsColimit (Cofork.ofπ π e)
U : Set Y
H : ⇑(hom f) ⁻¹' U = ⇑(hom g) ⁻¹' U
lem : ∀ (x y : (fun X ↦ X) Y), Function.Coequalizer.Rel (⇑(hom f)) (⇑(hom g)) x y → (x ∈ U ↔ y ∈ U)
eqv : _root_.Equivalence fun x y ↦ x ∈ U ↔ y ∈ U
x✝ : (fun X ↦ X) Y
⊢ x✝ ∈ ⇑(hom π) ⁻¹' ⇑(hom π) '' U → x✝ ∈ U

Tactic:
rw [←
      show _ = π from
        h.comp_coconePointUniqueUpToIso_inv (coequalizerColimit f g).2
          WalkingParallelPair.one]
    rintro ⟨y, hy, e'⟩
    dsimp at e'
    have e'' :=
      (mono_iff_injective
            (h.coconePointUniqueUpToIso (coequalizerColimit f g).isColimit).inv).mp
        inferInstance
    refine (eqv.eqvGen_iff.mp (Relation.EqvGen.mono lem y _ (Quot.eqvGen_exact ?_))).mp hy
    apply e''
    convert! e'

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ PrimeSpectrum.comap (RingHom.id R) ⁻¹' U.carrier

Tactic:
rwa [hUV, PrimeSpectrum.comap_id]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
ι : Type u_1
I : ι → Ideal ↑Γ(X, U)
t : Set ι
ht : t.Finite
ht' : t.Nonempty
⊢ X.zeroLocus ↑(⨅ i ∈ t, I i) = ⋃ i ∈ t, X.zeroLocus ↑(I i)

Tactic:
rw [zeroLocus_biInf I ht, Set.union_eq_left]
  obtain ⟨i, hi⟩ := ht'
  exact fun x hx ↦ Set.mem_iUnion₂_of_mem hi
    (codisjoint_iff_compl_le_left.mp (X.codisjoint_zeroLocus (U := U) (I i)) hx)

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

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
⊢ { l //
    (coequalizerCofork f g).π ≫ l = s.π ∧
      ∀ {m : (coequalizerCofork f g).pt ⟶ s.pt}, (coequalizerCofork f g).π ≫ m = s.π → m = l }

Tactic:
refine ⟨⟨(coequalizer.desc s.π.toShHom e).hom, fun x ↦ ?_⟩,
    ⟨Hom.ext' (Functor.congr_map SheafedSpace.forgetToPresheafedSpace
      (coequalizer.π_desc (Hom.toShHom s.π) e)),
      fun {m} hm ↦ LocallyRingedSpace.forgetToSheafedSpace.map_injective
        (coequalizer.hom_ext ((LocallyRingedSpace.forgetToSheafedSpace.congr_map hm).trans
      ((coequalizer.π_desc _ _).symm)))⟩⟩

Goal state after:
X Y : LocallyRingedSpace
f g : X ⟶ Y
s : Cofork f g
e : Hom.toShHom f ≫ Hom.toShHom s.π = Hom.toShHom g ≫ Hom.toShHom s.π
x : ↑↑(coequalizerCofork f g).pt.toPresheafedSpace
⊢ IsLocalHom (CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap (coequalizer.desc (Hom.toShHom s.π) e).hom x))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    inv (invApp (D.f i j) U) ≫
      (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
IsOpenImmersion.inv_invApp

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    ((D.f i j).c.app (op ((opensFunctor (D.f i j)).obj U)) ≫ (D.V (i, j)).presheaf.map (eqToHom ⋯)) ≫
      (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
        invApp (pullback.snd (D.f i j) (D.f i k))
            (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).1 (unop (op U))))) ≫
          (D.V (i, k)).presheaf.map (eqToHom ⋯)
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: D✝ : GlueData
D : GlueData
⊢ (∀ (x : ↥D.glued), ∃ i, x ∈ Set.range ⇑({ I₀ := D.J, X := D.U, f := D.ι }.f i)) ∧
    ∀ (i : { I₀ := D.J, X := D.U, f := D.ι }.I₀), IsOpenImmersion ({ I₀ := D.J, X := D.U, f := D.ι }.f i)

Tactic:
exact ⟨D.ι_jointly_surjective, inferInstance⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case right
ι : Type u
f : ι → Scheme
X : Scheme
α : (i : ι) → f i ⟶ X
inst✝ : ∀ (i : ι), IsOpenImmersion (α i)
hα : _root_.Pairwise (Disjoint on fun x ↦ Set.range ⇑(α x))
⊢ ∀ (x : ↥(∐ f)), IsIso (Scheme.Hom.stalkMap (Sigma.desc α) x)

Tactic:
intro x
    have ⟨y, hy⟩ := (Scheme.IsLocallyDirected.openCover (Discrete.functor f)).covers x
    rw [← hy]
    refine IsIso.of_isIso_fac_right
      (f := ((Scheme.IsLocallyDirected.openCover (Discrete.functor f)).f _).stalkMap y)
      (h := (X.presheaf.stalkCongr (.of_eq ?_)).hom ≫ (α _).stalkMap _) ?_
    · simp [← Scheme.Hom.comp_apply]
    · simp [← Scheme.Hom.stalkMap_comp, Scheme.Hom.stalkMap_congr_hom _ _ (colimit.ι_desc _ _)]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp_rw [Scheme.Hom.isoOpensRange_hom_ι_assoc, IsOpenImmersion.comp_lift_assoc]

Goal state after:
J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j k : Shrink.{u, w} J
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
l : J
fi : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fj : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
fk : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
α : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
z : ↥(F.obj l)
hα : IsOpenImmersion α
hα₁ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hα₂ : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
e : α z = x
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: case mpr
P : MorphismProperty Scheme
inst✝ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
⊢ targetAffineLocally (AffineTargetMorphismProperty.of P) f → P f

Tactic:
· intro hf
      exact P.of_zeroHypercover_target Y.affineCover
        fun i ↦ of_targetAffineLocally_of_isPullback (.of_hasPullback _ _) hf

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ P.RespectsIso

Tactic:
eq_targetAffineLocally P

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
this : Q.IsLocal := isLocal_affineProperty P
⊢ (targetAffineLocally Q).RespectsIso
Module: Mathlib.AlgebraicGeometry.Morphisms.Basic

Goal state before:
pp: P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ P f

Tactic:
eq_targetAffineLocally P

Goal state after:
P : MorphismProperty Scheme
Q : AffineTargetMorphismProperty
inst✝ : HasAffineProperty P Q
X Y : Scheme
f : X ⟶ Y
ι : Sort u_1
U : ι → ↑Y.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
hU' : ∀ (i : ι), Q (f ∣_ ↑(U i))
this : Q.IsLocal := isLocal_affineProperty P
⊢ targetAffineLocally Q f