awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Subset (α := Set ↥X) (Set.range (ι := ↥(Spec R)) ⇑g) (Set.range (ι := ↥(↑U : Scheme)) ⇑U.ι)

Tactic:
simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx

Premises used: Eq.ge, Set.range_subset_iff
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
rw : IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι
⊢ f = g

Tactic:
rw [← IsOpenImmersion.lift_fac U.ι f (by simpa [Set.range_subset_iff] using fun x hx ↦ hUf.ge hx),
    ← IsOpenImmersion.lift_fac U.ι g (by simpa [Set.range_subset_iff] using fun x hx ↦ hUg.ge hx)]

Premises used: AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.IsOpenImmersion.lift_fac
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
e_a : IsOpenImmersion.lift U.ι f ⋯ = IsOpenImmersion.lift U.ι g ⋯
⊢ IsOpenImmersion.lift U.ι f ⋯ ≫ U.ι = IsOpenImmersion.lift U.ι g ⋯ ≫ U.ι

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
e_a :
  Eq (α := Spec S ⟶ Spec Γ(X, U))
    (Spec.map
      ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ))
    (Spec.map
      ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ))
⊢ IsOpenImmersion.lift U.ι f ⋯ = IsOpenImmersion.lift U.ι g ⋯

Tactic:
rw [← cancel_mono hU.isoSpec.hom, ← Spec.homEquiv.injective.eq_iff,
    ← cancel_mono φ, ← Spec.map_injective.eq_iff]

Premises used: AlgebraicGeometry.IsAffineOpen.isoSpec, AlgebraicGeometry.Spec.map_injective, Function.Injective.eq_iff, AlgebraicGeometry.Spec.homEquiv, CategoryTheory.cancel_mono, Equiv.injective, CategoryTheory.Iso.hom
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
R S : CommRingCat
X : Scheme
φ : R ⟶ S
hφ :
  Function.Injective (α := (↑R : Type u_1)) (β := (↑S : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) φ) :
      (a : (↑R : Type u_1)) → (↑S : Type u_1))
f g : Spec R ⟶ X
U : X.Opens
hU : IsAffineOpen U
hUf : f ⁻¹ᵁ U = ⊤
hUg : g ⁻¹ᵁ U = ⊤
H : Spec.map φ ≫ f = Spec.map φ ≫ g
this : Mono φ
⊢ Eq (α := Spec S ⟶ Spec Γ(X, U))
    (Spec.map
      ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι f ⋯ ≫ hU.isoSpec.hom) ≫ φ))
    (Spec.map
      ((Spec.homEquiv : (a : Spec R ⟶ Spec Γ(X, U)) → Γ(X, U) ⟶ R) (IsOpenImmersion.lift U.ι g ⋯ ≫ hU.isoSpec.hom) ≫ φ))

Tactic:
simp [← cancel_mono U.ι, H]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.Opens.ι
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑X.toSpecΓ) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s

Tactic:
LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq s

Premises used: AlgebraicGeometry.Scheme.zeroLocus, AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
rw :
  Eq (α := Set ↥(Spec Γ(X, ⊤)))
    (Set.image (α := ↥X) (⇑X.isoSpec.hom)
      (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑X.toSpecΓ) (PrimeSpectrum.zeroLocus s)))
    (PrimeSpectrum.zeroLocus s)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.hom '' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)

Tactic:
rw [← X.toSpecΓ_preimage_zeroLocus]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤)))
    (Set.image (α := ↥X) (⇑X.isoSpec.hom)
      (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑X.toSpecΓ) (PrimeSpectrum.zeroLocus s)))
    (PrimeSpectrum.zeroLocus s)

Tactic:
simp [Scheme.isoSpec, Set.image_preimage_eq (h := (bijective_of_isIso _).surjective)]

Premises used: AlgebraicGeometry.Scheme.isoSpec, Set.image_preimage_eq, Function.Bijective.surjective, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (⇑X.toSpecΓ '' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)

Tactic:
X.isoSpec_image_zeroLocus _

Premises used: AlgebraicGeometry.Scheme.isoSpec_image_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
rw :
  Eq (α := Set ↥(Spec Γ(X, ⊤))) (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑(𝟙 (Spec Γ(X, ⊤)))) (PrimeSpectrum.zeroLocus s))
    (PrimeSpectrum.zeroLocus s)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.inv ⁻¹' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)

Tactic:
rw [← toSpecΓ_preimage_zeroLocus, ← Set.preimage_comp, ← TopCat.coe_comp, ← Scheme.Hom.comp_base,
    X.isoSpec_inv_toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.isoSpec_inv_toSpecΓ, AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus, Set.preimage_comp, AlgebraicGeometry.Scheme.Hom.comp_base, TopCat.coe_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Eq (α := Set ↥(Spec Γ(X, ⊤))) (Set.preimage (β := ↥(Spec Γ(X, ⊤))) (⇑(𝟙 (Spec Γ(X, ⊤)))) (PrimeSpectrum.zeroLocus s))
    (PrimeSpectrum.zeroLocus s)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
h : Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥X) ⇑X.isoSpec.inv
⊢ Set.image (α := ↥(Spec Γ(X, ⊤))) (⇑X.isoSpec.inv) (PrimeSpectrum.zeroLocus s) = X.zeroLocus s

Tactic:
rw [← isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq]

Premises used: AlgebraicGeometry.Scheme.isoSpec_inv_preimage_zeroLocus, Set.image_preimage_eq
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥X) ⇑X.isoSpec.inv

Tactic:
(bijective_of_isIso X.isoSpec.inv.base).surjective

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Bijective.surjective, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.inv, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set (↑Γ(X, ⊤) : Type u)
⊢ Function.Surjective (α := ↥(Spec Γ(X, ⊤))) (β := ↥X) ⇑X.isoSpec.inv

Tactic:
exact (bijective_of_isIso X.isoSpec.inv.base).surjective

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Bijective.surjective, AlgebraicGeometry.PresheafedSpace.Hom.base, CategoryTheory.Iso.inv, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
⊢ IsClosed s ↔ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))

Tactic:
⟨fun hs ↦ ?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
refine_1 : ∀ (hs : IsClosed s), ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
refine_2 : (∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))) → IsClosed s
⊢ IsClosed s ↔ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))

Tactic:
refine ⟨fun hs ↦ ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
⊢ IsClosed Z

Tactic:
have hZ : IsClosed Z := (X.isoSpec.hom.homeomorph).isClosedMap _ hs
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
refine_1 :
  ∀ (I : Ideal (↑Γ(X, ⊤) : Type u)) (hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))),
    ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))

Tactic:
obtain ⟨I, (hI : Z = _)⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal _).mp hZ

Premises used: PrimeSpectrum.isClosed_iff_zeroLocus_ideal, Iff.mp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
h : s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ ∃ (I : Ideal (↑Γ(X, ⊤) : Type u)), s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))

Tactic:
use I
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
h : s = ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s
⊢ s = X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))

Tactic:
simp only [← Scheme.toSpecΓ_preimage_zeroLocus, ← hI, Z]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_preimage_zeroLocus
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
h : ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s = s
⊢ s = ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s

Tactic:
symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s = s

Tactic:
Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective

Premises used: AlgebraicGeometry.LocallyRingedSpace.toΓSpecFun, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Bijective.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.preimage_image_eq, PrimeSpectrum.comap, CategoryTheory.Iso.hom, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
s : Set ↥X
hs : IsClosed s
Z : Set ↥(Spec Γ(X, ⊤)) := X.toΓSpecFun '' s
hZ : IsClosed Z
I : Ideal (↑Γ(X, ⊤) : Type u)
hI : Z = PrimeSpectrum.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u))
⊢ ⇑X.toSpecΓ ⁻¹' X.toΓSpecFun '' s = s

Tactic:
exact Set.preimage_image_eq _ (bijective_of_isIso X.isoSpec.hom.base).injective

Premises used: AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Bijective.injective, AlgebraicGeometry.PresheafedSpace.Hom.base, Set.preimage_image_eq, CategoryTheory.Iso.hom, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
I : Ideal (↑Γ(X, ⊤) : Type u)
⊢ IsClosed (X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u)))

Tactic:
zeroLocus_isClosed X I.carrier

Premises used: Submodule.toAddSubmonoid, AddSubsemigroup.carrier, AddSubmonoid.toAddSubsemigroup, AlgebraicGeometry.Scheme.zeroLocus_isClosed
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
inst : IsAffine X
I : Ideal (↑Γ(X, ⊤) : Type u)
⊢ IsClosed (X.zeroLocus (↑I : Set (↑Γ(X, ⊤) : Type u)))

Tactic:
exact zeroLocus_isClosed X I.carrier

Premises used: Submodule.toAddSubmonoid, AddSubsemigroup.carrier, AddSubmonoid.toAddSubsemigroup, AlgebraicGeometry.Scheme.zeroLocus_isClosed
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
dsimp :
  Functor.obj
      (Opens.map (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (↑U : Scheme).toSpecΓ))))
      (PrimeSpectrum.basicOpen
        ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
          r)) =
    U.ι ⁻¹ᵁ X.basicOpen r
⊢ U.toSpecΓ ⁻¹ᵁ PrimeSpectrum.basicOpen r = U.ι ⁻¹ᵁ X.basicOpen r

Tactic:
dsimp [toSpecΓ]

Premises used: AlgebraicGeometry.Scheme.Opens.toSpecΓ
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
simp :
  Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U)) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U) : Type u))
        r))
⊢ Functor.obj
      (Opens.map (PresheafedSpace.Hom.base (LocallyRingedSpace.Hom.toHom (Hom.toLRSHom' (↑U : Scheme).toSpecΓ))))
      (PrimeSpectrum.basicOpen
        ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
              (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
            (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
          r)) =
    U.ι ⁻¹ᵁ X.basicOpen r

Tactic:
simp only [Scheme.toSpecΓ_preimage_basicOpen, preimage_basicOpen, ι_app, homOfLE_leOfHom]

Premises used: CategoryTheory.homOfLE_leOfHom, AlgebraicGeometry.Scheme.Opens.ι_app, AlgebraicGeometry.Scheme.preimage_basicOpen, AlgebraicGeometry.Scheme.toSpecΓ_preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
rw :
  Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := U.ι ⁻¹ᵁ U)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U)) (Y := Γ((↑U : Scheme), U.ι ⁻¹ᵁ U)) (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), U.ι ⁻¹ᵁ U) : Type u))
        r))

Tactic:
rw [← Scheme.basicOpen_res_eq _ _ (eqToHom U.ι_preimage_self.symm).op,
    ← ConcreteCategory.comp_apply]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, Quiver.Hom.op, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.basicOpen_res_eq, AlgebraicGeometry.Scheme.Opens.ι_preimage_self, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
e_f :
  X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))
⊢ Eq.{u + 1} (α := (↑U : Scheme).Opens)
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
            (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))
    ((↑U : Scheme).basicOpen (U := ⊤)
      ((hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier) (X :=
            Γ(X, U))
            (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))) :
          (a : (↑Γ(X, U) : Type u)) → (↑Γ((↑U : Scheme), ⊤) : Type u))
        r))

Tactic:
congr 3
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
e_f :
  Eq (α := Γ(X, U) ⟶ Γ((↑U : Scheme), ⊤)) (X.presheaf.map (eqToHom ⋯))
    (X.presheaf.map
      (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ U)) (Quiver.Hom.op (homOfLE ⋯))
        (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))))
⊢ X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    X.presheaf.map (Quiver.Hom.op (homOfLE ⋯)) ≫ (↑U : Scheme).presheaf.map (Quiver.Hom.op (eqToHom ⋯))

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
r : (↑Γ(X, U) : Type u)
⊢ Eq (α := Γ(X, U) ⟶ Γ((↑U : Scheme), ⊤)) (X.presheaf.map (eqToHom ⋯))
    (X.presheaf.map
      (CategoryStruct.comp (Y := op (U.ι ''ᵁ U.ι ⁻¹ᵁ U)) (Quiver.Hom.op (homOfLE ⋯))
        (Quiver.Hom.op ((Hom.opensFunctor U.ι).map (eqToHom ⋯)))))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
h :
  ∀ (x : ↥(↑U : Scheme)),
    Membership.mem (γ := Set ↥(↑U : Scheme))
        (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s)) x ↔
      Membership.mem (γ := Set ↥(↑U : Scheme)) (U.carrier ↓∩ X.zeroLocus s) x
⊢ Eq (α := Set ↥(↑U : Scheme)) (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s))
    (U.carrier ↓∩ X.zeroLocus s)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥(↑U : Scheme)
⊢ Membership.mem (γ := Set ↥(↑U : Scheme))
      (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s)) x ↔
    Membership.mem (γ := Set ↥(↑U : Scheme)) (U.carrier ↓∩ X.zeroLocus s) x

Tactic:
.trans (forall₂_congr fun y hy ↦ ?_) Set.mem_iInter₂.symm

Premises used: Set.mem_iInter₂, forall₂_congr, Iff.trans, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥(↑U : Scheme)
h :
  ∀ (y : (↑Γ(X, U) : Type u)) (hy : y ∈ s),
    y ∈ (↑(PrimeSpectrum.asIdeal (U.toSpecΓ x)) : Set (↑Γ(X, U) : Type u)) ↔
      (↑x : ↥X) ∈ (↑(X.toRingedSpace.basicOpen y) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ
⊢ Membership.mem (γ := Set ↥(↑U : Scheme))
      (Set.preimage (β := ↥(Spec Γ(X, U))) (⇑U.toSpecΓ) (PrimeSpectrum.zeroLocus s)) x ↔
    Membership.mem (γ := Set ↥(↑U : Scheme)) (U.carrier ↓∩ X.zeroLocus s) x

Tactic:
refine .trans (forall₂_congr fun y hy ↦ ?_) Set.mem_iInter₂.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
s : Set (↑Γ(X, U) : Type u)
x : ↥(↑U : Scheme)
y : (↑Γ(X, U) : Type u)
hy : y ∈ s
⊢ y ∈ (↑(PrimeSpectrum.asIdeal (U.toSpecΓ x)) : Set (↑Γ(X, U) : Type u)) ↔
    (↑x : ↥X) ∈ (↑(X.toRingedSpace.basicOpen y) : Set (↑(↑X.toRingedSpace.toPresheafedSpace : TopCat) : Type u))ᶜ

Tactic:
exact iff_not_comm.mp congr(x ∈ $(Opens.toSpecΓ_preimage_basicOpen U y)).to_iff.symm

Premises used: iff_not_comm, congrArg, Eq.to_iff, Membership.mem, AlgebraicGeometry.Scheme.Opens.toSpecΓ_preimage_basicOpen, id, Iff.mp, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
h :
  ∀ (x : ↥(Spec Γ(X, U))),
    Membership.mem (γ := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) x ↔
      Membership.mem (γ := Set ↥(Spec Γ(X, U))) (PrimeSpectrum.zeroLocus s) x
⊢ Eq (α := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) (PrimeSpectrum.zeroLocus s)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
this : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
⊢ Membership.mem (γ := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) x ↔
    Membership.mem (γ := Set ↥(Spec Γ(X, U))) (PrimeSpectrum.zeroLocus s) x

Tactic:
simpa [← hU.fromSpec_image_basicOpen, -not_not] using this

Premises used: Classical.not_not, AlgebraicGeometry.IsAffineOpen.fromSpec_image_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
h : (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
⊢ Membership.mem (γ := Set ↥(Spec Γ(X, U))) (⇑hU.fromSpec ⁻¹' X.zeroLocus s) x ↔
    Membership.mem (γ := Set ↥(Spec Γ(X, U))) (PrimeSpectrum.zeroLocus s) x

Tactic:
suffices (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ x.asIdeal by
    simpa [← hU.fromSpec_image_basicOpen, -not_not] using this
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
h : (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))
⊢ (∀ f ∈ s, ¬f ∉ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))

Tactic:
simp_rw [not_not]

Premises used: Classical.not_not
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set (↑Γ(X, U) : Type u)
x : ↥(Spec Γ(X, U))
⊢ (∀ f ∈ s, f ∈ x.asIdeal) ↔ s ⊆ (↑x.asIdeal : Set (↑Γ(X, U) : Type u))

Tactic:
rfl