awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
⊢ ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U),
    x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
⟨_, hU, _, hV.basicOpen r, (X.basicOpen_le r).trans hVU, ?_, ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, AlgebraicGeometry.Scheme.basicOpen_le, And.intro, Exists.intro, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
refine_1 : x ∈ X.basicOpen r
refine_2 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
⊢ ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U),
    x ∈ V ∧ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).Smooth

Tactic:
refine ⟨_, hU, _, hV.basicOpen r, (X.basicOpen_le r).trans hVU, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
⊢ IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)

Tactic:
have := hV.isLocalization_basicOpen r
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))

Tactic:
rw [← RingHom.smooth_algebraMap] at hr

Premises used: RingHom.smooth_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
hr₁ :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
⊢ IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)

Tactic:
rw [← RingHom.smooth_algebraMap] at hr

Premises used: RingHom.smooth_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
⊢ (@fun {R S : Type u} [CommRing R] [CommRing S] ↦ (RingHom.Smooth : (f : R →+* S) → Prop)) (↑Γ(Y, U) : Type u)
    (↑Γ(X, X.basicOpen r) : Type u) _ _
    (@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom
        (AlgEquiv.toRingEquiv
          (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(X, X.basicOpen r) : Type u))))
      (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r)))

Tactic:
RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr

Premises used: CommRingCat.carrier, RingHom.Smooth.propertyIsLocal, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, And.left, Opposite.op, IsLocalization.algEquiv, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgEquiv.toRingEquiv, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, RingHom.PropertyIsLocal.respectsIso, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
h :
  CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) =
    @comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom
        (AlgEquiv.toRingEquiv
          (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(X, X.basicOpen r) : Type u))))
      (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth

Tactic:
convert!
      RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr

Premises used: CommRingCat.carrier, RingHom.Smooth.propertyIsLocal, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, And.left, Opposite.op, IsLocalization.algEquiv, Submonoid.powers, AlgebraicGeometry.Scheme.basicOpen, AlgEquiv.toRingEquiv, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, RingHom.PropertyIsLocal.respectsIso, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
h :
  ∀ (x : (↑Γ(Y, U) : Type u)),
    Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
      ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
          x :
        (↑Γ(X, X.basicOpen r) : Type u))
      ((@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
              (RingEquiv.toRingHom
                (AlgEquiv.toRingEquiv
                  (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(X, X.basicOpen r) : Type u))))
              (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r)) :
            (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
          x :
        (↑Γ(X, X.basicOpen r) : Type u))
⊢ CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) =
    @comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
      (RingEquiv.toRingHom
        (AlgEquiv.toRingEquiv
          (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(X, X.basicOpen r) : Type u))))
      (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
x_1 : (↑Γ(Y, U) : Type u)
h :
  Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))
    ((IsLocalization.map (R := (↑Γ(X, V) : Type u)) (M := Submonoid.powers r) (T := Submonoid.powers r)
            (↑Γ(X, X.basicOpen r) : Type u) (RingHom.id (↑Γ(X, V) : Type u)) ⋯ :
          (a : Localization.Away r) → (↑Γ(X, X.basicOpen r) : Type u))
        ((algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r) : (a : (↑Γ(Y, U) : Type u)) → Localization.Away r) x_1 :
          Localization.Away r) :
      (↑Γ(X, X.basicOpen r) : Type u))
⊢ Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))
    ((@comp _ (Localization.Away r) _ _ Semiring.toNonAssocSemiring _
            (RingEquiv.toRingHom
              (AlgEquiv.toRingEquiv
                (IsLocalization.algEquiv (Submonoid.powers r) (Localization.Away r) (↑Γ(X, X.basicOpen r) : Type u))))
            (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r)) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))

Tactic:
dsimp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
x_1 : (↑Γ(Y, U) : Type u)
h :
  Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))
    ((algebraMap (↑Γ(X, V) : Type u) (↑Γ(X, X.basicOpen r) : Type u) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        ((RingHom.id (↑Γ(X, V) : Type u) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, V) : Type u))
            ((algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                x_1 :
              (↑Γ(X, V) : Type u)) :
          (↑Γ(X, V) : Type u)) :
      (↑Γ(X, X.basicOpen r) : Type u))
⊢ Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))
    ((IsLocalization.map (R := (↑Γ(X, V) : Type u)) (M := Submonoid.powers r) (T := Submonoid.powers r)
            (↑Γ(X, X.basicOpen r) : Type u) (RingHom.id (↑Γ(X, V) : Type u)) ⋯ :
          (a : Localization.Away r) → (↑Γ(X, X.basicOpen r) : Type u))
        ((algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r) : (a : (↑Γ(Y, U) : Type u)) → Localization.Away r) x_1 :
          Localization.Away r) :
      (↑Γ(X, X.basicOpen r) : Type u))

Tactic:
simp only [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]

Premises used: CommRingCat.carrier, IsLocalization.map_eq, Localization, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, IsScalarTower.algebraMap_apply, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
H : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ (↑V : Set ↥X)
hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier
this_1 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) :=
  (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
this_2 :
  Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
r : (↑Γ(X, V) : Type u)
hrx : r ∉ (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal
hr :
  RingHom.Smooth.{u, u} (R := (↑Γ(Y, U) : Type u)) (S := Localization.Away r)
    (algebraMap (↑Γ(Y, U) : Type u) (Localization.Away r))
this : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
x_1 : (↑Γ(Y, U) : Type u)
⊢ Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
    ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯) :
          (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        x_1 :
      (↑Γ(X, X.basicOpen r) : Type u))
    ((algebraMap (↑Γ(X, V) : Type u) (↑Γ(X, X.basicOpen r) : Type u) :
          (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, X.basicOpen r) : Type u))
        ((RingHom.id (↑Γ(X, V) : Type u) : (a : (↑Γ(X, V) : Type u)) → (↑Γ(X, V) : Type u))
            ((algebraMap (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) : (a : (↑Γ(Y, U) : Type u)) → (↑Γ(X, V) : Type u))
                x_1 :
              (↑Γ(X, V) : Type u)) :
          (↑Γ(X, V) : Type u)) :
      (↑Γ(X, X.basicOpen r) : Type u))

Tactic:
simp only [algebraMap_toAlgebra, RingHomCompTriple.comp_apply, ← ConcreteCategory.comp_apply,
      Scheme.Hom.appLE_map]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, RingHomCompTriple.comp_apply, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_map
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}

Tactic:
isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
refine :
  ∀ (x : ↥X) (hx : Membership.mem (γ := Set ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth} x),
    ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}

Tactic:
refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_

Premises used: Iff.mpr, isOpen_iff_forall_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth} x
obtain :
  ∀ (U : Y.Opens) (hU : IsAffineOpen U) (V : X.Opens) (hV : IsAffineOpen V) (hVU : V ≤ f ⁻¹ᵁ U) (hxV : x ∈ V)
    (H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth),
    ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t
⊢ ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t

Tactic:
obtain ⟨U, hU, V, hV, hVU, hxV, H⟩ := exists_smooth_of_formallySmooth_stalk f x hx

Premises used: AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
hx : Membership.mem (γ := Set ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth} x
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hxV : x ∈ V
H : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
⊢ Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)

Tactic:
algebraize [(f.appLE U V hVU).hom]

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.Scheme.Hom.appLE