awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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))
    ((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))
have h : Eq (α := (↑Γ(X, X.basicOpen r) : Type u))
  ((CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) sorry) :
        (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 [IsScalarTower.algebraMap_apply Γ(Y, U) Γ(X, V) (Localization _),
      IsLocalization.map_eq]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
⊢ IsOpen.{u} (X := ↥X) {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}
have 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
Tactic: refine isOpen_iff_forall_mem_open.mpr fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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
⊢ ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t
have 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
Tactic: obtain ⟨U, hU, V, hV, hVU, hxV, H⟩ := exists_smooth_of_formallySmooth_stalk f x hx
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ ∃ t ⊆ {x : ↥X | (CommRingCat.Hom.hom (stalkMap f x)).FormallySmooth}, IsOpen t ∧ x ∈ t
have algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
Tactic: algebraize [(f.appLE U V hVU).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
⊢ smoothLocus f = ⊤
have rw : ⊤ ≤ smoothLocus f
Tactic: rw [← top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : Smooth f
x : ↥X
⊢ x ∈ smoothLocus f
have obtain : ∀ (U : TopologicalSpace.Opens ↥Y) (hU : U ∈ Y.affineOpens) (hxU : Membership.mem (α := ↥Y) (↑U : Set ↥Y) (f x : ↥Y)),
  x ∈ smoothLocus f
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ x ∈ smoothLocus f
have obtain : ∀ (V : TopologicalSpace.Opens ↥X) (hV : V ∈ X.affineOpens) (hxV : x ∈ (↑V : Set ↥X))
  (hVU : (↑V : Set ↥X) ⊆ ⇑f ⁻¹' U.carrier), x ∈ smoothLocus f
Tactic: obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
    X.isBasis_affineOpens.exists_subset_of_mem_open hxU (U.2.preimage f.continuous)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ x ∈ smoothLocus f
have this : (CommRingCat.Hom.hom (appLE f U V hVU)).Smooth
Tactic: have := f.smooth_appLE hU hV hVU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ x ∈ smoothLocus f
have algebraizeInst : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (↑Γ(X, V) : Type u)
Tactic: algebraize [(f.appLE U V hVU).hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ x ∈ smoothLocus f
have 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))
Tactic: rw [Scheme.Hom.mem_smoothLocus, formallySmooth_stalkMap_iff U hU V hV hVU hxV]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
⊢ smoothLocus f = ⊤ ↔ Smooth f
have refine : ∀ (H : smoothLocus f = ⊤), Smooth f
Tactic: refine ⟨fun H ↦ ?_, fun _ ↦ f.smoothLocus_eq_top⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H : smoothLocus f = ⊤
⊢ Smooth f
have refine : ∀ (x : ↥X), ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)
Tactic: refine IsZariskiLocalAtSource.iff_exists_resLE.mpr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
H : smoothLocus f = ⊤
x : ↥X
⊢ ∃ (U : Y.Opens) (V : X.Opens) (_ : x ∈ V.carrier) (e : V ≤ f ⁻¹ᵁ U), Smooth (resLE f U V e)
have 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)
Tactic: obtain ⟨U, hU, V, hV, hVU, hxV, H⟩ :=
    exists_smooth_of_formallySmooth_stalk f _ (H.ge (Set.mem_univ x))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
have refine : Smooth (resLE f U V hVU)
Tactic: refine ⟨U, V, hxV, hVU, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ Smooth (resLE f U V hVU)
have this : IsAffine.{u} (↑U : Scheme)
Tactic: have : IsAffine _ := hU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)
⊢ Smooth (resLE f U V hVU)
have this₁ : IsAffine.{u} (↑V : Scheme)
Tactic: have : IsAffine _ := hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ Smooth (resLE f U V hVU)
have rw : (CommRingCat.Hom.hom (appTop (resLE f U V hVU))).Smooth
Tactic: rw [HasRingHomProperty.iff_of_isAffine (P := @Smooth)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y U : Scheme
f : U ⟶ X
g : X ⟶ Y
inst : IsOpenImmersion f
inst_1 : LocallyOfFinitePresentation g
⊢ f ⁻¹ᵁ smoothLocus g = smoothLocus (f ≫ g)
have h : ∀ (x : ↥U), x ∈ (↑(f ⁻¹ᵁ smoothLocus g) : Set ↥U) ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
have h : ((CommRingCat.Hom.hom (stalkMap f x)).comp (CommRingCat.Hom.hom (stalkMap g (f x)))).FormallySmooth ↔
  x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
Tactic: refine (RingHom.FormallySmooth.respectsIso.cancel_right_isIso _ (f.stalkMap x)).symm.trans ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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 x)).comp (CommRingCat.Hom.hom (stalkMap g (f x)))).FormallySmooth ↔
    x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
