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

Goal state before:
pp: case op
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
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      (X.restrictStalkIso h x).inv =
    colimit.ι
        (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
              (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
          X.presheaf)
        (op V) ≫
      Hom.stalkMap (X.ofRestrict h) x

Tactic:
erw [Iso.comp_inv_eq, colimit.ι_map_assoc, colimit.ι_map_assoc, colimit.ι_pre]

Goal state after:
case op
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
V : OpenNhds ((ConcreteCategory.hom f) x)
i : (h.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V := homOfLE ⋯
⊢ colimit.ι
      (((whiskeringLeft (OpenNhds ((ConcreteCategory.hom f) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
            (OpenNhds.inclusion ((ConcreteCategory.hom f) x)).op).obj
        X.presheaf)
      (op V) =
    ((((whiskeringLeft (OpenNhds ((ConcreteCategory.hom (X.ofRestrict h).base) x))ᵒᵖ (Opens ↑↑X)ᵒᵖ C).obj
                  (OpenNhds.inclusion ((ConcreteCategory.hom (X.ofRestrict h).base) x)).op).map
              (X.ofRestrict h).c).app
          (op V) ≫
        (whiskerRight (NatTrans.op (OpenNhds.inclusionMapIso (X.ofRestrict h).base x).inv) (X.restrict h).presheaf).app
            (op V) ≫
          colimit.ι
            (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑↑(X.restrict h))ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj
              (X.restrict h).presheaf)
            ((OpenNhds.map (X.ofRestrict h).base x).op.obj (op V))) ≫
      (X.restrictStalkIso h x).hom
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ whiskerRight (𝟙 (Opens.map base).op) X.presheaf = c'
⊢ { base := base, c := c } = { base := base, c := c' }

Tactic:
whiskerRight_id',

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X Y : PresheafedSpace C
base : ↑X ⟶ ↑Y
c c' : Y.presheaf ⟶ (Presheaf.pushforward C base).obj X.presheaf
h : c ≫ 𝟙 ((Opens.map base).op ⋙ X.presheaf) = c'
⊢ { base := base, c := c } = { base := base, c := c' }
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace

Goal state before:
pp: X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x'

Tactic:
by
  subst hfg
  subst hxx'
  simp

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

Goal state before:
pp: X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) 1 =
    (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) ((ConcreteCategory.hom (X.presheaf.map (iVU y).op)) f * g y)

Tactic:
(hg y),

Goal state after:
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f : ↑(X.presheaf.obj (op U))
h : ∀ (x : ↑↑X.toPresheafedSpace) (hx : x ∈ U), IsUnit ((ConcreteCategory.hom (X.presheaf.germ U x hx)) f)
V : ↥U → Opens ↑↑X.toPresheafedSpace
iVU : (x : ↥U) → V x ⟶ U
m : ∀ (x : ↥U), ↑x ∈ V x
h_unit : ∀ (x : ↥U), IsUnit ((ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f)
hcover : U ≤ iSup V
g : (x : ↥U) → ↑(X.presheaf.obj (op (V x)))
hg : ∀ (x : ↥U), (ConcreteCategory.hom (X.presheaf.map (iVU x).op)) f * g x = 1
x y : ↥U
z : ↑↑X.toPresheafedSpace
hzVx : z ∈ ↑(V x)
hzVy : z ∈ ↑(V y)
⊢ (ConcreteCategory.hom (X.presheaf.germ (V x) z hzVx)) 1 = (ConcreteCategory.hom (X.presheaf.germ (V y) z hzVy)) 1
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case mp
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f)) → x ∈ ↑(unop V ⊓ X.basicOpen f)

pp: case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))

Tactic:
· rintro ⟨hxV, hx⟩
    rw [germ_res_apply' X.presheaf] at hx
    exact ⟨hxV, i.unop.le hxV, hx⟩

Goal state after:
case mpr
X : RingedSpace
U V : (Opens ↑↑X.toPresheafedSpace)ᵒᵖ
i : U ⟶ V
f : ↑(X.presheaf.obj U)
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑(unop V ⊓ X.basicOpen f) → x ∈ ↑(X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i)) f))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((eqToHom ⋯ ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (X.ofRestrict ⋯).c) ≫
          whiskerRight (eqToHom ⋯) (X.restrict ⋯).presheaf).app
      (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)

