awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
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))
⊢ 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

Tactic:
apply HasRingHomProperty.locally_of_iff

Premises used: AlgebraicGeometry.HasRingHomProperty.locally_of_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ LocalizationAwayPreserves.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

Tactic:
(isStandardSmoothOfRelativeDimension_localizationPreserves n).away

Premises used: RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves, RingHom.LocalizationPreserves.away
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ LocalizationAwayPreserves.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ IsStandardSmoothOfRelativeDimension n

Tactic:
exact (isStandardSmoothOfRelativeDimension_localizationPreserves n).away

Premises used: RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves, RingHom.LocalizationPreserves.away
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    IsStandardSmoothOfRelativeDimension n

Tactic:
isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n

Premises used: RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ StableUnderCompositionWithLocalizationAway.{u_1} fun {R S : Type u_1} [CommRing R] [CommRing S] ↦
    IsStandardSmoothOfRelativeDimension n

Tactic:
exact isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway n

Premises used: RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
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))
⊢ 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:
rw [smoothOfRelativeDimension_iff]

Premises used: AlgebraicGeometry.smoothOfRelativeDimension_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
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))
⊢ (∀ (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:
congr!
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
a : ↥X
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 ⋯))
⊢ (∃ (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:
simp [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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),
          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 ⋯))

Tactic:
grind [Scheme.affineOpens]

Premises used: AlgebraicGeometry.Scheme.affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n : ℕ
⊢ MorphismProperty.IsStableUnderBaseChange (@SmoothOfRelativeDimension n)

Tactic:
HasRingHomProperty.isStableUnderBaseChange <| locally_isStableUnderBaseChange
    isStandardSmoothOfRelativeDimension_respectsIso
    (isStandardSmoothOfRelativeDimension_isStableUnderBaseChange n)

Premises used: RingHom.locally_isStableUnderBaseChange, AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, RingHom.isStandardSmoothOfRelativeDimension_respectsIso, RingHom.isStandardSmoothOfRelativeDimension_isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ SmoothOfRelativeDimension 0 f

Tactic:
HasRingHomProperty.of_isOpenImmersion
    (locally_holdsForLocalizationAway <|
      isStandardSmoothOfRelativeDimension_holdsForLocalizationAway).containsIdentities

Premises used: RingHom.HoldsForLocalizationAway.containsIdentities, RingHom.locally_holdsForLocalizationAway, RingHom.isStandardSmoothOfRelativeDimension_holdsForLocalizationAway, AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
inst : IsOpenImmersion f
⊢ Smooth f

Tactic:
SmoothOfRelativeDimension.smooth 0 f

Premises used: AlgebraicGeometry.SmoothOfRelativeDimension.smooth, OfNat.ofNat
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Smooth g
⊢ Smooth (X := pullback f g) (pullback.fst f g)

Tactic:
MorphismProperty.pullback_fst f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_fst
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst : Smooth f
⊢ Smooth (X := pullback f g) (pullback.snd f g)

Tactic:
MorphismProperty.pullback_snd f g inferInstance

Premises used: inferInstance, CategoryTheory.MorphismProperty.pullback_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f_1 f : X ⟶ Y
V : Y.Opens
inst : Smooth f
⊢ Smooth (f ∣_ V)

Tactic:
IsZariskiLocalAtTarget.restrict ‹_› V

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.restrict
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f_1 f : X ⟶ Y
U : X.Opens
V : Y.Opens
e : U ≤ f ⁻¹ᵁ V
inst : Smooth f
⊢ Smooth (X.homOfLE e ≫ f ∣_ V)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
hf : SmoothOfRelativeDimension n f
hg : SmoothOfRelativeDimension m g
x : ↥X
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))
⊢ ∃ (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)

Premises used: AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension, CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₂))
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))
⊢ ∃ (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

Premises used: AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₁'))
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))
⊢ ∃ (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₂

Premises used: RingHom.isStandardSmoothOfRelativeDimension_localizationPreserves, Subtype.mk, RingHom.isStandardSmoothOfRelativeDimension_stableUnderCompositionWithLocalizationAway, And.right, AlgebraicGeometry.exists_basicOpen_le_appLE_of_appLE_of_isAffine, RingHom.LocalizationPreserves.away
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₁))
⊢ 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₂
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₁
rw₃ rw₄ : Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) e = Scheme.Hom.appLE (f ≫ g) U₂ (X.basicOpen s) ⋯
⊢ 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:
rw [RingHom.algebraMap_toAlgebra, CommRingCat.ofHom_hom,
        g.appLE_map_assoc, Scheme.Hom.appLE_comp_appLE]

Premises used: CommRingCat.ofHom_hom, AlgebraicGeometry.Scheme.Hom.appLE_map_assoc, RingHom.algebraMap_toAlgebra, AlgebraicGeometry.Scheme.Hom.appLE_comp_appLE
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₁

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]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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))

Tactic:
⟨U₂, hU₂, X.basicOpen s, hV₁'.basicOpen s, hx₁, e, heq ▸ ?_⟩

Premises used: AlgebraicGeometry.IsAffineOpen.basicOpen, Eq.rec, AlgebraicGeometry.Scheme.basicOpen, Exists.intro, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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₁
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₁))
⊢ ∃ (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:
refine ⟨U₂, hU₂, X.basicOpen s, hV₁'.basicOpen s, hx₁, e, heq ▸ ?_⟩