awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f_1 : X ⟶ Y
x x_1 : Type u
x_2 : CommRing x
x_3 : CommRing x_1
f x_4 : Type u
x_5 : CommRing f
x_6 : CommRing x_4
x_7 : f →+* x_4
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_7 ↔ x_7.Smooth
have h : Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_7 ↔
  Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_7
Tactic: rw [RingHom.smooth_iff_locally_isStandardSmooth]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have this : HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
  Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Tactic: have : HasRingHomProperty @Smooth.{u} (Locally IsStandardSmooth) := by
    convert! (inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)
    ext f
    rw [RingHom.smooth_iff_locally_isStandardSmooth]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have rw : (∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
  ∀ (x : ↥X),
    ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Tactic: rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
rw :
  (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have hQ : StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Tactic: rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
rw :
  (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
hQ :
  StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ Smooth f ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have hQi : RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
Tactic: rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
⊢ (∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
    ∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have a : ∀ (a : ↥X),
  (∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : a ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
    ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : a ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
this :
  HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth
a : ↥X
⊢ (∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : a ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e)).IsStandardSmooth) ↔
    ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : a ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have a : (∃ (a_1 : Y.Opens) (h : a_1 ∈ Y.affineOpens) (a_2 : X.Opens),
    a ∈ a_2 ∧
      ∃ (h_1 : a_2 ∈ X.affineOpens) (h_2 : a_2 ≤ f ⁻¹ᵁ a_1),
        (CommRingCat.Hom.hom (Scheme.Hom.appLE f a_1 a_2 sorry)).IsStandardSmooth) ↔
  ∃ (U : Y.Opens),
    IsAffineOpen U ∧
      ∃ (V : X.Opens),
        a ∈ V ∧ IsAffineOpen V ∧ ∃ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Tactic: simp [Subtype.exists]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
⊢ Smooth f
have rw : ∀ (x : ↥X),
  ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Tactic: rw [Smooth.iff_forall_exists_isStandardSmooth]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
x : ↥X
⊢ ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
have obtain : ∀ (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))),
  ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
    (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
Tactic: obtain ⟨U, hU, V, hV, hx, e, hf⟩ := exists_isStandardSmoothOfRelativeDimension (n := n) (f := f) x
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty.{u_1} (@SmoothOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
have hQl : LocalizationAwayPreserves.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
Tactic: apply HasRingHomProperty.locally_of_iff
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hQl :
  LocalizationAwayPreserves.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
⊢ HasRingHomProperty.{u_1} (@SmoothOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
have hQa : StableUnderCompositionWithLocalizationAway.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
  IsStandardSmoothOfRelativeDimension n
Tactic: apply HasRingHomProperty.locally_of_iff
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
hQl :
  LocalizationAwayPreserves.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
hQa :
  StableUnderCompositionWithLocalizationAway.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    IsStandardSmoothOfRelativeDimension n
⊢ HasRingHomProperty.{u_1} (@SmoothOfRelativeDimension n) fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n
have h : ∀ {X Y : Scheme.{u_1}} (f : X ⟶ Y),
  SmoothOfRelativeDimension n f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
Tactic: apply HasRingHomProperty.locally_of_iff
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ SmoothOfRelativeDimension n f ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
have h : (∀ (x : ↥X),
    ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
  ∀ (x : ↥X),
    ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : x ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
Tactic: rw [smoothOfRelativeDimension_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ↥X),
      ∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : x ∈ V) (e : V ≤ f ⁻¹ᵁ U),
        IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
    ∀ (x : ↥X),
      ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : x ∈ (↑V : X.Opens)) (e :
        (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
        IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
have h : ∀ (a : ↥X),
  (∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : a ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
    ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : a ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
Tactic: congr!
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
a : ↥X
⊢ (∃ (U : Y.Opens) (_ : IsAffineOpen U) (V : X.Opens) (_ : IsAffineOpen V) (_ : a ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
    ∃ (U : (↑Y.affineOpens : Type u_1)) (V : (↑X.affineOpens : Type u_1)) (_ : a ∈ (↑V : X.Opens)) (e :
      (↑V : X.Opens) ≤ f ⁻¹ᵁ (↑U : Y.Opens)),
      IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U : Y.Opens) (↑V : X.Opens) e))
have h : (∃ (U : Y.Opens),
    IsAffineOpen U ∧
      ∃ (V : X.Opens),
        a ∈ V ∧
          IsAffineOpen V ∧
            ∃ (e : V ≤ f ⁻¹ᵁ U),
              IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e))) ↔
  ∃ (a_1 : Y.Opens) (h : a_1 ∈ Y.affineOpens) (a_2 : X.Opens),
    a ∈ a_2 ∧
      ∃ (h_1 : a_2 ∈ X.affineOpens) (h_2 : a_2 ≤ f ⁻¹ᵁ a_1),
        IsStandardSmoothOfRelativeDimension n (CommRingCat.Hom.hom (Scheme.Hom.appLE f a_1 a_2 sorry))
Tactic: simp [Subtype.exists]
-- 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) (_ : 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 obtain : ∀ (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 : 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))
Tactic: obtain ⟨U₂, hU₂, V₂, hV₂, hfx₂, e₂, hf₂⟩ := hg.exists_isStandardSmoothOfRelativeDimension (f x)
-- 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 : 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 obtain : ∀ (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₁'))),
  ∃ (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))
Tactic: obtain ⟨U₁', hU₁', V₁', hV₁', hx₁', e₁', hf₁'⟩ :=
      hf.exists_isStandardSmoothOfRelativeDimension x
-- 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₁'))
⊢ ∃ (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 obtain : ∀ (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₁))),
  ∃ (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))
Tactic: obtain ⟨r, s, hx₁, e₁, hf₁⟩ := exists_basicOpen_le_appLE_of_appLE_of_isAffine
      (isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n).right
      (isStandardSmoothOfRelativeDimension_localizationPreserves n).away
      x ⟨V₂, hV₂⟩ ⟨U₁', hU₁'⟩ ⟨V₁', hV₁'⟩ ⟨V₁', hV₁'⟩ hx₁' hx₁' e₁' hf₁' hfx₂
-- 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₁))
⊢ ∃ (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 e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂
Tactic: have e : X.basicOpen s ≤ (f ≫ g) ⁻¹ᵁ U₂ :=
      le_trans e₁ <| f.preimage_mono <| le_trans (Y.basicOpen_le r) e₂
-- 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₂
⊢ 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₂ V₂ e₂ ≫
    CommRingCat.ofHom (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE sorry).op)) ≫
      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₁
⊢ 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₂ V₂ e₂ ≫ Y.presheaf.map (homOfLE sorry).op ≫ 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]