Tactic:
whiskerRight_id',

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑(X.restrict ⋯)
⊢ ((eqToHom ⋯ ≫ (Presheaf.pushforward C X.toRestrictTop.base).map (X.ofRestrict ⋯).c) ≫
          𝟙 ((Opens.map (X.ofRestrict ⋯ ≫ X.toRestrictTop).base).op ⋙ (X.restrict ⋯).presheaf)).app
      (op U✝) =
    (𝟙 (X.restrict ⋯)).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.Basic

Goal state before:
pp: case pos
X : RingedSpace
U : Opens ↑↑X.toPresheafedSpace
f g : ↑(X.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hx : x ∈ U
⊢ x ∈ ↑(X.basicOpen (f * g)) ↔ x ∈ ↑(X.basicOpen f ⊓ X.basicOpen g)

Tactic:
simp [mem_basicOpen (hx := hx)]

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

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
whiskerRight_id',

Goal state after:
case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((eqToHom ⋯ ≫ eqToHom ⋯) ≫ 𝟙 ((Opens.map (X.toRestrictTop ≫ X.ofRestrict ⋯).base).op ⋙ X.presheaf)).app (op U✝) =
    (𝟙 X).c.app (op U✝)
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace

Goal state before:
pp: case h
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : PresheafedSpace C
U✝ : Opens ↑↑X
⊢ ((X.toRestrictTop ≫ X.ofRestrict ⋯).c ≫ whiskerRight (eqToHom ⋯) X.presheaf).app (op U✝) = (𝟙 X).c.app (op U✝)

Tactic:
erw [comp_c, ofRestrict_top_c, toRestrictTop_c, eqToHom_map, whiskerRight_id', comp_id,
        eqToHom_trans, eqToHom_refl]
      rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: case w
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ (sheafedSpaceMap (f ≫ g)).hom.base = (sheafedSpaceMap g ≫ sheafedSpaceMap f).hom.base

Tactic:
exact Spec.topMap_comp f g

Goal state after:
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (structurePresheafInCommRingCat ↑R).germ ⊤ (PrimeSpectrum.comap (CommRingCat.Hom.hom f) p) trivial ≫
        PresheafedSpace.Hom.stalkMap (Spec.sheafedSpaceMap f).hom p =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial

Tactic:
PresheafedSpace.stalkMap_germ (Spec.sheafedSpaceMap f).hom ⊤ p trivial

Goal state after:
R S : CommRingCat
f : R ⟶ S
p : PrimeSpectrum ↑S
⊢ CommRingCat.ofHom (algebraMap (↑R) ((structureSheafInType ↑R ↑R).obj.obj (op ⊤))) ≫
      (Spec.sheafedSpaceMap f).hom.c.app (op ⊤) ≫
        (Spec.sheafedSpaceObj S).presheaf.germ ((TopologicalSpace.Opens.map (Spec.sheafedSpaceMap f).hom.base).obj ⊤) p
          trivial =
    f ≫
      CommRingCat.ofHom (algebraMap (↑S) ((structureSheafInType ↑S ↑S).obj.obj (op ⊤))) ≫
        (structurePresheafInCommRingCat ↑S).germ ⊤ p trivial
Module: Mathlib.AlgebraicGeometry.Spec

Goal state before:
pp: X Y : CommRingCat
f : X ⟶ Y
⊢ (𝟭 CommRingCat).map f ≫ (asIso (toSpecΓ Y)).hom =
    (asIso (toSpecΓ X)).hom ≫ (Spec.toLocallyRingedSpace.rightOp ⋙ Γ).map f

Tactic:
convert! Spec_Γ_naturality (R := X) (S := Y) f

Goal state after:
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 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (TopCat.Presheaf.pushforward C (Iso.refl ↑X).hom).obj X.presheaf ≅ (Y.restrict ⋯).presheaf

Tactic:
by
    symm
    fapply NatIso.ofComponents
    · intro U
      refine asIso (f.c.app (op (opensFunctor f |>.obj (unop U)))) ≪≫ X.presheaf.mapIso (eqToIso ?_)
      induction U with | op U => ?_
      cases U
      dsimp only [IsOpenMap.functor, Functor.op, Opens.map_def]
      congr 2
      erw [Set.preimage_image_eq _ H.base_open.injective]
      rfl
    · intro U V i
      dsimp
      simp only [NatTrans.naturality_assoc, TopCat.Presheaf.pushforward_obj_obj,
        TopCat.Presheaf.pushforward_obj_map, Quiver.Hom.unop_op, Category.assoc]
      rw [← X.presheaf.map_comp, ← X.presheaf.map_comp]
      congr 1

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U V : X.Opens
i : U ≤ V
s : Set ↑Γ(X, V)
⊢ X.zeroLocus (⇑(CommRingCat.Hom.hom (X.presheaf.map (homOfLE i).op)) '' s) = X.zeroLocus s ∪ (↑U)ᶜ

Tactic:
by
  ext x
  suffices (∀ f ∈ s, x ∈ U → x ∉ X.basicOpen f) ↔ x ∈ U → (∀ f ∈ s, x ∉ X.basicOpen f) by
    simpa [or_iff_not_imp_right]
  grind

Goal state after:
Module: Mathlib.AlgebraicGeometry.Scheme

Goal state before:
pp: X : Scheme
U : X.Opens
⊢ X.zeroLocus Set.univ = (↑U)ᶜ

Tactic:
by
  ext x
  simp only [Scheme.mem_zeroLocus_iff, Set.mem_univ, forall_const, Set.mem_compl_iff,
    SetLike.mem_coe, ← not_exists, not_iff_not]
  exact ⟨fun ⟨f, hf⟩ ↦ X.basicOpen_le f hf, fun _ ↦ ⟨1, by rwa [X.basicOpen_of_isUnit isUnit_one]⟩⟩

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U U' : X.Opens
h : f ''ᵁ U ≤ f ''ᵁ U'
⊢ f ⁻¹ᵁ f ''ᵁ U ≤ f ⁻¹ᵁ f ''ᵁ U'

Tactic:
apply f.preimage_mono h

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

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
X Y Z : PresheafedSpace C
f : X ⟶ Z
hf : IsOpenImmersion f
g : Y ⟶ Z
s : PullbackCone f g
⊢ (pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).base = s.fst.base

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
s : PullbackCone f g
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x

Tactic:
· change pullback.lift _ _ _ ≫ pullback.fst _ _ = _
    simp

Goal state after:
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
s : PullbackCone f g
x : (Opens ↑↑X)ᵒᵖ
⊢ ((pullbackConeOfLeftLift f g s ≫ (pullbackConeOfLeft f g).fst).c ≫ Functor.whiskerRight (eqToHom ⋯) s.pt.presheaf).app
      x =
    s.fst.c.app x
Module: Mathlib.CategoryTheory.Sites.MorphismProperty

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : P.IsMultiplicative
⊢ P.grothendieckTopology = P.pretopology.toGrothendieck

Tactic:
grothendieckTopology,

Goal state after:
C : Type u_1
inst✝³ : Category.{v_1, u_1} C
P : MorphismProperty C
inst✝² : P.IsStableUnderBaseChange
inst✝¹ : HasPullbacks C
inst✝ : P.IsMultiplicative
⊢ P.coverage.toGrothendieck = P.pretopology.toGrothendieck
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
⊢ HasLimit (cospan g f ⋙ forget)

Tactic:
have : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl)
      ((cospan g f ⋙ forget).map Hom.inr)) := by
    change HasLimit (cospan ((forget).map g) ((forget).map f))
    infer_instance

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
this : HasLimit (cospan ((cospan g f ⋙ forget).map Hom.inl) ((cospan g f ⋙ forget).map Hom.inr))
⊢ HasLimit (cospan g f ⋙ forget)
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]
      intro i
      exact 𝒰.map_prop _

Goal state after:
Module: Mathlib.AlgebraicGeometry.OpenImmersion

Goal state before:
pp: case neg.mp
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W) → x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W)

pp: case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W) → x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)

Tactic:
· rintro ⟨x, hx, rfl⟩; cases hx ⟨x, rfl⟩

Goal state after:
case neg.mpr
X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : IsOpenImmersion iU
H : IsPullback f' iU iV f
W : V.Opens
x : ↥X
hx : x ∉ Set.range ⇑iU
⊢ x ∈ ↑(f ⁻¹ᵁ iV ''ᵁ W) → x ∈ ↑(iU ''ᵁ f' ⁻¹ᵁ W)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ IsPullback (f ∣_ U) (f ⁻¹ᵁ U).ι U.ι f

Tactic:
apply IsOpenImmersion.isPullback <;>
  simp

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ Y✝ X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ UY ≤ g ⁻¹ᵁ UX

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X✝ Y✝ X Y S T : Scheme
f : T ⟶ S
g : Y ⟶ X
iX : X ⟶ S
iY : Y ⟶ T
H : IsPullback g iY iX f
US : S.Opens
UT : T.Opens
UX : X.Opens
hUST : UT ≤ f ⁻¹ᵁ US
hUSX : UX ≤ iX ⁻¹ᵁ US
UY : Y.Opens
hUY : UY = g ⁻¹ᵁ UX ⊓ iY ⁻¹ᵁ UT
⊢ UY ≤ iY ⁻¹ᵁ UT

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = ↑(𝒰.f i ⁻¹ᵁ Hom.opensRange U.ι)

Tactic:
Opens.opensRange_ι

Goal state after:
case refine_1
C : Type u₁
inst✝ : Category.{v, u₁} C
X : Scheme
𝒰 : X.OpenCover
U : X.Opens
i : 𝒰.I₀
⊢ Set.range ⇑(𝒰.f i ⁻¹ᵁ U).ι = ↑(𝒰.f i ⁻¹ᵁ U)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Equalizer

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasEqualizers C
inst✝ : HasPullbacks C
X Y S T : C
f g : X ⟶ Y
s : X ⟶ S
t : Y ⟶ S
hf : f ≫ t = s
hg : g ≫ t = s
v : T ⟶ S
⊢ (equalizerPullbackMapIso hf hg v).hom ≫ pullback.snd (equalizer.ι f g) (pullback.fst s v) =
    equalizer.ι (pullback.map s v t v f (𝟙 T) (𝟙 S) ⋯ ⋯) (pullback.map s v t v g (𝟙 T) (𝟙 S) ⋯ ⋯)

Tactic:
by
  ext <;> simp [equalizerPullbackMapIso]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) y = x

