awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
this_1 : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
this :
  IsLocalization.Away (R := (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r :
      (↑Γ(X, f ⁻¹ᵁ U) : Type u))
    (↑Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)) :
      Type u)
⊢ CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.app f (Y.basicOpen r)) =
    (CommRingCat.Hom.hom (X.presheaf.map (Quiver.Hom.op (homOfLE ⋯) ≫ Quiver.Hom.op (eqToHom ⋯)))).comp
      (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y_1 : Scheme
U_1 : X_1.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X_1, U_1) : Type u)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
⊢ X.basicOpen (U := f ⁻¹ᵁ U)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.app f U) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
        r) =
    f ⁻¹ᵁ Y.basicOpen r

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y_1 : Scheme
U_1 : X_1.Opens
hU_1 : IsAffineOpen U_1
f_1 : (↑Γ(X_1, U_1) : Type u)
X Y : Scheme
f : X ⟶ Y
U : Y.Opens
hU : IsAffineOpen U
h : IsAffineOpen (f ⁻¹ᵁ U)
r : (↑Γ(Y, U) : Type u)
⊢ Eq (α :=
    Γ(Y, Y.basicOpen r) ⟶
      CommRingCat.of
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ U)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.app f U) :
                    (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                  r)) :
          Type u))
    (CommRingCat.ofHom
      (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
        (↑Γ(X,
              X.basicOpen (U := f ⁻¹ᵁ U)
                ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                      CommRingCat.carrier) (Scheme.Hom.app f U) :
                    (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                  r)) :
          Type u)
        (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r))
    (CommRingCat.ofHom
        (IsLocalization.Away.map (↑Γ(Y, Y.basicOpen r) : Type u)
          (↑Γ(X,
                X.basicOpen (U := f ⁻¹ᵁ U)
                  ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                        CommRingCat.carrier) (Scheme.Hom.app f U) :
                      (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
                    r)) :
            Type u)
          (CommRingCat.Hom.hom (Scheme.Hom.app f U)) r) ≫
      𝟙
        Γ(X,
          X.basicOpen (U := f ⁻¹ᵁ U)
            ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Scheme.Hom.app f U) :
                (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, f ⁻¹ᵁ U) : Type u))
              r)))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
V : X.Opens
i : V ⟶ U
e : V = X.basicOpen f
subst : ∀ (i : X.basicOpen f ⟶ U), IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, V) : Type u)

Tactic:
subst e
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
isLocalization_basicOpen hU f

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen, CategoryTheory.homOfLE
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
i : X.basicOpen f ⟶ U
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
exact isLocalization_basicOpen hU f

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X_1 Y : Scheme
U : X_1.Opens
hU : IsAffineOpen U
f : (↑Γ(X_1, U) : Type u)
X : Scheme
inst : IsAffine X
r : (↑Γ(X, ⊤) : Type u)
⊢ IsLocalization.Away r (↑Γ((↑(X.basicOpen r) : Scheme), ⊤) : Type u)

Tactic:
(isAffineOpen_top X).isLocalization_of_eq_basicOpen r _ (Opens.isOpenEmbedding_obj_top _)

Premises used: AlgebraicGeometry.IsAffineOpen.isLocalization_of_eq_basicOpen, AlgebraicGeometry.isAffineOpen_top, Set.Mem, TopologicalSpace.Opens.isOpenEmbedding_obj_top, Set.univ, setOf, Set.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
g : (↑Γ(X, X.basicOpen f) : Type u)
⊢ IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)

Tactic:
have := isLocalization_basicOpen hU f
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
g : (↑Γ(X, X.basicOpen f) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
obtain :
  ∀ (x : (↑Γ(X, U) : Type u)) (n : ℕ),
    ∃ (f' : (↑Γ(X, U) : Type u)),
      X.basicOpen f' =
        X.basicOpen
          (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
            (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                    (a : ↥(Submonoid.powers f)) →
                      ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
                  (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                    Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x)
                    ((fun (x : ℕ) ↦ f ^ x) n) ⋯)) :
              (↑Γ(X, X.basicOpen f) : Type u)))
⊢ ∃ (f' : (↑Γ(X, U) : Type u)), X.basicOpen f' = X.basicOpen g

Tactic:
obtain ⟨x, ⟨_, n, rfl⟩, rfl⟩ := IsLocalization.surj'' (Submonoid.powers f) g

Premises used: IsLocalization.surj'', Submonoid.powers, rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
h :
  X.basicOpen (f * x) =
    X.basicOpen
      (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u)))
⊢ ∃ (f' : (↑Γ(X, U) : Type u)),
    X.basicOpen f' =
      X.basicOpen
        (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
          (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                  (a : ↥(Submonoid.powers f)) →
                    ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
                (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                  Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                  ⋯)) :
            (↑Γ(X, X.basicOpen f) : Type u)))

