awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
h : s ⊆ t
⊢ ∀ (x : ↥X), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
fun x H f hf hxf ↦ H f (h hf) hxf

Premises used: Not
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
s t : Set (↑Γ(X, U) : Type u)
h : s ⊆ t
⊢ ∀ (x : ↥X), (∀ f ∈ t, x ∉ X.basicOpen f) → ∀ f ∈ s, x ∉ X.basicOpen f

Tactic:
exact fun x H f hf hxf ↦ H f (h hf) hxf
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set (↑Γ(Y, U) : Type u)
h :
  ∀ (x : ↥X),
    Membership.mem (γ := Set ↥X) (⇑f ⁻¹' Y.zeroLocus s) x ↔
      x ∈
        X.zeroLocus (U := f ⁻¹ᵁ U)
          ((⇑(CommRingCat.Hom.hom (Hom.app f U)) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u)) '' s)
⊢ ⇑f ⁻¹' Y.zeroLocus s =
    X.zeroLocus (U := f ⁻¹ᵁ U)
      ((⇑(CommRingCat.Hom.hom (Hom.app f U)) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u)) '' s)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
s : Set (↑Γ(Y, U) : Type u)
x : ↥X
⊢ Membership.mem (γ := Set ↥X) (⇑f ⁻¹' Y.zeroLocus s) x ↔
    x ∈
      X.zeroLocus (U := f ⁻¹ᵁ U)
        ((⇑(CommRingCat.Hom.hom (Hom.app f U)) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u)) '' s)

Tactic:
simp [← Scheme.preimage_basicOpen]

Premises used: AlgebraicGeometry.Scheme.preimage_basicOpen
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
h : ∀ (x : ↥X), x ∈ X.zeroLocus (U := U) Set.univ ↔ x ∈ (↑U : Set ↥X)ᶜ
⊢ X.zeroLocus (U := U) Set.univ = (↑U : Set ↥X)ᶜ

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
x : ↥X
h : (∃ (x_1 : (↑Γ(X, U) : Type u)), x ∈ X.basicOpen x_1) ↔ x ∈ U
⊢ x ∈ X.zeroLocus (U := U) Set.univ ↔ x ∈ (↑U : Set ↥X)ᶜ

Tactic:
simp only [Scheme.mem_zeroLocus_iff, Set.mem_univ, forall_const, Set.mem_compl_iff,
    SetLike.mem_coe, ← not_exists, not_iff_not]

Premises used: not_iff_not, not_exists, SetLike.mem_coe, Set.mem_univ, forall_const, Set.mem_compl_iff, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
x : ↥X
h rwa rwa₁ rwa₂ rwa₃ : x ∈ U
⊢ x ∈ X.basicOpen (U := U) 1

Tactic:
rwa [X.basicOpen_of_isUnit isUnit_one]

Premises used: AlgebraicGeometry.Scheme.basicOpen_of_isUnit, isUnit_one
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
x : ↥X
⊢ (∃ (x_1 : (↑Γ(X, U) : Type u)), x ∈ X.basicOpen x_1) ↔ x ∈ U

Tactic:
exact ⟨fun ⟨f, hf⟩ ↦ X.basicOpen_le f hf, fun _ ↦ ⟨1, by rwa [X.basicOpen_of_isUnit isUnit_one]⟩⟩
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
ι : Type u_1
f : ι → Set (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (U := U) (⋃ (i : ι), f i) = ⋂ (i : ι), X.zeroLocus (f i)

Tactic:
simpa [zeroLocus, AlgebraicGeometry.RingedSpace.zeroLocus] using Set.iInter_comm _

Premises used: AlgebraicGeometry.RingedSpace.zeroLocus, AlgebraicGeometry.Scheme.zeroLocus, Set.iInter_comm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
⊢ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u)) = X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u))

Tactic:
(X.zeroLocus_mono I.le_radical).antisymm ?_

Premises used: Ideal.le_radical, AlgebraicGeometry.Scheme.zeroLocus_mono, HasSubset.Subset.antisymm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
refine : X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ⊆ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u))
⊢ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u)) = X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u))

Tactic:
refine (X.zeroLocus_mono I.le_radical).antisymm ?_

Premises used: Ideal.le_radical, AlgebraicGeometry.Scheme.zeroLocus_mono, HasSubset.Subset.antisymm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
simp : ∀ (x : ↥X), (∀ f ∈ I, x ∉ X.basicOpen f) → ∀ f ∈ I.radical, x ∉ X.basicOpen f
⊢ X.zeroLocus (↑I : Set (↑Γ(X, U) : Type u)) ⊆ X.zeroLocus (↑I.radical : Set (↑Γ(X, U) : Type u))

Tactic:
simp only [Set.subset_def, mem_zeroLocus_iff, SetLike.mem_coe]

Premises used: Set.subset_def, SetLike.mem_coe, AlgebraicGeometry.Scheme.mem_zeroLocus_iff
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
inl : ∀ (hn : HPow.hPow (β := ℕ) f 0 ∈ I), False
inr : ∀ (hn' : n > 0), False
⊢ False

Tactic:
rcases n.eq_zero_or_pos with rfl | hn'

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
hx : x ∈ X.basicOpen f
hn : HPow.hPow (β := ℕ) f 0 ∈ I
⊢ f ∈ I

Tactic:
simpa using I.mul_mem_left f hn

Premises used: Ideal.mul_mem_left
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
hx : x ∈ X.basicOpen f
hn : HPow.hPow (β := ℕ) f 0 ∈ I
⊢ False

Tactic:
exact H f (by simpa using I.mul_mem_left f hn) hx
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
hn' : n > 0
⊢ False

Tactic:
H _ hn (X.basicOpen_pow f hn' ▸ hx)

Premises used: Eq.rec, AlgebraicGeometry.Scheme.basicOpen_pow, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
I : Ideal (↑Γ(X, U) : Type u)
x : ↥X
H : ∀ f ∈ I, x ∉ X.basicOpen f
f : (↑Γ(X, U) : Type u)
n : ℕ
hn : f ^ n ∈ I
hx : x ∈ X.basicOpen f
hn' : n > 0
⊢ False

Tactic:
exact H _ hn (X.basicOpen_pow f hn' ▸ hx)

Premises used: Eq.rec, AlgebraicGeometry.Scheme.basicOpen_pow, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
h :
  ∀ (x : ↥(Spec R)),
    x ∈
        (↑((Spec R).basicOpen (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))
                f)) :
          Set ↥(Spec R)) ↔
      x ∈ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R))
⊢ Eq.{u_1 + 1} (α := (Spec R).Opens)
    ((Spec R).basicOpen (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))
        f))
    (PrimeSpectrum.basicOpen f)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
h :
  IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
              ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : 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))
              f :
            (↑Γ(Spec R, ⊤) : Type u_1)) :
        (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
    Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x
⊢ x ∈
      (↑((Spec R).basicOpen (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))
              f)) :
        Set ↥(Spec R)) ↔
    x ∈ (↑(PrimeSpectrum.basicOpen f) : Set ↥(Spec R))

Tactic:
simp only [SetLike.mem_coe, Scheme.mem_basicOpen_top]

Premises used: SetLike.mem_coe, AlgebraicGeometry.Scheme.mem_basicOpen_top
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
this :
  IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
    f ∉ x.asIdeal
⊢ IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
              ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : 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))
              f :
            (↑Γ(Spec R, ⊤) : Type u_1)) :
        (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
    Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x

Tactic:
this

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, Not
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
this :
  IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
    f ∉ x.asIdeal
⊢ IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
              ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : 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))
              f :
            (↑Γ(Spec R, ⊤) : Type u_1)) :
        (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
    Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x

Tactic:
exact this
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
h :
  IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
    f ∉ x.asIdeal
⊢ IsUnit (M := (↑((Spec R).presheaf.stalk x) : Type u_1))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (X := (Spec R).presheaf.obj (op ⊤)) (Y := (Spec R).presheaf.stalk x)
              ((Spec R).presheaf.germ ⊤ x _root_.trivial) :
            (a : (↑((Spec R).presheaf.obj (op ⊤)) : Type u_1)) → (↑((Spec R).presheaf.stalk x) : 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))
              f :
            (↑Γ(Spec R, ⊤) : Type u_1)) :
        (↑((Spec R).presheaf.stalk x) : Type u_1)) ↔
    Membership.mem (γ := Opens ↥(Spec R)) (PrimeSpectrum.basicOpen f) x

Tactic:
suffices IsUnit (algebraMap _ ((structurePresheafInCommRingCat ↑R).stalk x) f) ↔
    f ∉ PrimeSpectrum.asIdeal x by exact this
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
h :
  IsUnit (M := Localization.AtPrime x.asIdeal)
      ((algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal) :
            (a : (↑R : Type u_1)) → Localization.AtPrime x.asIdeal)
          f :
        Localization.AtPrime x.asIdeal) ↔
    f ∉ x.asIdeal
⊢ IsUnit (M := (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1))
      ((algebraMap (↑R : Type u_1) (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1) :
            (a : (↑R : Type u_1)) → (↑((structurePresheafInCommRingCat (↑R : Type u_1)).stalk x) : Type u_1))
          f :
        (↑(Presheaf.stalk (structurePresheafInCommRingCat (↑R : Type u_1)) x) : Type u_1)) ↔
    f ∉ x.asIdeal

Tactic:
rw [← isUnit_map_iff (StructureSheaf.stalkIso R x).symm, AlgEquiv.commutes]

Premises used: CommRingCat.carrier, AlgEquiv.symm, AlgEquiv.commutes, AlgebraicGeometry.StructureSheaf.stalkIso, isUnit_map_iff
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
⊢ IsUnit (M := Localization.AtPrime x.asIdeal)
      ((algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal) :
            (a : (↑R : Type u_1)) → Localization.AtPrime x.asIdeal)
          f :
        Localization.AtPrime x.asIdeal) ↔
    f ∉ x.asIdeal

Tactic:
IsLocalization.AtPrime.isUnit_to_map_iff _ (PrimeSpectrum.asIdeal x) f

Premises used: Set.Mem, setOf, IsLocalization.AtPrime.isUnit_to_map_iff, PrimeSpectrum.asIdeal, Not
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑R : Type u_1)
x : ↥(Spec R)
⊢ IsUnit (M := Localization.AtPrime x.asIdeal)
      ((algebraMap (↑R : Type u_1) (Localization.AtPrime x.asIdeal) :
            (a : (↑R : Type u_1)) → Localization.AtPrime x.asIdeal)
          f :
        Localization.AtPrime x.asIdeal) ↔
    f ∉ x.asIdeal

Tactic:
exact IsLocalization.AtPrime.isUnit_to_map_iff _ (PrimeSpectrum.asIdeal x) f

Premises used: IsLocalization.AtPrime.isUnit_to_map_iff, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑Γ(Spec R, ⊤) : Type u_1)
⊢ Eq.{u_1 + 1} (α := (Spec R).Opens)
    ((Spec R).basicOpen (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))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
              CommRingCat.carrier) (Scheme.ΓSpecIso R).hom :
            (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
          f)))
    (PrimeSpectrum.basicOpen
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f))

Tactic:
basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.basicOpen_eq_of_affine, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑Γ(Spec R, ⊤) : Type u_1)
h :
  f =
    (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).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f)
⊢ (Spec R).basicOpen f =
    PrimeSpectrum.basicOpen
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.ΓSpecIso R).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f)

Tactic:
convert! basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.Scheme.ΓSpecIso, AlgebraicGeometry.basicOpen_eq_of_affine, CategoryTheory.Iso.hom, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑Γ(Spec R, ⊤) : Type u_1)
⊢ f =
    (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).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f)

Tactic:
(Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Iso.hom_inv_id_apply, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
R : CommRingCat
f : (↑Γ(Spec R, ⊤) : Type u_1)
⊢ f =
    (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).hom :
          (a : (↑Γ(Spec R, ⊤) : Type u_1)) → (↑R : Type u_1))
        f)

Tactic:
exact (Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

Premises used: AlgebraicGeometry.Scheme.ΓSpecIso, CategoryTheory.Iso.hom_inv_id_apply, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
refl :
  ∀ (W : (Spec Γ(X, U)).Opens),
    Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ⁻¹ᵁ W)
⊢ Γ(Spec Γ(X, V), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom h))) ⁻¹ᵁ W)

Tactic:
cases h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
W : (Spec Γ(X, U)).Opens
⊢ Γ(Spec Γ(X, U), W) = Γ(Spec Γ(X, U), Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯))) ⁻¹ᵁ W)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
rw : Scheme.Spec.map (Quiver.Hom.op (𝟙 Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
rw₁ : Scheme.Spec.map (𝟙 (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
rw₂ rw₃ : 𝟙 (Scheme.Spec.obj (op Γ(X, U))) = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]

Premises used: AlgebraicGeometry.Scheme.Spec, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.Functor.map_id, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace, CategoryTheory.op_id
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
⊢ Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))

Tactic:
have : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 _ := by
    rw [X.presheaf.map_id, op_id, Scheme.Spec.map_id]
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U V : X.Opens
h : U = V
W : (Spec Γ(X, V)).Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
refl : ∀ (W : (Spec Γ(X, U)).Opens), Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) W = eqToHom ⋯
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom h)))) W = eqToHom ⋯

Tactic:
cases h
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) W = eqToHom ⋯

Tactic:
(Scheme.Hom.congr_app this _).trans ?_

Premises used: Eq.mpr, Set.Mem, CategoryTheory.eqToHom, AlgebraicGeometry.Scheme.Hom.congr_app, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
refl :
  Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫
      (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    eqToHom ⋯
⊢ Hom.app (Spec.map (X.presheaf.map (Quiver.Hom.op (eqToHom ⋯)))) W = eqToHom ⋯

Tactic:
refine (Scheme.Hom.congr_app this _).trans ?_

Premises used: AlgebraicGeometry.Scheme.Hom.congr_app, Eq.trans
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : X.Opens
this : Scheme.Spec.map (X.presheaf.map (𝟙 (op U))).op = 𝟙 (Scheme.Spec.obj (op Γ(X, U)))
W : (Spec Γ(X, U)).Opens
⊢ Hom.app (𝟙 (Scheme.Spec.obj (op Γ(X, U)))) W ≫
      (Scheme.Spec.obj (op Γ(X, U))).presheaf.map (Quiver.Hom.op (eqToHom ⋯)) =
    eqToHom ⋯

Tactic:
simp [eqToHom_map]

Premises used: CategoryTheory.eqToHom_map
-- Module: Mathlib.AlgebraicGeometry.Scheme
Goal:
X : Scheme
U : Opens ↥X
x : ↥U
f s : (↑Γ(X, U) : Type u)
hx : (↑x : ↥X) ∈ X.basicOpen s
n : ℕ
hf : s ^ n * f = 0
rw :
  ∀
    (hx :
      IsUnit (M := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
              (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
            s :
          (↑(X.presheaf.stalk (↑x : ↥X)) : Type u)))
    {n : ℕ} (hf : s ^ n * f = 0),
    Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
            (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
          f :
        (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
      (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
⊢ Eq (α := (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk (↑x : ↥X)) (X.presheaf.germ U (↑x : ↥X) ⋯) :
          (a : (↑(X.presheaf.obj (op U)) : Type u)) → (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
        f :
      (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))
    (0 : (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))

Tactic:
rw [Scheme.mem_basicOpen X s x x.2] at hx

Premises used: Subtype.val, Subtype.property, AlgebraicGeometry.Scheme.mem_basicOpen