Tactic:
← Multicoequalizer.ι_sigmaπ D.diagram

Goal state after:
D : GlueData (Type v)
x : D.glued
⊢ ∃ i y, (ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) y = x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ ⇑hU.fromSpec ⁻¹' (⨆ f, X.basicOpen ↑f).carrier = ⇑hU.fromSpec ⁻¹' U.carrier ↔
    ⋃ i, (PrimeSpectrum.basicOpen ↑i).carrier = Set.univ

Tactic:
· simp only [Opens.iSup_def, Set.preimage_iUnion]
      congr! 1
      · refine congr_arg (Set.iUnion ·) ?_
        ext1 x
        exact congr_arg Opens.carrier (hU.fromSpec_preimage_basicOpen _)
      · exact congr_arg Opens.carrier hU.fromSpec_preimage_self

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
P : ↑X.affineOpens → Prop
ι : Sort u_2
U : ι → ↑X.affineOpens
iSup_U : ⨆ i, ↑(U i) = ⊤
V : ↑X.affineOpens
basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑Γ(X, ↑U)), P U → P (X.affineBasicOpen f)
openCover :
  ∀ (U : ↑X.affineOpens) (s : Finset ↑Γ(X, ↑U)), Ideal.span ↑s = ⊤ → (∀ (f : ↥s), P (X.affineBasicOpen ↑f)) → P U
hU : ∀ (i : ι), P (U i)
f : ↥↑V → ↑Γ(X, ↑V)
hf₁ : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (f x)
hf₂ : ∀ (x : ↥↑V), P (X.affineBasicOpen (f x))
x : ↥X
hx : x ∈ ↑V
⊢ ∃ i, x ∈ X.basicOpen (f i)

Tactic:
exact ⟨_, hf₁ ⟨x, hx⟩⟩

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

Goal state before:
pp: case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ (Opens.map (D.f j k).base).op.obj (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))) =
    op
      ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj
        (⋯.functor.obj U))

Tactic:
rw [Functor.op_obj]

Goal state after:
case left
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
j k : D.J
⊢ op ((Opens.map (D.f j k).base).obj (unop (op ((Opens.map (D.ι j).base).obj (⋯.functor.obj U))))) =
    op
      ((Opens.map (colimit.ι D.diagram.multispan (unop (op (WalkingMultispan.left (j, k))))).base).obj
        (⋯.functor.obj U))
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'

Tactic:
let f : Y ⟶ X := f'.unop

Goal state after:
case op.op
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i : D.J
U : Opens ↑↑(D.U i)
X Y : WalkingMultispan (MultispanShape.prod D.J)
f' : op X ⟶ op Y
f : Y ⟶ X := f'.unop
⊢ ((Functor.const (WalkingMultispan (MultispanShape.prod D.J))ᵒᵖ).obj ((D.U i).presheaf.obj (op U))).map f' ≫
      D.ιInvAppπApp U (unop (op Y)) =
    D.ιInvAppπApp U (unop (op X)) ≫ (D.diagramOverOpen U).map f'
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: case h₂
ι : Type u
f : ι → Scheme
σ : Type v
g : σ → Scheme
X Y : Scheme
R✝ S✝ : Type u
inst✝¹ : CommRing R✝
inst✝ : CommRing S✝
R S : CommRingCat
⊢ coprod.inr ≫
      coprodComparison Scheme.Spec (op R) (op S) ≫
        Spec.map
          ((limit.isoLimitCone { cone := R.prodFan S, isLimit := R.prodFanIsLimit S }).inv ≫
            (opProdIsoCoprod R S).unop.inv) =
    coprod.inr ≫ coprodSpec ↑R ↑S

Tactic:
rw [coprodComparison_inr_assoc, coprodSpec, coprod.inr_desc, Scheme.Spec_map,
        ← Spec.map_comp, Category.assoc, Iso.unop_inv, opProdIsoCoprod_inv_inr,
        limit.isoLimitCone_inv_π]
      rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Limits

Goal state before:
pp: σ : Type v
X : Scheme
inst✝ : Finite σ
U : σ → X.Opens
hU : ∀ (i : σ), IsAffineOpen (U i)
hU' : _root_.Pairwise (Disjoint on U)
ι : Type u
e : σ ≃ ι
this : Finite ι
⊢ ∀ (i : ι), IsAffineOpen (U (e.symm i))

Tactic:
by simp [*]

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
X Y : Scheme
f : X ⟶ Y
inst✝ : P.RespectsRight IsOpenImmersion
ι : Type u_1
U : ι → Y.Opens
H : Set.range ⇑f ⊆ ↑(⨆ i, U i)
hf : ∀ (i : ι), P (f ∣_ U i)
g : X ⟶ ↑(⨆ i, U i) := IsOpenImmersion.lift (⨆ i, U i).ι f ⋯
i : ι
heq : g ⁻¹ᵁ (⨆ i, U i).ι ⁻¹ᵁ U i = f ⁻¹ᵁ U i
e : Arrow.mk (g ∣_ (⨆ i, U i).ι ⁻¹ᵁ U i) ≅ Arrow.mk (f ∣_ U i) := Arrow.isoMk (X.isoOfEq heq) (Scheme.Opens.isoOfLE ⋯) ⋯
⊢ P (f ∣_ U i)

Tactic:
exact hf i

Goal state after:
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)

Tactic:
Cover.pushforwardIso_I₀,

Goal state after:
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
x : ↥(pullback f g)
i : (Cover.ulift 𝒰).I₀
⊢ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ =
    (Iso.refl (pullback ((Cover.ulift 𝒰).f i ≫ f) g)).hom ≫
      (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
            (limit.isoLimitCone
                { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
                  isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).f
        ((Equiv.refl (Cover.ulift 𝒰).I₀) i)
Module: Mathlib.AlgebraicGeometry.Pullbacks

Goal state before:
pp: case refine_1
X Y Z : Scheme
𝒰✝ : X.OpenCover
f✝ : X ⟶ Z
g✝ : Y ⟶ Z
inst✝ : ∀ (i : 𝒰✝.I₀), HasPullback (𝒰✝.f i ≫ f✝) g✝
s : PullbackCone f✝ g✝
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
𝒱 : Cover (precoverage IsOpenImmersion) (limit (cospan f g)) :=
  (Cover.pushforwardIso (gluing (Cover.ulift 𝒰) f g).openCover
        (limit.isoLimitCone
            { cone := PullbackCone.mk (p1 (Cover.ulift 𝒰) f g) (p2 (Cover.ulift 𝒰) f g) ⋯,
              isLimit := gluedIsLimit (Cover.ulift 𝒰) f g }).inv).copy
    (Cover.ulift 𝒰).I₀ (fun i ↦ pullback ((Cover.ulift 𝒰).f i ≫ f) g)
    (fun i ↦ pullback.map ((Cover.ulift 𝒰).f i ≫ f) g f g ((Cover.ulift 𝒰).f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯)
    (Equiv.refl (Cover.ulift 𝒰).I₀) (fun x ↦ Iso.refl (pullback ((Cover.ulift 𝒰).f x ≫ f) g)) ⋯
i : 𝒱.I₀
x : ↥(𝒱.X i)
⊢ ∃ i_1,
    (𝒱.f i) x ∈
      Set.range
        ⇑({ I₀ := 𝒰.I₀, X := fun i ↦ pullback (𝒰.f i ≫ f) g,
                f := fun i ↦ pullback.map (𝒰.f i ≫ f) g f g (𝒰.f i) (𝟙 Y) (𝟙 Z) ⋯ ⋯ }.f
            i_1)

Tactic:
exact ⟨_, x, rfl⟩

Goal state after: