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

Goal state before:
pp: case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
j : Discrete ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
as✝ : ι
h : { as := as✝ } ≠ j
U : Opens ↑↑(F.obj { as := as✝ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝ }).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F j) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False

Tactic:
;

Goal state after:
case mk
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasLimits C
ι : Type v
F : Discrete ι ⥤ SheafedSpace C
inst✝ : HasColimit F
j : Discrete ι
x : ↑↑((F ⋙ forgetToPresheafedSpace).obj j)
as✝ : ι
h : { as := as✝ } ≠ j
U : Opens ↑↑(F.obj { as := as✝ }).toPresheafedSpace
y : ↑↑(F.obj { as := as✝ }).toPresheafedSpace
hy : y ∈ ↑U
eq :
  (ConcreteCategory.hom
        ((forget C).map (colimit.ι F { as := as✝ }) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      y =
    (ConcreteCategory.hom
        ((forget C).map (colimit.ι F j) ≫
          (preservesColimitIso (forget C) F).hom ≫
            (HasColimit.isoOfNatIso Discrete.natIsoFunctor).hom ≫
              (TopCat.sigmaIsoSigma ((F ⋙ forget C).obj ∘ Discrete.mk)).hom))
      x
⊢ False
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f✝) g
𝒱 : X.OpenCover
f : 𝒰 ⟶ 𝒱
i : 𝒰.I₀
⊢ IsOpenImmersion (𝒰.f i)

Tactic:
;

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f✝ : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f✝) g
𝒱 : X.OpenCover
f : 𝒰 ⟶ 𝒱
i : 𝒰.I₀
⊢ IsOpenImmersion (𝒰.f i)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
⊢ ⋃ i, ↑(Hom.opensRange (𝒰.f i)) = ↑⊤

Tactic:
;

Goal state after:
X : Scheme
𝒰 : X.OpenCover
⊢ ⋃ i, ↑(Hom.opensRange (𝒰.f i)) = ↑⊤
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
H : CompactSpace ↥X
⊢ Fintype
    (have this := ⋯;
      let t := this.choose;
      have h := ⋯;
      { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x), mem₀ := ⋯ }).I₀

Tactic:
;

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
H : CompactSpace ↥X
⊢ Fintype
    (have this := ⋯;
      let t := this.choose;
      have h := ⋯;
      { I₀ := ↥t, X := fun x ↦ 𝒰.X (Cover.idx 𝒰 ↑x), f := fun x ↦ 𝒰.f (Cover.idx 𝒰 ↑x), mem₀ := ⋯ }).I₀
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ False

Tactic:
;

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ False
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ x.asIdeal = ⊤

Tactic:
;

Goal state after:
X Y Z : Scheme
𝒰 : X.OpenCover
f : X ⟶ Z
g : Y ⟶ Z
inst✝ : ∀ (x : 𝒰.I₀), HasPullback (𝒰.f x ≫ f) g
R : CommRingCat
ι : Type u_1
s : ι → ↑R
hs : Ideal.span (Set.range s) = ⊤
x : ↥(Spec R)
h : ∀ (i : ι), s i ∈ x.asIdeal
⊢ x.asIdeal = ⊤
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
h : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s = 0
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) (s ^ N) = 0

Tactic:
;

Goal state after:
case h
X : Scheme
U : X.Opens
s : ↑Γ(X, U)
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
fn : 𝒰.I₀ → ℕ
hfn : ∀ (i : 𝒰.I₀), (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) s ^ fn i = 0
this : Fintype 𝒰.I₀
N : ℕ := Finset.univ.sup fn
hfnleN : ∀ (i : 𝒰.I₀), fn i ≤ N
i : 𝒰.I₀
⊢ (ConcreteCategory.hom (Hom.app (𝒰.f i) U)) (s ^ N) = 0
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
P : ↑(PrimeSpectrum.Top R)
V U : Opens ↑(PrimeSpectrum.Top R)
i : V ⟶ U
f : (x : ↥U) → Localizations M ↑x
r : M
s : R
w : ∀ (x : ↥U), ∃ (hs : s ∉ (↑x).asIdeal), f x = LocalizedModule.mk r ⟨s, hs⟩
⊢ IsFraction fun x ↦ f (i x)

Tactic:
;

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
P : ↑(PrimeSpectrum.Top R)
V U : Opens ↑(PrimeSpectrum.Top R)
i : V ⟶ U
f : (x : ↥U) → Localizations M ↑x
r : M
s : R
w : ∀ (x : ↥U), ∃ (hs : s ∉ (↑x).asIdeal), f x = LocalizedModule.mk r ⟨s, hs⟩
⊢ IsFraction fun x ↦ f (i x)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mp
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
y : ↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y)
eq :
  (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x✝ =
    (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)

Tactic:
;

Goal state after:
case mp
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
y : ↑((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).obj Y)
eq :
  (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x✝ =
    (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y
⊢ x✝ ∈ ⇑(ConcreteCategory.hom f.base) ⁻¹' Set.range ⇑(ConcreteCategory.hom g.base)
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: X : Scheme
a : ↥X
U : Set ↥X
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
haU : (X.affineCover.f (Cover.idx X.affineCover a)) x ∈ U
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'

Tactic:
;

Goal state after:
X : Scheme
a : ↥X
U : Set ↥X
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
haU : (X.affineCover.f (Cover.idx X.affineCover a)) x ∈ U
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
⊢ x ∈ U'
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: case mpr
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
eq : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x✝
⊢ x✝ ∈
    {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y}

Tactic:
;

Goal state after:
case mpr
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
this✝ : IsIso (pullback.snd f g)
this :
  (PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat) f g).hom ≫
      pullback.fst ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g) =
    (pullback.fst f g).base
x✝ : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
eq : (ConcreteCategory.hom g.base) y = (ConcreteCategory.hom f.base) x✝
⊢ x✝ ∈
    {x |
      ∃ y,
        (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map f)) x =
          (ConcreteCategory.hom ((forgetToSheafedSpace ⋙ SheafedSpace.forget CommRingCat).map g)) y}
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 : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ((structureSheafInType R R).obj.obj X) ((structureSheafInType R M).obj.obj X)

Tactic:
;

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
X : (Opens ↑(PrimeSpectrum.Top R))ᵒᵖ
⊢ Module ((structureSheafInType R R).obj.obj X) ((structureSheafInType R M).obj.obj X)
Module: Mathlib.Geometry.RingedSpace.OpenImmersion

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ IsIso (PresheafedSpace.IsOpenImmersion.invApp f.toHom U)

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y : LocallyRingedSpace
f : X ⟶ Y
H : IsOpenImmersion f
U : Opens ↑X.toTopCat
⊢ IsIso (PresheafedSpace.IsOpenImmersion.invApp f.toHom U)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
W : (↑U).Opens
e : W ≤ U.ι ⁻¹ᵁ V
⊢ Hom.appLE U.ι V W e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [Hom.appLE, ι_app, toScheme_presheaf_map, Quiver.Hom.unop_op,
    Hom.opensFunctor_map_homOfLE, ← Functor.map_comp]
  rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ (g * g') • f = (g' * g) • f

Tactic:
;

