awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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₂
rw :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
rw₁ :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫ Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
⊢ 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₁
have rw₂ : Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
  Scheme.Hom.appLE g U₂ (Y.basicOpen r) sorry ≫ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
Tactic: rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom,
        g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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₂
rw :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫
      CommRingCat.ofHom (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op)) ≫
        Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
rw₁ :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ V₂ e₂ ≫ Y.presheaf.map (homOfLE ⋯).op ≫ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
rw₂ :
  Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e =
    Scheme.Hom.appLE g U₂ (Y.basicOpen r) ⋯ ≫ Scheme.Hom.appLE f (Y.basicOpen r) (X.basicOpen s) e₁
⊢ 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₁
have rw₃ : Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e = Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) sorry
Tactic: rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom,
        g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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₂
⊢ ∃ (U : Z.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
    IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))
have 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₁
Tactic: have heq : (f ≫ g).appLE U₂ (X.basicOpen s) e = g.appLE U₂ V₂ e₂ ≫
        CommRingCat.ofHom (algebraMap Γ(Y, V₂) Γ(Y, Y.basicOpen r)) ≫
          f.appLE (Y.basicOpen r) (X.basicOpen s) e₁ := by
      rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom,
        g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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₁
⊢ ∃ (U : Z.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ (f ≫ g) ⁻¹ᵁ U),
    IsStandardSmoothOfRelativeDimension (n + m) (CommRingCat.Hom.hom (Scheme.Hom.appLE (f ≫ g) U V e))
have refine : 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: refine ⟨U₂, hU₂, X.basicOpen s, hV₁'.basicOpen s, hx₁, e, heq ▸ ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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₁
⊢ 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₁))
have 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₁))
Tactic: apply IsStandardSmoothOfRelativeDimension.comp ?_ hf₂
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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₁
⊢ 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₁))
have this : IsLocalization.Away r (↑Γ(Y, Y.basicOpen r) : Type u)
Tactic: haveI : IsLocalization.Away r Γ(Y, Y.basicOpen r) := hV₂.isLocalization_basicOpen r
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
⊢ LocallyOfFinitePresentation f
have rw : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ FinitePresentation) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @LocallyOfFinitePresentation]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hf : Smooth f
⊢ affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ FinitePresentation) f
have hf₁ : affineLocally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
Tactic: rw [HasRingHomProperty.eq_affineLocally @Smooth] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ (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))
have this₁ : q.LiesOver p
Tactic: have : q.LiesOver p :=
    ⟨congr($(IsAffineOpen.comap_primeIdealOf_appLE U hU V hV hVU hx).1).symm⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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 ↔
    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))
have trans : (CommRingCat.Hom.hom (Scheme.Hom.stalkMap f x)).FormallySmooth ↔
  Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q)
Tactic: trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ (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))
have 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))
Tactic: trans Algebra.FormallySmooth (Localization.AtPrime p) (Localization.AtPrime q)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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 ↔
    Algebra.FormallySmooth.{u, u} (Localization.AtPrime p) (Localization.AtPrime q)
have 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))
Tactic: rw [← formallySmooth_algebraMap]
-- 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 : 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 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
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 : 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)
⊢ ∃ (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 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
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 : 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
⊢ ∃ (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 this : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
Tactic: have := f.finitePresentation_appLE hU hV hVU
-- 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 : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)).FinitePresentation
⊢ ∃ (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 algebraizeInst : Algebra.FinitePresentation.{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 (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 : (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)
⊢ ∃ (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 this₁ : 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
-- 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
⊢ ∃ (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 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
Tactic: obtain ⟨r, hrx, hr⟩ := Algebra.IsSmoothAt.exists_notMem_smooth Γ(Y, U)
    (hV.primeIdealOf ⟨x, hxV⟩).asIdeal
-- 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)
⊢ ∃ (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_1 : x ∈ X.basicOpen r
Tactic: refine ⟨_, hU, _, hV.basicOpen r, (X.basicOpen_le r).trans hVU, ?_, ?_⟩