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 :
  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
⊢ ∃ (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
have refine_2 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) sorry)).Smooth
Tactic: refine ⟨_, hU, _, hV.basicOpen r, (X.basicOpen_le r).trans hVU, ?_, ?_⟩
-- 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 :
  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)
⊢ x ∈ X.basicOpen r
have refine_1 : ∀
  (hrx :
    Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
      (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
  (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
Tactic: rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
Cleared hypotheses: hrx, hr
-- 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 :
  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 :
  ∀
    (hrx :
      Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
⊢ x ∈ X.basicOpen r
have refine_1₁ : ∀
  (hrx :
    Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (γ :=
      TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
      ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
  (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
Tactic: rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
Cleared hypotheses: hrx, hr
-- 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 :
  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 :
  ∀
    (hrx :
      Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₁ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (γ :=
        TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
⊢ x ∈ X.basicOpen r
have refine_1₂ : ∀
  (hrx :
    Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ X.basicOpen r)
      ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
  (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
Tactic: rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
Cleared hypotheses: hrx, hr
-- 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 :
  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 :
  ∀
    (hrx :
      Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₁ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (γ :=
        TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₂ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ X.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
⊢ x ∈ X.basicOpen r
have refine_1₃ : ∀
  (hrx :
    Membership.mem (α := ↥X) (X.basicOpen r)
      ((IsAffineOpen.fromSpec hV)
          ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))) :
        ↥X))
  (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
Tactic: rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
Cleared hypotheses: hrx, hr
-- 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 :
  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 :
  ∀
    (hrx :
      Membership.mem (γ := TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        (IsAffineOpen.primeIdealOf hV (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV)))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₁ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (γ :=
        TopologicalSpace.Opens (PrimeSpectrum (↑Γ(X, V) : Type u))) (PrimeSpectrum.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₂ :
  ∀
    (hrx :
      Membership.mem (α := PrimeSpectrum (↑Γ(X, V) : Type u)) (IsAffineOpen.fromSpec hV ⁻¹ᵁ X.basicOpen r)
        ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
refine_1₃ :
  ∀
    (hrx :
      Membership.mem (α := ↥X) (X.basicOpen r)
        ((IsAffineOpen.fromSpec hV)
            ((IsAffineOpen.isoSpec hV).hom (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥(Spec Γ(X, V))) :
          ↥X))
    (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
⊢ x ∈ X.basicOpen r
have refine_1₄ : ∀
  (hrx :
    Membership.mem (α := ↥X) (X.basicOpen r)
      (((IsAffineOpen.isoSpec hV).hom ≫ IsAffineOpen.fromSpec hV) (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ V) x hxV) : ↥X))
  (hr : Algebra.Smooth.{u, u} (↑Γ(Y, U) : Type u) (Localization.Away r)), x ∈ X.basicOpen r
Tactic: rwa [← PrimeSpectrum.mem_basicOpen, IsAffineOpen.primeIdealOf,
      ← hV.fromSpec_preimage_basicOpen, Scheme.Hom.mem_preimage, ← Scheme.Hom.comp_apply,
      IsAffineOpen.isoSpec_hom, IsAffineOpen.toSpecΓ_fromSpec] at hrx
Cleared hypotheses: hrx, hr
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
have this₁ : IsLocalization.Away r (↑Γ(X, X.basicOpen r) : Type u)
Tactic: have := hV.isLocalization_basicOpen r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
have hr₁ : 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
Cleared hypotheses: hr, this
-- 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)
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) ⋯)).Smooth
have h : CommRingCat.Hom.hom (Scheme.Hom.appLE f U (X.basicOpen r) sorry) =
  @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: convert!
      RingHom.Smooth.propertyIsLocal.respectsIso.1 _
        (IsLocalization.algEquiv (.powers r) _ Γ(X, X.basicOpen r)).toRingEquiv hr
-- 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)
⊢ 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))
have h : ∀ (x : (↑Γ(Y, U) : Type u)),
  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 :
      (↑Γ(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))
Tactic: ext
-- 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))
    ((@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))
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))
  ((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)) sorry :
        (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: dsimp