Goal state after:
case refine_3
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
U : Opens ↑(PrimeSpectrum.Top R)
s : (structureSheafInType R M).obj.obj (op U)
x : ↑(PrimeSpectrum.Top R)
hx : x ∈ U
V : Opens ↑(PrimeSpectrum.Top R)
hxV : ↑⟨x, hx⟩ ∈ V
iVU : V ⟶ unop (op U)
f : M
g : R
hfg : ∀ (x : ↥V), ∃ (hs : g ∉ (↑x).asIdeal), (fun x ↦ ↑s (iVU x)) x = LocalizedModule.mk f ⟨g, hs⟩
g' : R
hxg' : ↑⟨x, hx⟩ ∈ ↑(basicOpen g')
hg'U : ↑(basicOpen g') ⊆ ↑V
x✝ : ↥(unop (op (basicOpen (g' * g))))
y : ↑(PrimeSpectrum.Top R)
hy✝ : y ∈ unop (op (basicOpen (g' * g)))
hy : y ∈ unop (op (basicOpen g' ⊓ basicOpen g))
hgy : g ∉ (↑⟨y, ⋯⟩).asIdeal
H : (fun x ↦ ↑s (iVU x)) ⟨y, ⋯⟩ = LocalizedModule.mk f ⟨g, hgy⟩
⊢ (g * g') • f = (g' * g) • f
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ 0 = ↑0 x

Tactic:
;

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen f
x : ↥(unop (op U))
⊢ 0 = ↑0 x
Module: Mathlib.AlgebraicGeometry.Cover.Open

Goal state before:
pp: case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ (PrimeSpectrum.basicOpen s).carrier ⊆ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U

Tactic:
;

Goal state after:
case h_nhds.refine_2
X : Scheme
a : ↥X
U : Set ↥X
haU : a ∈ U
hU : IsOpen U
x : ↥(X.affineCover.X (Cover.idx X.affineCover a))
e : (X.affineCover.f (Cover.idx X.affineCover a)) x = a
U' : Set ↥(X.affineCover.X (Cover.idx X.affineCover a)) := ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
hxU' : x ∈ U'
s : ↑((fun x ↦ Classical.choose ⋯) (Cover.idx X.affineCover a))
hxV : x ∈ ↑(PrimeSpectrum.basicOpen s)
hVU : ↑(PrimeSpectrum.basicOpen s) ⊆ U'
⊢ (PrimeSpectrum.basicOpen s).carrier ⊆ ⇑(X.affineCover.f (Cover.idx X.affineCover a)) ⁻¹' U
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ : M
g₁ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
⊢ const f₁ g₁ U hu = const f₁ g₁ U ⋯

Tactic:
;

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ : M
g₁ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu : U ≤ basicOpen g₁
⊢ const f₁ g₁ U hu = const f₁ g₁ U ⋯
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ • (f * g₁) = (g₁ * g₂) • f

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ • (f * g₁) = (g₁ * g₂) • f
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: R : TopCommRingCat
⊢ Continuous ⇑{ toFun := fun x ↦ x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

Tactic:
;

Goal state after:
R : TopCommRingCat
⊢ Continuous ⇑{ toFun := fun x ↦ x, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Module: Mathlib.Topology.Category.TopCommRingCat

Goal state before:
pp: R : TopCommRingCat
⊢ Continuous fun x ↦ x

Tactic:
;

Goal state after:
R : TopCommRingCat
⊢ Continuous fun x ↦ x
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ * (f * g₁) = g₁ * g₂ * f

Tactic:
;

Goal state after:
R : Type u
inst✝ : CommRing R
f g₁ g₂ : R
U : Opens ↑(PrimeSpectrum.Top R)
hu₁ : U ≤ basicOpen g₁
hu₂ : U ≤ basicOpen g₂
⊢ g₂ * (f * g₁) = g₁ * g₂ * f
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 : R
f : M
g : ↥(Submonoid.powers s)
this : ∀ (n : ℕ), basicOpen s ≤ basicOpen (s ^ n)
⊢ basicOpen s ≤ basicOpen ↑g

Tactic:
;

Goal state after:
R M A : Type u
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : CommRing A
inst✝ : Algebra R A
s : R
f : M
g : ↥(Submonoid.powers s)
this : ∀ (n : ℕ), basicOpen s ≤ basicOpen (s ^ n)
⊢ basicOpen s ≤ basicOpen ↑g
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥↑U
⊢ (X.homOfLE e) a = (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a

Tactic:
;

Goal state after:
X : Scheme
U V : X.Opens
e : U ≤ V
a : ↥↑U
⊢ (X.homOfLE e) a = (ConcreteCategory.hom ((Opens.toTopCat ↑X.toPresheafedSpace).map (homOfLE e))) a
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom (1 ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ = (ConcreteCategory.hom 1) x✝

Tactic:
;

Goal state after:
X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom (1 ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ = (ConcreteCategory.hom 1) x✝
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝² x✝¹ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom ((x✝² * x✝¹) ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ =
    (ConcreteCategory.hom (x✝² ≫ (forget₂ TopCommRingCat TopCat).map φ * x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ))
      x✝

Tactic:
;

Goal state after:
X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝² x✝¹ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom ((x✝² * x✝¹) ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ =
    (ConcreteCategory.hom (x✝² ≫ (forget₂ TopCommRingCat TopCat).map φ * x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ))
      x✝
Module: Mathlib.Topology.Sheaves.CommRingCat

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

Tactic:
;

Goal state after:
X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom (0 ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ = (ConcreteCategory.hom 0) x✝
Module: Mathlib.Topology.Sheaves.CommRingCat

Goal state before:
pp: X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝² x✝¹ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom ((x✝² + x✝¹) ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ =
    (ConcreteCategory.hom (x✝² ≫ (forget₂ TopCommRingCat TopCat).map φ + x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ))
      x✝

Tactic:
;

Goal state after:
X✝ : TopCat
R✝ : TopCommRingCat
X : TopCatᵒᵖ
R S : TopCommRingCat
φ : R ⟶ S
x✝² x✝¹ : unop X ⟶ (forget₂ TopCommRingCat TopCat).obj R
x✝ : ↑(unop X)
⊢ (ConcreteCategory.hom ((x✝² + x✝¹) ≫ (forget₂ TopCommRingCat TopCat).map φ)) x✝ =
    (ConcreteCategory.hom (x✝² ≫ (forget₂ TopCommRingCat TopCat).map φ + x✝¹ ≫ (forget₂ TopCommRingCat TopCat).map φ))
      x✝
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
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ (g j * g i) • f j = (g i * g j) • f j

Tactic:
;

Goal state after:
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
i j : ↥U
this : const (f i) (g i) (basicOpen (g i)) ⋯ = (ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op)) s
a : ↥(unop (op (basicOpen (g i * g j))))
⊢ (g j * g i) • f j = (g i * g j) • f j
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 (f * g))

Tactic:
;

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: R : CommRingCat
f g x : ↑R
⊢ (algebraMap (↑R) (Localization.Away (f * g))) x =
    ((IsLocalization.Away.awayToAwayRight f g).comp (algebraMap (↑R) (Localization.Away f))) x

Tactic:
exact (IsLocalization.Away.awayToAwayRight_eq f g x (S := Localization.Away f)).symm

Goal state after:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).inv ≫ pullback.fst f U.ι = (f ⁻¹ᵁ U).ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
⊢ (IsOpenImmersion.isoOfRangeEq (pullback.fst f U.ι) (f ⁻¹ᵁ U).ι ⋯).hom ≫ (f ⁻¹ᵁ U).ι = pullback.fst f U.ι
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ IsIso ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
U : Y.Opens
⊢ IsIso ((pullbackRestrictIsoRestrict f U).inv ≫ pullback.snd f U.ι)
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : (↑U).Opens
⊢ Hom.app (f ∣_ U) V = Hom.app f (U.ι ''ᵁ V) ≫ X.presheaf.map (eqToHom ⋯).op

Tactic:
by
  obtain ⟨V, rfl⟩ : ∃ V', U.ι ⁻¹ᵁ U.ι ''ᵁ V' = V := ⟨_, U.ι.preimage_image_eq V⟩
  simpa [← Functor.map_comp_assoc, ← Functor.map_comp] using!
    congr(Y.presheaf.map (eqToHom (congr_arg (U.ι ''ᵁ ·) (U.ι.preimage_image_eq V).symm)).op ≫
      $(Scheme.Hom.congr_app (morphismRestrict_ι f U) (U.ι ''ᵁ V)))

Goal state after: