awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ Eq (α := ↥Y) ((e.inv ≫ e.hom) y : ↥Y)
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
            (PresheafedSpace.Hom.base (𝟙 Y.toPresheafedSpace)) :
          (a : ↥Y) → ↥Y)
        y :
      ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
h :
  ∀ (x : ↥(Spec R)),
    Membership.mem (γ := Set ↥(Spec R))
        ((Spec R).zeroLocus (U := ⊤)
          ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                  CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
              (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
            s))
        x ↔
      Membership.mem (γ := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus s) x
⊢ Eq (α := Set ↥(Spec R))
    ((Spec R).zeroLocus (U := ⊤)
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
        s))
    (PrimeSpectrum.zeroLocus s)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
x : ↥(Spec R)
this :
  (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑R : Type u_1))) (PrimeSpectrum.zeroLocus s) x
⊢ Membership.mem (γ := Set ↥(Spec R))
      ((Spec R).zeroLocus (U := ⊤)
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
            (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
          s))
      x ↔
    Membership.mem (γ := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus s) x

Tactic:
simpa
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
x : ↥(Spec R)
h :
  (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑R : Type u_1))) (PrimeSpectrum.zeroLocus s) x
⊢ Membership.mem (γ := Set ↥(Spec R))
      ((Spec R).zeroLocus (U := ⊤)
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
            (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ''
          s))
      x ↔
    Membership.mem (γ := Set ↥(Spec R)) (PrimeSpectrum.zeroLocus s) x

Tactic:
suffices (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔ x ∈ PrimeSpectrum.zeroLocus s by simpa
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑R : Type u_1)
x : ↥(Spec R)
⊢ (∀ a ∈ s, x ∉ PrimeSpectrum.basicOpen a) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑R : Type u_1))) (PrimeSpectrum.zeroLocus s) x

Tactic:
simp [Spec_carrier, PrimeSpectrum.mem_zeroLocus, Set.subset_def,
    PrimeSpectrum.mem_basicOpen _ x]

Premises used: Set.subset_def, PrimeSpectrum.mem_zeroLocus, AlgebraicGeometry.Spec_carrier, PrimeSpectrum.mem_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
⊢ Eq (α := Set ↥(Spec R))
    ((Spec R).zeroLocus (U := ⊤)
      (Set.image (α := (↑R : Type u_1))
        (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
        ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
                CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
            (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
          s)))
    (PrimeSpectrum.zeroLocus
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s))

Tactic:
Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, Set.preimage, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
h :
  s =
    Set.image (α := (↑R : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
        (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s)
⊢ (Spec R).zeroLocus s =
    PrimeSpectrum.zeroLocus
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s)

Tactic:
convert! Spec_zeroLocus_eq_zeroLocus ((Scheme.ΓSpecIso R).inv ⁻¹' s)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.Spec_zeroLocus_eq_zeroLocus, Set.preimage, DFunLike.coe, CategoryTheory.Iso.inv
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
h :
  Function.Surjective (α := (↑R : Type u_1)) (β := (↑Γ(Spec R, ⊤) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
      (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
⊢ s =
    Set.image (α := (↑R : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
        (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))
      ((⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
          (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1)) ⁻¹'
        s)

Tactic:
rw [Set.image_preimage_eq]

Premises used: Set.image_preimage_eq
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
⊢ Function.Surjective (α := (↑R : Type u_1)) (β := (↑Γ(Spec R, ⊤) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
      (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))

Tactic:
(ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2

Premises used: And.right, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
s : Set (↑Γ(Spec R, ⊤) : Type u_1)
⊢ Function.Surjective (α := (↑R : Type u_1)) (β := (↑Γ(Spec R, ⊤) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.ΓSpecIso R).inv) :
      (a : (↑R : Type u_1)) → (↑Γ(Spec R, ⊤) : Type u_1))

Tactic:
exact (ConcreteCategory.bijective_of_isIso (C := CommRingCat) _).2

Premises used: And.right, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ IsLocalHom (R := (↑(Y.presheaf.stalk (f x)) : Type u)) (S := (↑(X.presheaf.stalk x) : Type u))
    (CommRingCat.Hom.hom (stalkMap f x))

Tactic:
f.prop x

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.LocallyRingedSpace.Hom.prop
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
x : ↥X
⊢ stalkMap (𝟙 X) x = 𝟙 (X.presheaf.stalk x)

Tactic:
PresheafedSpace.stalkMap.id _ x

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.id, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
x : ↥X
⊢ stalkMap (f ≫ g) x = stalkMap g (f x) ≫ stalkMap f x

Tactic:
PresheafedSpace.stalkMap.comp f.toPshHom g.toPshHom x

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.toPshHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.stalkMap.comp, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.LocallyRingedSpace.Hom.stalkMap
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x x' : ↥X
h : x ⤳ x'
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f x = stalkMap f x' ≫ X.presheaf.stalkSpecializes h

Tactic:
PresheafedSpace.stalkMap.stalkSpecializes_stalkMap f.toPshHom h

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap, AlgebraicGeometry.PresheafedSpace.Hom.toPshHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom'
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x x' : ↥X
h : x ⤳ x'
y : (↑(Y.presheaf.stalk ((Hom.hom f.base : (a : ↥X) → ↥Y) x')) : Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (stalkMap f x) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Y.presheaf.stalk ((Hom.hom f.base : (a : ↥X) → ↥Y) x'))
                (Y.presheaf.stalkSpecializes ⋯) :
              (a : (↑(Y.presheaf.stalk ((Hom.hom f.base : (a : ↥X) → ↥Y) x')) : Type u)) →
                (↑(Y.presheaf.stalk ((Hom.hom f.base : (a : ↥X) → ↥Y) x)) : Type u))
            y :
          (↑(Y.presheaf.stalk ((Hom.hom f.base : (a : ↥X) → ↥Y) x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.stalk x') (X.presheaf.stalkSpecializes h) :
          (a : (↑(X.presheaf.stalk x') : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (stalkMap f x') :
              (a : (↑(Y.presheaf.stalk (f x')) : Type u)) → (↑(X.presheaf.stalk x') : Type u))
            y :
          (↑(X.presheaf.stalk x') : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkSpecializes_stalkMap f x x' h)) y

Premises used: DFunLike.congr_fun, AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap, CommRingCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
hfg : f = g
x x' : ↥X
hxx' : x = x'
⊢ stalkMap f x ≫ Iso.hom (X.presheaf.stalkCongr ⋯) = Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ stalkMap g x'

Tactic:
LocallyRingedSpace.stalkMap_congr f.toLRSHom g.toLRSHom congr(($hfg).toLRSHom) x x' hxx'

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, congrArg, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr, id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f g : X ⟶ Y
hfg : f = g
x : ↥X
⊢ stalkMap f x = Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ stalkMap g x

Tactic:
LocallyRingedSpace.stalkMap_congr_hom f.toLRSHom g.toLRSHom congr(($hfg).toLRSHom) x

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, congrArg, id, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_hom
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x x' : ↥X
hxx' : x = x'
⊢ stalkMap f x ≫ Iso.hom (X.presheaf.stalkCongr ⋯) = Iso.hom (Y.presheaf.stalkCongr ⋯) ≫ stalkMap f x'

Tactic:
LocallyRingedSpace.stalkMap_congr_point f.toLRSHom x x' hxx'

Premises used: AlgebraicGeometry.Scheme.Hom.toLRSHom, AlgebraicGeometry.LocallyRingedSpace.stalkMap_congr_point
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
⊢ e.hom (e.inv y : ↥X) = y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
y : ↥Y
⊢ stalkMap e.hom (e.inv y) ≫ stalkMap e.inv y = Iso.hom (Y.presheaf.stalkCongr ⋯)

Tactic:
LocallyRingedSpace.stalkMap_hom_inv (forgetToLocallyRingedSpace.mapIso e) y

Premises used: Set.Mem, TopCat.Presheaf.stalkSpecializes, AlgebraicGeometry.LocallyRingedSpace.stalkMap_hom_inv, CategoryTheory.Limits.colimit.desc, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
y : ↥Y
z : (↑(Y.presheaf.stalk (e.hom (e.inv y : ↥X))) : Type u)
⊢ e.hom (e.inv y : ↥X) = y

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
y : ↥Y
z : (↑(Y.presheaf.stalk (e.hom (e.inv y : ↥X))) : Type u)
⊢ Eq (α := (↑(Y.presheaf.stalk y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (stalkMap e.inv y) :
          (a : (↑(X.presheaf.stalk (e.inv y)) : Type u)) → (↑(Y.presheaf.stalk y) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := Y.presheaf.stalk (e.hom (e.inv y : ↥X))) (stalkMap e.hom (e.inv y)) :
              (a : (↑(Y.presheaf.stalk (e.hom (e.inv y))) : Type u)) → (↑(X.presheaf.stalk (e.inv y)) : Type u))
            z :
          (↑(X.presheaf.stalk (e.inv y)) : Type u)) :
      (↑(Y.presheaf.stalk y) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := Y.presheaf.stalk (e.hom (e.inv y : ↥X))) (Iso.hom (Y.presheaf.stalkCongr ⋯)) :
          (a : (↑(Y.presheaf.stalk (e.hom (e.inv y))) : Type u)) → (↑(Y.presheaf.stalk y) : Type u))
        z :
      (↑(Y.presheaf.stalk y) : Type u))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_hom_inv e y)) z

Premises used: DFunLike.congr_fun, AlgebraicGeometry.Scheme.Hom.stalkMap_hom_inv, CommRingCat.hom_ext_iff, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
⊢ e.inv (e.hom x : ↥Y) = x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
⊢ stalkMap e.inv (e.hom x) ≫ stalkMap e.hom x = Iso.hom (X.presheaf.stalkCongr ⋯)

Tactic:
LocallyRingedSpace.stalkMap_inv_hom (forgetToLocallyRingedSpace.mapIso e) x

Premises used: Set.Mem, AlgebraicGeometry.LocallyRingedSpace.stalkMap_inv_hom, TopCat.Presheaf.stalkSpecializes, CategoryTheory.Limits.colimit.desc, AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace, CategoryTheory.Functor.mapIso
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
e : X ≅ Y
x : ↥X
y : (↑(X.presheaf.stalk (e.inv (e.hom x : ↥Y))) : Type u)
⊢ e.inv (e.hom x : ↥Y) = x

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
e : X ≅ Y
x : ↥X
y : (↑(X.presheaf.stalk (e.inv (e.hom x : ↥Y))) : Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (stalkMap e.hom x) :
          (a : (↑(Y.presheaf.stalk (e.hom x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X := X.presheaf.stalk (e.inv (e.hom x : ↥Y))) (stalkMap e.inv (e.hom x)) :
              (a : (↑(X.presheaf.stalk (e.inv (e.hom x))) : Type u)) → (↑(Y.presheaf.stalk (e.hom x)) : Type u))
            y :
          (↑(Y.presheaf.stalk (e.hom x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.stalk (e.inv (e.hom x : ↥Y))) (Iso.hom (X.presheaf.stalkCongr ⋯)) :
          (a : (↑(X.presheaf.stalk (e.inv (e.hom x))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        y :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
DFunLike.congr_fun (CommRingCat.hom_ext_iff.mp (stalkMap_inv_hom e x)) y

Premises used: DFunLike.congr_fun, CommRingCat.hom_ext_iff, Iff.mp, AlgebraicGeometry.Scheme.Hom.stalkMap_inv_hom
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
x : ↥X
hx : Membership.mem (α := ↥Y) U (f x : ↥Y)
⊢ Y.presheaf.germ U (f x) hx ≫ stalkMap f x = app f U ≫ X.presheaf.germ (f ⁻¹ᵁ U) x hx

Tactic:
PresheafedSpace.stalkMap_germ f.toPshHom U x hx

Premises used: AlgebraicGeometry.PresheafedSpace.stalkMap_germ, AlgebraicGeometry.PresheafedSpace.Hom.toPshHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom'
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
x : ↥X
hx : Membership.mem (α := ↥Y) U (f x : ↥Y)
y : (↑(Y.presheaf.obj (op U)) : Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (stalkMap f x) :
          (a : (↑(Y.presheaf.stalk (f x)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := Y.presheaf.stalk (f x)) (Y.presheaf.germ U (f x) hx) :
              (a : (↑(Y.presheaf.obj (op U)) : Type u)) → (↑(Y.presheaf.stalk (f x)) : Type u))
            y :
          (↑(Y.presheaf.stalk (f x)) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X := X.presheaf.obj (op (f ⁻¹ᵁ U))) (Y := X.presheaf.stalk x)
            (X.presheaf.germ (f ⁻¹ᵁ U) x hx) :
          (a : (↑(X.presheaf.obj (op (f ⁻¹ᵁ U))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (app f U) :
              (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
            y :
          (↑Γ(X, f ⁻¹ᵁ U) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
PresheafedSpace.stalkMap_germ_apply f.toPshHom U x hx y

Premises used: AlgebraicGeometry.PresheafedSpace.Hom.toPshHom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.stalkMap_germ_apply
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
rw : stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
h₁ : y ⤳ x
rw₁ : stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯
h₂ : y ⤳ x
⊢ Y.presheaf.stalkSpecializes ⋯ ≫ stalkMap f y = stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯

Tactic:
rw [stalkSpecializes_stalkMap]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkSpecializes_stalkMap
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R S : CommRingCat
inst : IsLocalRing.{u_1} (↑R : Type u_1)
inst_1 : IsLocalRing.{u_1} (↑S : Type u_1)
f : R ⟶ S
inst_2 : IsLocalHom (R := (↑R : Type u_1)) (S := (↑S : Type u_1)) (CommRingCat.Hom.hom f)
⊢ Eq (α := ↥(Spec R)) ((Spec.map f) (closedPoint (↑S : Type u_1)) : ↥(Spec R))
    (closedPoint (↑R : Type u_1) : PrimeSpectrum (↑R : Type u_1))

Tactic:
IsLocalRing.comap_closedPoint f.hom

Premises used: CommRingCat.Hom.hom, IsLocalRing.comap_closedPoint, PrimeSpectrum.comap
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
rw :
  ∃ (𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
    ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
    𝒰.toPresieveOverProp (P := P) (Q := P) h ≤
      (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows
⊢ Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U ∈
    (smallGrothendieckTopology P : (a : P.Over ⊤ S) → Set (Sieve a)) U

Tactic:
rw [Scheme.mem_smallGrothendieckTopology]

Premises used: AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  Cover.changeProp (Q := P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineCover ⋯
x : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
x_1 : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
⊢ ∃ (𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
    ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
    𝒰.toPresieveOverProp (P := P) (Q := P) h ≤
      (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows

Tactic:
⟨𝒰, inferInstance,
      fun i ↦ P.comp_mem _ _ (𝒰.map_prop i) U.prop, fun X f ⟨i⟩ ↦ ?_⟩

Premises used: CategoryTheory.PreZeroHypercover.f, CategoryTheory.MorphismProperty.CostructuredArrow.toOver, inferInstance, CategoryTheory.Comma.hom, CategoryTheory.Sieve.arrows, AlgebraicGeometry.Scheme.Spec, CategoryTheory.MorphismProperty.comp_mem, CategoryTheory.MorphismProperty.Comma.toComma, CategoryTheory.MorphismProperty.Comma.prop, CategoryTheory.Sieve.coverByImage, Exists.intro, AlgebraicGeometry.Scheme.Cover.map_prop, _private.0.AlgebraicGeometry.Scheme.isCoverDense_toOver_Spec.match_1, CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover
-- Module: Mathlib.AlgebraicGeometry.Sites.Affine
Goal:
S : Scheme
P : MorphismProperty Scheme
inst : P.IsMultiplicative
inst_1 : IsZariskiLocalAtSource P
inst_2 : P.IsStableUnderBaseChange
inst_3 : P.HasOfPostcompProperty P
U : P.Over ⊤ S
𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left :=
  Cover.changeProp (Q := P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left.affineCover ⋯
x : (i : 𝒰.I₀) → (𝒰.X i).Over S := fun (i : 𝒰.I₀) ↦ { hom := 𝒰.f i ≫ U.toComma (P := P) (Q := ⊤) (W := ⊤).hom }
x_1 : Cover.Over S (P := P) 𝒰 := Cover.Over.mk (P := P) inferInstance ⋯
refine :
  ∀ (X : P.Over ⊤ S) (f : X ⟶ U),
    𝒰.toPresieveOverProp (P := P) (Q := P) ⋯ f →
      ∀ (i : 𝒰.I₀),
        (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows (Y :=
          (𝒰.X i).asOverProp (P := P) S ⋯) (Hom.asOverProp (P := P) (𝒰.f i) S)
⊢ ∃ (𝒰 : Cover (precoverage P) U.toComma (P := P) (Q := ⊤) (W := ⊤).left) (x : Cover.Over S (P := P) 𝒰) (h :
    ∀ (j : 𝒰.I₀), P (𝒰.X j ↘ S)),
    𝒰.toPresieveOverProp (P := P) (Q := P) h ≤
      (Sieve.coverByImage (MorphismProperty.CostructuredArrow.toOver P Scheme.Spec S) U).arrows

Tactic:
refine ⟨𝒰, inferInstance,
      fun i ↦ P.comp_mem _ _ (𝒰.map_prop i) U.prop, fun X f ⟨i⟩ ↦ ?_⟩