awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
⊢ ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t

Tactic:
⟨V, fun y hy ↦ (formallySmooth_stalkMap_iff U hU V hV hVU hy).mpr
    (inferInstanceAs (Algebra.IsSmoothAt _ _)), V.2, hxV⟩

Premises used: Iff.mpr, AlgebraicGeometry.formallySmooth_stalkMap_iff, Subtype.mk, SetLike.coe, Algebra.FormallySmooth.instLocalization, And.intro, Exists.intro, AlgebraicGeometry.IsAffineOpen.primeIdealOf, Ideal.primeCompl, TopologicalSpace.Opens.is_open', PrimeSpectrum.asIdeal
-- 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
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
⊢ ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t

Tactic:
exact ⟨V, fun y hy ↦ (formallySmooth_stalkMap_iff U hU V hV hVU hy).mpr
    (inferInstanceAs (Algebra.IsSmoothAt _ _)), V.2, hxV⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
x : ↥X
⊢ x ∈ smoothLocus f ↔ (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, RingHom.FormallySmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
rw : ⊤ ≤ smoothLocus f
⊢ smoothLocus f = ⊤

Tactic:
rw [← top_le_iff]

Premises used: top_le_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
obtain :
  ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
    x ∈ smoothLocus f
⊢ x ∈ smoothLocus f

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 : Smooth f
x : ↥X
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), x ∈ smoothLocus f
⊢ x ∈ smoothLocus f

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 : Smooth f
x : ↥X
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 (appLE f U V hVU)).Smooth

Tactic:
have := f.smooth_appLE hU hV hVU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
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 (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
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
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 (appLE f U V hVU)).Smooth
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
rw :
  Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
    (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV))
⊢ x ∈ smoothLocus f

Tactic:
rw [Scheme.Hom.mem_smoothLocus, formallySmooth_stalkMap_iff U hU V hV hVU hxV]

Premises used: AlgebraicGeometry.formallySmooth_stalkMap_iff, AlgebraicGeometry.Scheme.Hom.mem_smoothLocus
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
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 (appLE f U V hVU)).Smooth
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
⊢ Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
    (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV))

Tactic:
inferInstanceAs (Algebra.IsSmoothAt _ _)

Premises used: Set.Mem, setOf, Subtype.mk, Algebra.FormallySmooth.instLocalization, Algebra.smoothLocus, AlgebraicGeometry.IsAffineOpen.primeIdealOf, Ideal.primeCompl, PrimeSpectrum.asIdeal
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
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 (appLE f U V hVU)).Smooth
algInst : Algebra (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u) := (CommRingCat.Hom.hom (appLE f U V hVU)).toAlgebra
algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
⊢ Membership.mem (γ := Set (PrimeSpectrum (↑Γ(X, V) : Type u)))
    (Algebra.smoothLocus (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u))
    (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV))

Tactic:
exact inferInstanceAs (Algebra.IsSmoothAt _ _)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
⊢ smoothLocus f = ⊤ ↔ Smooth f

Tactic:
⟨fun H ↦ ?_, fun _ ↦ f.smoothLocus_eq_top⟩

Premises used: Iff.intro, AlgebraicGeometry.Scheme.Hom.smoothLocus_eq_top
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
refine : ∀ (H : smoothLocus f = ⊤), Smooth f
⊢ smoothLocus f = ⊤ ↔ Smooth f

Tactic:
refine ⟨fun H ↦ ?_, fun _ ↦ f.smoothLocus_eq_top⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H : smoothLocus f = ⊤
⊢ Smooth f

Tactic:
IsZariskiLocalAtSource.iff_exists_resLE.mpr fun x ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H : smoothLocus f = ⊤
refine : ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)
⊢ Smooth f

Tactic:
refine IsZariskiLocalAtSource.iff_exists_resLE.mpr fun x ↦ ?_

Premises used: Iff.mpr, AlgebraicGeometry.IsZariskiLocalAtSource.iff_exists_resLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H : smoothLocus f = ⊤
x : ↥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),
    ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)

Tactic:
obtain ⟨U, hU, V, hV, hVU, hxV, H⟩ :=
    exists_smooth_of_formallySmooth_stalk f _ (H.ge (Set.mem_univ x))

Premises used: Eq.ge, AlgebraicGeometry.exists_smooth_of_formallySmooth_stalk, Set.mem_univ
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)

Tactic:
⟨U, V, hxV, hVU, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
refine : Smooth (resLE f U V hVU)
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)

Tactic:
refine ⟨U, V, hxV, hVU, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
⊢ IsAffine.{u} (↑U : Scheme)

Tactic:
have : IsAffine _ := hU
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
this : IsAffine.{u} (↑U : Scheme)
⊢ IsAffine.{u} (↑V : Scheme)

Tactic:
have : IsAffine _ := hV
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
rw : (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth
⊢ Smooth (resLE f U V hVU)

Tactic:
rw [HasRingHomProperty.iff_of_isAffine (P := @Smooth)]

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_of_isAffine
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
⊢ (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth

Tactic:
(RingHom.Smooth.propertyIsLocal.respectsIso.arrow_mk_iso_iff
    (arrowResLEAppIso f U V hVU)).mpr H

Premises used: Iff.mpr, RingHom.Smooth.propertyIsLocal, AlgebraicGeometry.arrowResLEAppIso, RingHom.RespectsIso.arrow_mk_iso_iff, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H_1 : smoothLocus f = ⊤
x : ↥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
this_1 : IsAffine.{u} (↑U : Scheme)
this : IsAffine.{u} (↑V : Scheme)
⊢ (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth

Tactic:
exact (RingHom.Smooth.propertyIsLocal.respectsIso.arrow_mk_iso_iff
    (arrowResLEAppIso f U V hVU)).mpr H

Premises used: Iff.mpr, RingHom.Smooth.propertyIsLocal, AlgebraicGeometry.arrowResLEAppIso, RingHom.RespectsIso.arrow_mk_iso_iff, RingHom.PropertyIsLocal.respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
h : ∀ (x : ↥U), x ∈ (↑(f ⁻¹ᵁ smoothLocus g) : Set ↥U) ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
⊢ f ⁻¹ᵁ smoothLocus g = smoothLocus (f ≫ g)

Tactic:
ext x
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
x : ↥U
⊢ x ∈ (↑(f ⁻¹ᵁ smoothLocus g) : Set ↥U) ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)

Tactic:
(RingHom.FormallySmooth.respectsIso.cancel_right_isIso _ (f.stalkMap x)).symm.trans ?_

Premises used: Set.Mem, setOf, RingHom.RespectsIso.cancel_right_isIso, Set.preimage, Iff.trans, RingHom.FormallySmooth.respectsIso, AlgebraicGeometry.Scheme.Hom.stalkMap, RingHom.FormallySmooth, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
x : ↥U
h :
  ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (stalkMap g (f x)))).FormallySmooth ↔
    x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
⊢ x ∈ (↑(f ⁻¹ᵁ smoothLocus g) : Set ↥U) ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)

Tactic:
refine (RingHom.FormallySmooth.respectsIso.cancel_right_isIso _ (f.stalkMap x)).symm.trans ?_

Premises used: RingHom.RespectsIso.cancel_right_isIso, Iff.trans, RingHom.FormallySmooth.respectsIso, AlgebraicGeometry.Scheme.Hom.stalkMap, Iff.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
x : ↥U
h : (CommRingCat.Hom.hom (stalkMap (f ≫ g) x)).FormallySmooth ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
⊢ ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (stalkMap g (f x)))).FormallySmooth ↔
    x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)

Tactic:
rw [← CommRingCat.hom_comp, ← stalkMap_comp]

Premises used: CommRingCat.hom_comp, AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
x : ↥U
⊢ (CommRingCat.Hom.hom (stalkMap (f ≫ g) x)).FormallySmooth ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
⊢ EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))

Tactic:
have := LocallyOfFiniteType.stalkMap f (genericPoint X)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
⊢ Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)

Tactic:
algebraize [(f.stalkMap (genericPoint X)).hom]

Premises used: CommRingCat.Hom.hom, AlgebraicGeometry.PresheafedSpace.carrier, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, genericPoint, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.Hom.stalkMap, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algInst : Algebra (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
  (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u) :=
  toAlgebra (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algebraizeInst :
  Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)
K' : CommRingCat :=
  TopCat.Presheaf.stalk (X := PrimeSpectrum.Top K) (TopCat.Sheaf.presheaf (Spec.structureSheaf K)) (f (genericPoint ↥X))
x : (↑(CommRingCat.of K) : Type u)
hx :
  Membership.mem (γ := Submonoid (↑(CommRingCat.of K) : Type u))
    (Ideal.primeCompl (PrimeSpectrum.asIdeal (f (genericPoint ↥X)))) x
⊢ Membership.mem (γ := Submonoid (↑(CommRingCat.of K) : Type u)) (IsUnit.submonoid (↑(CommRingCat.of K) : Type u)) x

Tactic:
aesop (add simp IsUnit.mem_submonoid_iff)

Premises used: IsUnit.mem_submonoid_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algInst : Algebra (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
  (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u) :=
  toAlgebra (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algebraizeInst :
  Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)
K' : CommRingCat :=
  TopCat.Presheaf.stalk (X := PrimeSpectrum.Top K) (TopCat.Sheaf.presheaf (Spec.structureSheaf K)) (f (genericPoint ↥X))
e : K ≃ₐ[K] (↑K' : Type u) :=
  IsLocalization.atUnits (↑(CommRingCat.of K) : Type u) (Ideal.primeCompl (PrimeSpectrum.asIdeal (f (genericPoint ↥X))))
    ⋯
⊢ Algebra.IsAlgebraic K (↑K' : Type u)

Tactic:
have : Algebra.IsAlgebraic K K' :=
    .of_injective e.symm.toAlgHom e.symm.injective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algInst : Algebra (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
  (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u) :=
  toAlgebra (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algebraizeInst :
  Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)
K' : CommRingCat :=
  TopCat.Presheaf.stalk (X := PrimeSpectrum.Top K) (TopCat.Sheaf.presheaf (Spec.structureSheaf K)) (f (genericPoint ↥X))
e : K ≃ₐ[K] (↑K' : Type u) :=
  IsLocalization.atUnits (↑(CommRingCat.of K) : Type u) (Ideal.primeCompl (PrimeSpectrum.asIdeal (f (genericPoint ↥X))))
    ⋯
this_2 : Algebra.IsAlgebraic K (↑K' : Type u)
this_3 : Field (↑K' : Type u) := ⋯.toField
this : Field (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u) := this_3
⊢ PerfectField.{u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)

Tactic:
have : PerfectField ((Spec (.of K)).presheaf.stalk (f (genericPoint X))) :=
    Algebra.IsAlgebraic.perfectField (K := K)
      (L := (Spec.structureSheaf K).presheaf.stalk (f (genericPoint X)))
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algInst : Algebra (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
  (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u) :=
  toAlgebra (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algebraizeInst :
  Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)
K' : CommRingCat :=
  TopCat.Presheaf.stalk (X := PrimeSpectrum.Top K) (TopCat.Sheaf.presheaf (Spec.structureSheaf K)) (f (genericPoint ↥X))
e : K ≃ₐ[K] (↑K' : Type u) :=
  IsLocalization.atUnits (↑(CommRingCat.of K) : Type u) (Ideal.primeCompl (PrimeSpectrum.asIdeal (f (genericPoint ↥X))))
    ⋯
this_2 : Algebra.IsAlgebraic K (↑K' : Type u)
this_3 : Field (↑K' : Type u) := ⋯.toField
this_4 : Field (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u) := this_3
this : PerfectField.{u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
⊢ FormallySmooth (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))

Tactic:
Algebra.FormallySmooth.of_perfectField

Premises used: AlgebraicGeometry.Spec.topObj, Set.Mem, setOf, Algebra.FormallySmooth.of_perfectField, AlgebraicGeometry.PrimeSpectrum.Top, AlgebraicGeometry.structurePresheafInCommRingCat, RingHom.FormallySmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsIntegral X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  EssFiniteType (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algInst : Algebra (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
  (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u) :=
  toAlgebra (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
algebraizeInst :
  Algebra.EssFiniteType.{u, u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
    (↑(X.presheaf.stalk (genericPoint ↥X)) : Type u)
K' : CommRingCat :=
  TopCat.Presheaf.stalk (X := PrimeSpectrum.Top K) (TopCat.Sheaf.presheaf (Spec.structureSheaf K)) (f (genericPoint ↥X))
e : K ≃ₐ[K] (↑K' : Type u) :=
  IsLocalization.atUnits (↑(CommRingCat.of K) : Type u) (Ideal.primeCompl (PrimeSpectrum.asIdeal (f (genericPoint ↥X))))
    ⋯
this_2 : Algebra.IsAlgebraic K (↑K' : Type u)
this_3 : Field (↑K' : Type u) := ⋯.toField
this_4 : Field (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u) := this_3
this : PerfectField.{u} (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u)
⊢ FormallySmooth (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))

Tactic:
exact Algebra.FormallySmooth.of_perfectField

Premises used: Algebra.FormallySmooth.of_perfectField