have h : (CommRingCat.Hom.hom (stalkMap (f ≫ g) x)).FormallySmooth ↔ x ∈ (↑(smoothLocus (f ≫ g)) : Set ↥U)
Tactic: rw [← CommRingCat.hom_comp, ← stalkMap_comp]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ genericPoint ↥X ∈ smoothLocus f
have this : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)))
⊢ FormallySmooth (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
have algebraizeInst : 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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))))
    ⋯
⊢ FormallySmooth (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
have this₁ : Algebra.IsAlgebraic K (↑K' : Type u)
Tactic: have : Algebra.IsAlgebraic K K' :=
    .of_injective e.symm.toAlgHom e.symm.injective
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ FormallySmooth (R := (↑((Spec (CommRingCat.of K)).presheaf.stalk (f (genericPoint ↥X))) : Type u))
    (CommRingCat.Hom.hom (stalkMap f (genericPoint ↥X)))
have this₁ : 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)))
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
⊢ Dense (↑(smoothLocus f) : Set ↥X)
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
      (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X))
  (H : ¬CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
Tactic: wlog H : CompactSpace X generalizing X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
        (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X))
    (H : ¬CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
⊢ Dense (↑(smoothLocus f) : Set ↥X)
have wlog : ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
  (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
Tactic: wlog H : CompactSpace X generalizing X
Cleared hypotheses: inst_2, f, inst_3
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have inr : ∀ (U : X.Opens) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)), x ∈ closure (↑(smoothLocus f) : Set ↥X)
Tactic: obtain ⟨_, ⟨U : X.Opens, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have this₁ : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))
Tactic: have := this (U.ι ≫ f) (isCompact_iff_compactSpace.mp hU.isCompact) ⟨x, hxU⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have inr : ∀ (this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(U.ι ⁻¹ᵁ smoothLocus f) : Set ↥(↑U : Scheme))),
  x ∈ closure (↑(smoothLocus f) : Set ↥X)
Tactic: rwa [← preimage_smoothLocus_eq, Scheme.Hom.coe_preimage,
      ← U.ι.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage U.ι.continuous,
      Set.mem_preimage, U.ι_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))
inr :
  ∀ (this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(U.ι ⁻¹ᵁ smoothLocus f) : Set ↥(↑U : Scheme))),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have inr₁ : ∀
  (this :
    Membership.mem (γ := Set ↥(↑U : Scheme)) (closure (⇑U.ι ⁻¹' (↑(smoothLocus f) : Set ↥X)))
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)),
  x ∈ closure (↑(smoothLocus f) : Set ↥X)
Tactic: rwa [← preimage_smoothLocus_eq, Scheme.Hom.coe_preimage,
      ← U.ι.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage U.ι.continuous,
      Set.mem_preimage, U.ι_apply] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))
inr :
  ∀ (this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(U.ι ⁻¹ᵁ smoothLocus f) : Set ↥(↑U : Scheme))),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
inr₁ :
  ∀
    (this :
      Membership.mem (γ := Set ↥(↑U : Scheme)) (closure (⇑U.ι ⁻¹' (↑(smoothLocus f) : Set ↥X)))
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have inr₂ : ∀
  (this :
    Membership.mem (γ := Set ↥(↑U : Scheme)) (⇑U.ι ⁻¹' closure (↑(smoothLocus f) : Set ↥X))
      (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)),
  x ∈ closure (↑(smoothLocus f) : Set ↥X)
Tactic: rwa [← preimage_smoothLocus_eq, Scheme.Hom.coe_preimage,
      ← U.ι.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage U.ι.continuous,
      Set.mem_preimage, U.ι_apply] at this
Cleared hypotheses: this