mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
O : (↑U).Opens
W : (↑V).Opens
e' : W ≤ resLE f U V e ⁻¹ᵁ O
⊢ app f (U.ι ''ᵁ O) ≫ X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) =
    app f (U.ι ''ᵁ O) ≫ X.presheaf.map (homOfLE ⋯).op
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x

Tactic:
]

Goal state after:
C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U U' : Y.Opens
V V' : X.Opens
e : V ≤ f ⁻¹ᵁ U
x : ↥V
⊢ (Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f ↑x) ≫ stalkMap V.ι x =
    (Y.presheaf.stalkCongr ⋯).hom ≫ stalkMap f (V.ι x) ≫ stalkMap V.ι x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
f : (structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)) ⟶ X.presheaf.obj (op (X.toΓSpecMapBasicOpen r))
⊢ CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen r)))) ≫
        f =
      X.toToΓSpecMapBasicOpen r ↔
    f = X.toΓSpecCApp r

Tactic:
by
  have loc_inst := IsLocalization.to_basicOpen (Γ.obj (op X)) r
  refine ConcreteCategory.ext_iff.trans ?_
  rw [← @IsLocalization.Away.lift_comp _ _ _ _ _ _ _ r loc_inst _
      (X.isUnit_res_toΓSpecMapBasicOpen r)]
  constructor
  · intro h
    ext : 1
    exact IsLocalization.ringHom_ext (Submonoid.powers r) h
  apply congr_arg

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
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus (Set.range b), f ∈ x.asIdeal

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
this : PrimeSpectrum.zeroLocus (Set.range b) ⊆ PrimeSpectrum.zeroLocus {f}
⊢ ∀ x ∈ PrimeSpectrum.zeroLocus (Set.range b), f ∈ x.asIdeal
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    (CommRingCat.ofHom
          (algebraMap ↑(Γ.obj (op X)) ↑((structureSheaf ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        X.toΓSpecCApp (unop r)) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
show algebraMap (Γ.obj (op X)) ((structureSheaf (Γ.obj (op X))).obj.obj _) = algebraMap _
      ((structureSheafInType (Γ.obj (op X)) (Γ.obj (op X))).obj.obj _) from rfl,

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        X.toΓSpecCApp (unop r)) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v, u₁} C
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
V : X.Opens
e : V ≤ f ⁻¹ᵁ U
⊢ Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯ = Scheme.Hom.appLE f (U.ι ''ᵁ ⊤) V ⋯

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    X.toToΓSpecMapBasicOpen (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
r s : (InducedCategory (Opens (PrimeSpectrum ↑(Γ.obj (op X)))) basicOpen)ᵒᵖ
f : r ⟶ s
⊢ (CommRingCat.ofHom
          (algebraMap (↑(Γ.obj (op X)))
            ((structureSheafInType ↑(Γ.obj (op X)) ↑(Γ.obj (op X))).obj.obj (op (basicOpen (unop r))))) ≫
        ((inducedFunctor basicOpen).op ⋙ (structureSheaf ↑(Γ.obj (op X))).obj).map f) ≫
      X.toΓSpecCApp (unop s) =
    X.toToΓSpecMapBasicOpen (unop r) ≫
      ((inducedFunctor basicOpen).op ⋙ ((TopCat.Sheaf.pushforward CommRingCat X.toΓSpecBase).obj X.𝒪).obj).map f
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ ⊤

Tactic:
]

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
hn : ∃ c, (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
hn : ∃ c, (c.sum fun i a ↦ a • b i) = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝¹ : IsAffine X
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ f = f

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
h : Scheme.Spec.essImage Y
⊢ Scheme.Spec.essImage X
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f g : X ⟶ Y
e : Scheme.Hom.appTop f = Scheme.Hom.appTop g
⊢ X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g) = X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop g)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    ((pushforward CommRingCat ?m.124).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.124) x) True.intro ≫
      stalkPushforward CommRingCat ?m.124 X.presheaf x

pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

pp: X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.123

Tactic:
]

Goal state after:
X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ (X.toToΓSpecMapBasicOpen 1 ≫
        ((pushforward CommRingCat X.toΓSpecSheafedSpace.hom.base).obj X.presheaf).germ (basicOpen 1)
          ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x) ⋯) ≫
      stalkPushforward CommRingCat X.toΓSpecSheafedSpace.hom.base X.presheaf x =
    ((pushforward CommRingCat ?m.124).obj X.presheaf).germ ⊤ ((ConcreteCategory.hom ?m.124) x) True.intro ≫
      stalkPushforward CommRingCat ?m.124 X.presheaf x

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ TopCat

X : LocallyRingedSpace
x : ↑X.toTopCat
⊢ ↑X.toPresheafedSpace ⟶ ?m.123
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
⊢ ∃ a, (toBasicOpenₗ R M f) a = s
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U

Tactic:
]

Goal state after:
X : Scheme
⊢ ∀ {U : TopologicalSpace.Opens ↥X} {x : ↥X}, x ∈ U → ∃ U' ∈ X.affineOpens, x ∈ U' ∧ U' ≤ U
Module: Mathlib.AlgebraicGeometry.Restrict

Goal state before:
pp: case refine_1
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
⊢ (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY

Tactic:
]

Goal state after:
case refine_1
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
⊢ (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ iY ⁻¹ᵁ UT = (g ⁻¹ᵁ UX).ι ''ᵁ (g ⁻¹ᵁ UX).ι ⁻¹ᵁ UY
Module: Mathlib.AlgebraicGeometry.AffineScheme

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

Tactic:
]

Goal state after:
X : Scheme
⊢ ⋃ i, ↑↑i = ↑⊤
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)

Tactic:
]

Goal state after:
X : Scheme
⊢ IsTopologicalBasis (SetLike.coe '' X.affineOpens)
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r)

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op))
          (const (∑ i, c i • a i) (↑⟨f ^ (n + 1), ⋯⟩) (basicOpen f) ⋯))
      x =
    ↑(const (a i) (b i) (basicOpen (b i)) ⋯) x

Tactic:
]

Goal state after:
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : R
s : (structureSheafInType R M).obj.obj (op (basicOpen f))
ι : Type u
w✝ : Fintype ι
a : ι → M
b : ι → R
ibU : ∀ (i : ι), basicOpen (b i) ≤ basicOpen f
iU : basicOpen f ≤ ⨆ i, basicOpen (b i)
hab : ∀ (i j : ι), b j • a i = b i • a j
H :
  ∀ (i : ι),
    (ConcreteCategory.hom ((structureSheafInType R M).presheaf.map ⋯.hom.op)) s = const (a i) (b i) (basicOpen (b i)) ⋯
n : ℕ
c : ι →₀ R
hc : ∑ i, c i • b i = f ^ (n + 1)
i : ι
x : ↥(unop (op (basicOpen (b i))))
⊢ ↑((ConcreteCategory.hom ((structureSheafInType R M).obj.map ⋯.hom.op))
          (const (∑ i, c i • a i) (↑⟨f ^ (n + 1), ⋯⟩) (basicOpen f) ⋯))
      x =
    ↑(const (a i) (b i) (basicOpen (b i)) ⋯) x
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
      ((ConcreteCategory.hom
          (toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)))
        r))

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x))
      ((ConcreteCategory.hom
          (toStalk (↑(unop (op (Γ.obj (op X))))) ((ConcreteCategory.hom X.toΓSpecSheafedSpace.hom.base) x)))
        r))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) (t * t'))

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) (t * t'))
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.germ U ↑x ⋯)) ((Spec.map (U.stalkIso x).inv) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ (Spec.map (X.presheaf.germ U ↑x ⋯)) ((Spec.map (U.stalkIso x).inv) (closedPoint ↑((↑U).presheaf.stalk x))) =
    (Spec.map (X.presheaf.germ U ↑x ⋯)) (closedPoint ↑(X.presheaf.stalk ↑x))
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t *
      (ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t')

Tactic:
]

Goal state after:
X : LocallyRingedSpace
r✝ : ↑(Γ.obj (op X))
x : ↑X.toTopCat
p : PrimeSpectrum ↑(Γ.obj (op X)) := X.toΓSpecFun x
S : CommRingCat := (structureSheaf ↑(Γ.obj (op X))).presheaf.stalk p
t : ↑S
ht : IsUnit ((CommRingCat.Hom.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t)
r : ↑(Γ.obj (op X))
s : ↥p.asIdeal.primeCompl
t' : ↑S := (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) ↑s
he : t * t' = (algebraMap ↑(X.presheaf.obj (op ⊤)) ↑S) r
⊢ IsUnit
    ((ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t *
      (ConcreteCategory.hom (PresheafedSpace.Hom.stalkMap X.toΓSpecSheafedSpace.hom x)) t')
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' ↑(basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Scheme.Hom.appTop (hU.isoSpec.hom ≫ hU.isoSpec.inv) =
    (U.topIso.hom ≫ (Scheme.ΓSpecIso Γ(X, U)).inv) ≫ (Scheme.ΓSpecIso Γ(X, U)).hom ≫ U.topIso.inv
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
i : ↑(Γ.obj (op X))
x✝ : i ∈ s
⊢ (↑(X.toRingedSpace.basicOpen i))ᶜ = (↑(X.toRingedSpace.basicOpen i))ᶜ

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.GammaSpecAdjunction

Goal state before:
pp: X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ

Tactic:
]

Goal state after:
X : LocallyRingedSpace
s : Set ↑(X.presheaf.obj (op ⊤))
this : ∀ i ∈ s, (↑(X.toRingedSpace.basicOpen i))ᶜ = ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
⊢ ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' zeroLocus s =
    ⋂ i ∈ s, ⇑(ConcreteCategory.hom X.toΓSpec.base) ⁻¹' (basicOpen i).carrierᶜ
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Set.range ⇑(TopCat.Hom.hom U.ι.base) = ↑U

X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Function.Surjective
    (⇑(TopCat.Hom.hom (↑U).isoSpec.inv.base) ∘ ⇑(TopCat.Hom.hom (Spec.map (X.presheaf.map (eqToHom ⋯).op)).base))
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 ⁻¹ᵁ U)

Tactic:
]

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.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
⊢ Epi ((Spec.map (X.presheaf.map (eqToHom ⋯).op)).base ≫ (↑U).isoSpec.inv.base)
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 ≫ U.ι =
    ((IsOpenImmersion.isoOfRangeEq (𝒰.f i ⁻¹ᵁ U).ι (pullback.snd U.ι (𝒰.f ((Equiv.refl 𝒰.I₀) i))) ⋯).hom ≫
        (Precoverage.ZeroHypercover.pullback₁ U.ι 𝒰).f ((Equiv.refl 𝒰.I₀) i)) ≫
      U.ι

Tactic:
]

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

Goal state before:
pp: R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ IsLocalizedModule ⊥ (toOpenₗ R M ⊤) ↔ IsLocalizedModule ⊥ (toOpenₗ R M ⊤)

Tactic:
]

Goal state after: