awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : Membership.mem (α := ↥Y) V₂ (f x : ↥Y)
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) V₂ hV₂) : Y.Opens)) : Type u)
s : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V₁' hV₁') : X.Opens)) : Type u)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
heq :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
apply :
  IsStandardSmoothOfRelativeDimension n (R := (↑Γ(Y, V₂) : Type u))
    (CommRingCat.Hom.hom'
      (CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
⊢ IsStandardSmoothOfRelativeDimension (n + m)
    (CommRingCat.Hom.hom
      (Scheme.Hom.appLE g U₂ V₂ e₂ ≫
        CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
          Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))

Tactic:
apply IsStandardSmoothOfRelativeDimension.comp ?_ hf₂

Premises used: RingHom.IsStandardSmoothOfRelativeDimension.comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : Membership.mem (α := ↥Y) V₂ (f x : ↥Y)
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) V₂ hV₂) : Y.Opens)) : Type u)
s : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V₁' hV₁') : X.Opens)) : Type u)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
heq :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
⊢ IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)

Tactic:
haveI : IsLocalization.Away r Γ(Y, Y.basicOpen r) := hV₂.isLocalization_basicOpen r
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : Membership.mem (α := ↥Y) V₂ (f x : ↥Y)
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) V₂ hV₂) : Y.Opens)) : Type u)
s : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V₁' hV₁') : X.Opens)) : Type u)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
heq :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ IsStandardSmoothOfRelativeDimension n (R := (↑Γ(Y, V₂) : Type u))
    (CommRingCat.Hom.hom'
      (CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))

Tactic:
(isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).left
      _ r _ hf₁

Premises used: RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway, And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
U₂ : Z.Opens
hU₂ : IsAffineOpen U₂
V₂ : Y.Opens
hV₂ : IsAffineOpen V₂
hfx₂ : Membership.mem (α := ↥Y) V₂ (f x : ↥Y)
e₂ : V₂ ≤ g ⁻¹ᵁ U₂
hf₂ : IsStandardSmoothOfRelativeDimension m (CommRingCat.Hom.hom (Scheme.Hom.appLE g U₂ V₂ e₂))
U₁' : Y.Opens
hU₁' : IsAffineOpen U₁'
V₁' : X.Opens
hV₁' : IsAffineOpen V₁'
hx₁' : x ∈ V₁'
e₁' : V₁' ≤ f ⁻¹ᵁ U₁'
hf₁' : IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U₁' V₁' e₁'))
r : (↑Γ(Y, (↑(Subtype.mk (p := fun (x : Y.Opens) ↦ x ∈ Y.affineOpens) V₂ hV₂) : Y.Opens)) : Type u)
s : (↑Γ(X, (↑(Subtype.mk (p := fun (x : X.Opens) ↦ x ∈ X.affineOpens) V₁' hV₁') : X.Opens)) : Type u)
hx₁ : x ∈ X.basicOpen s
e₁ : X.basicOpen s ≤ f ⁻¹ᵁ Y.basicOpen r
hf₁ :
  IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))
e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
heq :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
⊢ IsStandardSmoothOfRelativeDimension n (R := (↑Γ(Y, V₂) : Type u))
    (CommRingCat.Hom.hom'
      (CommRingCat.ofHom (algebraMap (↑Γ(Y, V₂) : Type u) (↑Γ(Y, Y.basicOpen r) : Type u)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁))

Tactic:
exact (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).left
      _ r _ hf₁

Premises used: RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway, And.left
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
inst : SmoothOfRelativeDimension 0 f
inst_1 : SmoothOfRelativeDimension 0 g
⊢ SmoothOfRelativeDimension 0 (f ≫ g)

Tactic:
inferInstanceAs <| SmoothOfRelativeDimension (0 + 0) (f ≫ g)

Premises used: _private.0.AlgebraicGeometry.instSmoothOfRelativeDimensionOfNatNatCompScheme._proof_1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ FinitePresentation) f
⊢ LocallyOfFinitePresentation f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation]

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.LocallyOfFinitePresentation
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f

Tactic:
rw [HasRingHomProperty.eq_affineLocally @Smooth] at hf

Premises used: AlgebraicGeometry.HasRingHomProperty.eq_affineLocally, AlgebraicGeometry.Smooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ FinitePresentation) f

Tactic:
affineLocally_le (fun hf ↦ hf.finitePresentation) f hf

Premises used: AlgebraicGeometry.affineLocally_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ FinitePresentation) f

Tactic:
exact affineLocally_le (fun hf ↦ hf.finitePresentation) f hf

Premises used: AlgebraicGeometry.affineLocally_le
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
⊢ q.LiesOver p

Tactic:
have : q.LiesOver p :=
    ⟨congr($(IsAffineOpen.comap_primeIdealOf_appLE U hU V hV hVU hx).1).symm⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
trans :
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q)
trans₁ :
  Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
      (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
      (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
      (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
      (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))

Tactic:
trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)

Premises used: Localization.AtPrime, Algebra.FormallySmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
rw :
  (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    FormallySmooth.{u, u} (R := Localization.AtPrime p) (S := Localization.AtPrime q)
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q)

Tactic:
rw [← formallySmooth_algebraMap]

Premises used: RingHom.formallySmooth_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    FormallySmooth.{u, u} (R := Localization.AtPrime p) (S := Localization.AtPrime q)
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))

Tactic:
RingHom.FormallySmooth.respectsIso.arrow_mk_iso_iff
      (IsAffineOpen.arrowStalkMapIso f U hU V hV hVU hx)

Premises used: IsLocalization.map, Set.Mem, OreLocalization, Localization.localRingHom, setOf, AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso, IsLocalization.lift, Quotient, RingHom.FormallySmooth.respectsIso, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
    FormallySmooth.{u, u} (R := Localization.AtPrime p) (S := Localization.AtPrime q)
      (algebraMap (Localization.AtPrime p) (Localization.AtPrime q))

Tactic:
exact RingHom.FormallySmooth.respectsIso.arrow_mk_iso_iff
      (IsAffineOpen.arrowStalkMapIso f U hU V hV hVU hx)

Premises used: AlgebraicGeometry.IsAffineOpen.arrowStalkMapIso, RingHom.FormallySmooth.respectsIso, RingHom.RespectsIso.arrow_mk_iso_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
      (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
      (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))

Tactic:
Algebra.FormallySmooth.iff_restrictScalars.symm

Premises used: Set.Mem, setOf, Algebra.smoothLocus, Iff.symm, Algebra.FormallySmooth.iff_restrictScalars
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
this_1 : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).toAlgebra
p : Ideal (↑Γ(Y, U) : Type u) := (hU.primeIdealOf (Subtype.mk (p := fun (x : ↥Y) ↦ x ∈ U) (f x) ⋯)).asIdeal
q : Ideal (↑Γ(X, V) : Type u) := (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx)).asIdeal
this_2 : q.LiesOver p
this : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
⊢ Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q) ↔
    Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
      (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
      (hV.primeIdealOf (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hx))

Tactic:
exact Algebra.FormallySmooth.iff_restrictScalars.symm

Premises used: Iff.symm, Algebra.FormallySmooth.iff_restrictScalars
-- 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
obtain :
  ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
    ∃ (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
⊢ ∃ (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:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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)
obtain :
  ∀ (V : TopologicalSpace.Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X))
    (hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier),
    ∃ (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
⊢ ∃ (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:
obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (U.2.preimage f.continuous)

Premises used: AlgebraicGeometry.Scheme.Hom.continuous, TopologicalSpace.Opens.is_open', IsOpen.preimage, AlgebraicGeometry.Scheme.isBasis_affineOpens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- 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
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation

Tactic:
have := f.finitePresentation_appLE hU hV 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 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
⊢ Algebra.FinitePresentation.{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
-- 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 : (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)
⊢ Algebra.IsSmoothAt (↑Γ(Y, U) : Type u)
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)).asIdeal

Tactic:
have : Algebra.IsSmoothAt _ _ := (formallySmooth_stalkMap_iff U hU V hV hVU hxV).mp H
-- 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
obtain :
  ∀ (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
⊢ ∃ (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:
obtain ⟨r, hrx, hr⟩ := Algebra.IsSmoothAt.exists_notMem_smooth Γ(Y, U)
    (hV.primeIdealOf ⟨x, hxV⟩).asIdeal

Premises used: CommRingCat.carrier, Subtype.mk, Algebra.IsSmoothAt.exists_notMem_smooth, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, Opposite.op, AlgebraicGeometry.IsAffineOpen.primeIdealOf, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, PrimeSpectrum.asIdeal, CategoryTheory.Functor.obj, AlgebraicGeometry.Scheme.toLocallyRingedSpace