Tactic:
use f * x
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
h :
  X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen (U := X.basicOpen f)
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u))
⊢ X.basicOpen (f * x) =
    X.basicOpen
      (HSMul.hSMul (β := (↑Γ(X, X.basicOpen f) : Type u)) x
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u)))

Tactic:
rw [Algebra.smul_def, Scheme.basicOpen_mul, Scheme.basicOpen_mul, RingHom.algebraMap_toAlgebra,
    Scheme.basicOpen_res]

Premises used: AlgebraicGeometry.Scheme.basicOpen_mul, AlgebraicGeometry.Scheme.basicOpen_res, Algebra.smul_def, RingHom.algebraMap_toAlgebra
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen (U := X.basicOpen f)
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
(inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm

Premises used: Iff.mpr, LE.le.trans_eq, AlgebraicGeometry.Scheme.basicOpen_of_isUnit, inf_eq_left, inf_le_left, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
h :
  IsUnit.{u} (M := (↑Γ(X, X.basicOpen f) : Type u))
    (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : ↥(Submonoid.powers f)) →
              ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
          (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯)) :
      (↑Γ(X, X.basicOpen f) : Type u))
⊢ X.basicOpen f ⊓ X.basicOpen x =
    X.basicOpen f ⊓ X.basicOpen x ⊓
      X.basicOpen (U := X.basicOpen f)
        (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
                (a : ↥(Submonoid.powers f)) →
                  ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
              (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
                Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n)
                ⋯)) :
          (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
refine (inf_eq_left.mpr (inf_le_left.trans_eq (Scheme.basicOpen_of_isUnit _ ?_).symm)).symm

Premises used: Iff.mpr, LE.le.trans_eq, AlgebraicGeometry.Scheme.basicOpen_of_isUnit, inf_eq_left, inf_le_left, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ IsUnit.{u} (M := (↑Γ(X, X.basicOpen f) : Type u))
    (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : ↥(Submonoid.powers f)) →
              ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
          (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯)) :
      (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
Submonoid.leftInv_le_isUnit _
      (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f))
        _).prop

Premises used: CommRingCat.carrier, Set.Mem, setOf, IsUnit, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Subtype.prop, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, IsLocalization.toInvSubmonoid, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Submonoid.leftInv_le_isUnit, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
f : (↑Γ(X, U) : Type u)
this : IsLocalization.Away f (↑Γ(X, X.basicOpen f) : Type u)
x : (↑Γ(X, U) : Type u)
n : ℕ
⊢ IsUnit.{u} (M := (↑Γ(X, X.basicOpen f) : Type u))
    (↑((IsLocalization.toInvSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u) :
            (a : ↥(Submonoid.powers f)) →
              ↥(IsLocalization.invSubmonoid (Submonoid.powers f) (↑Γ(X, X.basicOpen f) : Type u)))
          (Subtype.mk (p := fun (x : (↑Γ(X, U) : Type u)) ↦
            Membership.mem (γ := Submonoid (↑Γ(X, U) : Type u)) (Submonoid.powers f) x) ((fun (x : ℕ) ↦ f ^ x) n) ⋯)) :
      (↑Γ(X, X.basicOpen f) : Type u))

Tactic:
exact
    Submonoid.leftInv_le_isUnit _
      (IsLocalization.toInvSubmonoid (Submonoid.powers f) (Γ(X, X.basicOpen f))
        _).prop

Premises used: CommRingCat.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, Subtype.prop, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgebraicGeometry.PresheafedSpace.presheaf, IsLocalization.toInvSubmonoid, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, Submonoid.leftInv_le_isUnit, DFunLike.coe, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
obtain :
  ∀ (f : (↑Γ(X, U) : Type u)) (hf₁ : X.basicOpen f ≤ V)
    (hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f),
    ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := hU.exists_basicOpen_le ⟨x, hx.2⟩ hx.1

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, And.right, And.left
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
obtain :
  ∀ (g : (↑Γ(X, V) : Type u)) (hg₁ : X.basicOpen g ≤ X.basicOpen f)
    (hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g),
    ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨g, hg₁, hg₂⟩ := hV.exists_basicOpen_le ⟨x, hf₂⟩ hx.2

Premises used: Subtype.mk, AlgebraicGeometry.IsAffineOpen.exists_basicOpen_le, And.right
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
obtain :
  ∀ (f' : (↑Γ(X, U) : Type u))
    (hf' :
      X.basicOpen f' =
        X.basicOpen (U := X.basicOpen f)
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                CommRingCat.carrier) (X.presheaf.map (homOfLE hf₁).op) :
              (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
            g)),
    ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
obtain ⟨f', hf'⟩ :=
    basicOpen_basicOpen_is_basicOpen hU f (X.presheaf.map (homOfLE hf₁ : _ ⟶ V).op g)

Premises used: CategoryTheory.ConcreteCategory.hom, Quiver.Hom.op, CategoryTheory.Functor.map, AlgebraicGeometry.IsAffineOpen.basicOpen_basicOpen_is_basicOpen, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, CategoryTheory.homOfLE, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
f' : (↑Γ(X, U) : Type u)
hf' :
  X.basicOpen f' =
    X.basicOpen (U := X.basicOpen f)
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (X.presheaf.map (homOfLE hf₁).op) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen f) : Type u))
        g)
⊢ X.basicOpen f' = X.toRingedSpace.basicOpen g

Tactic:
replace hf' := (hf'.trans (RingedSpace.basicOpen_res _ _ _)).trans (inf_eq_right.mpr hg₁)
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
f' : (↑Γ(X, U) : Type u)
hf' : X.basicOpen f' = X.toRingedSpace.basicOpen g
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
⟨f', g, hf', hf'.symm ▸ hg₂⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
x : ↥X
hx : x ∈ U ⊓ V
f : (↑Γ(X, U) : Type u)
hf₁ : X.basicOpen f ≤ V
hf₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x ⋯) : ↥X) ∈ X.basicOpen f
g : (↑Γ(X, V) : Type u)
hg₁ : X.basicOpen g ≤ X.basicOpen f
hg₂ : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ X.basicOpen f) x hf₂) : ↥X) ∈ X.basicOpen g
f' : (↑Γ(X, U) : Type u)
hf' : X.basicOpen f' = X.toRingedSpace.basicOpen g
⊢ ∃ (f : (↑Γ(X, U) : Type u)) (g : (↑Γ(X, V) : Type u)), X.basicOpen f = X.basicOpen g ∧ x ∈ X.basicOpen f

Tactic:
exact ⟨f', g, hf', hf'.symm ▸ hg₂⟩
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
rw : U.ι x = (↑x : ↥X)
⊢ (hU.isoSpec.inv ≫ U.ι) (hU.isoSpec.hom x : ↥(Spec Γ(X, U))) = (↑x : ↥X)

Tactic:
rw [← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, CategoryTheory.Iso.hom_inv_id_assoc
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ U.ι x = (↑x : ↥X)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
⊢ hU.primeIdealOf x = (Spec.map (X.presheaf.germ U (↑x : ↥X) ⋯)) (closedPoint (↑(X.presheaf.stalk (↑x : ↥X)) : Type u))

Tactic:
hU.isoSpec_hom_apply _

Premises used: AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom_apply
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
simp :
  Eq (α := ↥(Spec Γ(Y, U)))
    ((Scheme.Hom.resLE f U V hVU ≫ U.toSpecΓ) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(Spec Γ(Y, U)))
    (U.toSpecΓ (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥(Spec Γ(Y, U)))
⊢ (Spec.map (Scheme.Hom.appLE f U V hVU)) (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) =
    hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)

Tactic:
simp only [IsAffineOpen.primeIdealOf, ← Scheme.Hom.comp_apply, IsAffineOpen.isoSpec_hom,
    Scheme.Opens.toSpecΓ_SpecMap_appLE]

Premises used: AlgebraicGeometry.Scheme.Hom.comp_apply, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.Scheme.Opens.toSpecΓ_SpecMap_appLE
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
h :
  Eq (α := ↥(↑U : Scheme)) ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(↑U : Scheme))
    (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯ : ↥U)
⊢ Eq (α := ↥(Spec Γ(Y, U)))
    (U.toSpecΓ ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) : ↥(Spec Γ(Y, U)))
    (U.toSpecΓ (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥(Spec Γ(Y, U)))

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
h :
  Eq (α := ↥Y) ((↑((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) : ↥Y) : ↥Y)
    ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y) : ↥Y)
⊢ Eq (α := ↥(↑U : Scheme)) ((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx) : ↥(↑U : Scheme))
    (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯ : ↥U)

Tactic:
apply Subtype.ext

Premises used: Subtype.ext
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
⊢ Eq (α := ↥Y) ((↑((Scheme.Hom.resLE f U V hVU) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)) : ↥Y) : ↥Y)
    ((↑(Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯) : ↥Y) : ↥Y)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
⊢ IsClosed (X := ↥U) {x}

Tactic:
simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective]
      using hx.preimage U.isOpenEmbedding'.continuous

Premises used: Set.image_singleton, Subtype.val_injective, TopologicalSpace.Opens.isOpenEmbedding', Topology.IsOpenEmbedding.continuous, Set.preimage_image_eq, IsClosed.preimage
-- Module: Mathlib.AlgebraicGeometry.AffineScheme
Goal:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
x : ↥U
hx : IsClosed (X := ↥X) {(↑x : ↥X)}
⊢ IsClosed (X := ↥U) {x}

Tactic:
have hx₀ : IsClosed {x} := by
    simpa [← Set.image_singleton, Set.preimage_image_eq _ Subtype.val_injective]
      using hx.preimage U.isOpenEmbedding'.continuous