awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X : Scheme
rw :
  autoParam
      (IsClosedImmersion (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam =
    IsClosedImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
⊢ X.IsSeparated ↔ IsClosedImmersion (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rw [isSeparated_iff, AlgebraicGeometry.isSeparated_iff, iff_iff_eq,
    ← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion _ (prodIsoPullback X X).hom]

Premises used: iff_iff_eq, AlgebraicGeometry.isSeparated_iff, AlgebraicGeometry.Scheme.isSeparated_iff, prodIsoPullback, CategoryTheory.Iso.hom, AlgebraicGeometry.IsClosedImmersion, CategoryTheory.MorphismProperty.cancel_right_of_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X : Scheme
e_f :
  Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
⊢ autoParam
      (IsClosedImmersion (Y := pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
        (pullback.diagonal (terminal.from X)))
      IsSeparated.isClosedImmersion_diagonal._autoParam =
    IsClosedImmersion (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))

Tactic:
congr
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X : Scheme
e_f :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
e_f₁ :
  CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)
⊢ Eq (α := X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (pullback.diagonal (terminal.from X) : X ⟶ pullback.diagonalObj (Y := ⊤_ Scheme) (terminal.from X))
    (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
      X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))

Tactic:
ext : 1
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X : Scheme
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.fst (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.fst (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
X : Scheme
⊢ CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.diagonal (terminal.from X)) (pullback.snd (terminal.from X) (terminal.from X)) =
    CategoryStruct.comp (Y := pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (CategoryStruct.comp (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X)) (Iso.hom (prodIsoPullback X X)) :
        X ⟶ pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X))
      (pullback.snd (terminal.from X) (terminal.from X) :
        pullback (Z := ⊤_ Scheme) (terminal.from X) (terminal.from X) ⟶ X)

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst rwa rwa₁ rwa₂ rwa₃ : X.IsSeparated
⊢ IsClosedImmersion (Y := X ⨯ X) (prod.lift (𝟙 X) (𝟙 X))

Tactic:
rwa [← isSeparated_iff_isClosedImmersion_prod_lift]

Premises used: AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
inst : IsAffine X
⊢ X.IsSeparated

Tactic:
⟨inferInstance⟩

Premises used: inferInstance, AlgebraicGeometry.Scheme.IsSeparated.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y Z : Scheme
f : X_1 ⟶ Y
g : Y ⟶ Z
X : Scheme
inst : X.IsSeparated
⊢ QuasiSeparatedSpace.{u} ↥X

Tactic:
quasiSeparatedSpace_of_quasiSeparated (terminal.from X)

Premises used: CategoryTheory.Limits.terminal.from, AlgebraicGeometry.quasiSeparatedSpace_of_quasiSeparated
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : X.IsSeparated
inst : IsSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)
⊢ IsSeparated f

Tactic:
apply +allowSynthFailures @IsSeparated.of_comp (g := terminal.from Y)

Premises used: AlgebraicGeometry.IsSeparated.of_comp, CategoryTheory.Limits.terminal.from
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst_1 : X.IsSeparated
inst : IsSeparated (Y := ⊤_ Scheme) (terminal.from X)
⊢ IsSeparated (Y := ⊤_ Scheme) (f ≫ terminal.from Y)

Tactic:
rw [terminal.comp_from]

Premises used: CategoryTheory.Limits.terminal.comp_from
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : X.IsSeparated
⊢ IsSeparated (Y := ⊤_ Scheme) (terminal.from X)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f_1 : X ⟶ Y
g_1 : Y ⟶ Z
f g : X ⟶ Y
inst : Y.IsSeparated
⊢ IsClosedImmersion (X := equalizer f g) (equalizer.ι f g)

Tactic:
MorphismProperty.of_isPullback (isPullback_equalizer_prod f g).flip inferInstance

Premises used: CategoryTheory.MorphismProperty.of_isPullback, CategoryTheory.Limits.isPullback_equalizer_prod, inferInstance, CategoryTheory.IsPullback.flip
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ HasAffineProperty (@IsSeparated) (AffineTargetMorphismProperty.of @IsSeparated)

Tactic:
HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated

Premises used: AlgebraicGeometry.IsSeparated, AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
h :
  ∀ (X Y : Scheme.{u_1}) (f : X ⟶ Y) (hY : IsAffine Y), X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
⊢ HasAffineProperty @IsSeparated fun (X x : Scheme.{u_1}) (x_1 : X ⟶ x) (x_2 : IsAffine x) ↦ X.IsSeparated

Tactic:
convert! HasAffineProperty.of_isZariskiLocalAtTarget @IsSeparated with X Y f hY

Premises used: AlgebraicGeometry.IsSeparated, AlgebraicGeometry.HasAffineProperty.of_isZariskiLocalAtTarget
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
h : IsSeparated f ↔ AffineTargetMorphismProperty.of (@IsSeparated) f
⊢ X.IsSeparated ↔ AffineTargetMorphismProperty.of (@IsSeparated) f

Tactic:
rw [Scheme.isSeparated_iff, ← terminal.comp_from f, IsSeparated.comp_iff]

Premises used: CategoryTheory.Limits.terminal.comp_from, AlgebraicGeometry.Scheme.isSeparated_iff, AlgebraicGeometry.IsSeparated.comp_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X_1 Y_1 Z : Scheme
f_1 : X_1 ⟶ Y_1
g : Y_1 ⟶ Z
X Y : Scheme
f : X ⟶ Y
hY : IsAffine Y
⊢ IsSeparated f ↔ AffineTargetMorphismProperty.of (@IsSeparated) f

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Separated
Goal:
W X Y : Scheme
inst : IsReduced X
f g : X ⟶ Y
inst_1 : Y.IsSeparated
ι : W ⟶ X
inst_2 : IsDominant ι
hU : ι ≫ f = ι ≫ g
⊢ f = g

Tactic:
ext_of_isDominant_of_isSeparated (Limits.terminal.from _) (Limits.terminal.hom_ext _ _) ι hU

Premises used: CategoryTheory.Limits.terminal.hom_ext, AlgebraicGeometry.ext_of_isDominant_of_isSeparated, CategoryTheory.Limits.terminal.from
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
h :
  ∀ ⦃X Y : Scheme.{u_1}⦄ (f : X ⟶ Y),
    Smooth f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
⊢ @Smooth = affineLocally fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth

Tactic:
ext X Y f
-- 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 :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
    affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f
h₁ h₂ :
  (∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens},
          IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth) ↔
    ∀ {U : Y.Opens},
      IsAffineOpen U →
        ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).Smooth
⊢ Smooth f ↔ affineLocally (fun {R S : Type u_1} [CommRing R] [CommRing S] ↦ RingHom.Smooth) f

Tactic:
rw [smooth_iff, affineLocally_iff_forall_isAffineOpen]

Premises used: AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen, AlgebraicGeometry.smooth_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦ RingHom.Smooth

Tactic:
(inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)

Premises used: inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
h :
  ∀ (x x_1 : Type u) (x : CommRing x) (x : CommRing x_1),
    (@Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) = @RingHom.Smooth
⊢ HasRingHomProperty @Smooth fun {R S : Type u} [CommRing R] [CommRing S] ↦
    Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
convert! (inferInstance : HasRingHomProperty (@Smooth.{u}) RingHom.Smooth)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
x x_1 : Type u
x_2 : CommRing x
x_3 : CommRing x_1
h :
  ∀ (f x : Type u) (x_4 : CommRing f) (x_5 : CommRing x) (x_6 : f →+* x),
    Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_6 ↔ x_6.Smooth
⊢ (@Locally fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) = @RingHom.Smooth

Tactic:
ext f
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
h 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
⊢ Locally (fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth) x_7 ↔ x_7.Smooth

Tactic:
rw [RingHom.smooth_iff_locally_isStandardSmooth]

Premises used: RingHom.smooth_iff_locally_isStandardSmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
⊢ 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]
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
hQi : RespectsIso.{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

Tactic:
rw [HasRingHomProperty.iff_exists_appLE_locally (P := @Smooth)]

Premises used: AlgebraicGeometry.HasRingHomProperty.iff_exists_appLE_locally
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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 :
  ∀ (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
⊢ (∀ (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:
congr!
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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_1 : ↥X
a :
  (∃ (a : Y.Opens) (h : a ∈ Y.affineOpens) (a_2 : X.Opens),
      a_1 ∈ a_2 ∧
        ∃ (h_1 : a_2 ∈ X.affineOpens) (h_2 : a_2 ≤ f ⁻¹ᵁ a),
          (CommRingCat.Hom.hom (Scheme.Hom.appLE f a a_2 ⋯)).IsStandardSmooth) ↔
    ∃ (U : Y.Opens),
      IsAffineOpen U ∧
        ∃ (V : X.Opens),
          a_1 ∈ V ∧
            IsAffineOpen V ∧ ∃ (e : V ≤ f ⁻¹ᵁ U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth
⊢ (∃ (U : (↑Y.affineOpens : Type u)) (V : (↑X.affineOpens : Type u)) (_ : a_1 ∈ (↑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_1 ∈ V) (e : V ≤ f ⁻¹ᵁ U),
      (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).IsStandardSmooth

Tactic:
simp [Subtype.exists]

Premises used: Subtype.exists
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
⊢ (∃ (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 ⋯)).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:
grind [Scheme.affineOpens]

Premises used: AlgebraicGeometry.Scheme.affineOpens
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
⊢ StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
isStandardSmooth_stableUnderCompositionWithLocalizationAway.left

Premises used: And.left, RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
⊢ StableUnderCompositionWithLocalizationAwaySource.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
exact isStandardSmooth_stableUnderCompositionWithLocalizationAway.left

Premises used: And.left, RingHom.isStandardSmooth_stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
isStandardSmooth_respectsIso

Premises used: RingHom.isStandardSmooth_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
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
⊢ RespectsIso.{u} fun {R S : Type u} [CommRing R] [CommRing S] ↦ IsStandardSmooth

Tactic:
exact isStandardSmooth_respectsIso

Premises used: RingHom.isStandardSmooth_respectsIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X Y : Scheme
f : X ⟶ Y
inst : 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

Tactic:
(iff_forall_exists_isStandardSmooth f).mp ‹_› x

Premises used: Iff.mp, AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderComposition @Smooth

Tactic:
HasRingHomProperty.stableUnderComposition Smooth.stableUnderComposition

Premises used: RingHom.Smooth.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.stableUnderComposition
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
Z : Scheme
g : Y ⟶ Z
inst : Smooth f
inst_1 : Smooth g
⊢ Smooth (f ≫ g)

Tactic:
MorphismProperty.comp_mem _ f g ‹Smooth f› ‹Smooth g›

Premises used: CategoryTheory.MorphismProperty.comp_mem
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.IsStableUnderBaseChange @Smooth

Tactic:
HasRingHomProperty.isStableUnderBaseChange Smooth.isStableUnderBaseChange

Premises used: AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange, RingHom.Smooth.isStableUnderBaseChange
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n m : ℕ
X Y : Scheme
f : X ⟶ Y
⊢ MorphismProperty.Respects (@Smooth) IsOpenImmersion

Tactic:
HasRingHomProperty.respects_isOpenImmersion
    (RingHom.Smooth.stableUnderComposition.stableUnderCompositionWithLocalizationAway
      RingHom.Smooth.holdsForLocalizationAway).1

Premises used: RingHom.Smooth.stableUnderComposition, AlgebraicGeometry.HasRingHomProperty.respects_isOpenImmersion, RingHom.Smooth.holdsForLocalizationAway, And.left, RingHom.StableUnderComposition.stableUnderCompositionWithLocalizationAway
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
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
⊢ Smooth f

Tactic:
rw [Smooth.iff_forall_exists_isStandardSmooth]

Premises used: AlgebraicGeometry.Smooth.iff_forall_exists_isStandardSmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
x : ↥X
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
⊢ ∃ (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

Premises used: AlgebraicGeometry.SmoothOfRelativeDimension.exists_isStandardSmoothOfRelativeDimension
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
x : ↥X
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:
⟨U, hU, V, hV, hx, e, hf.isStandardSmooth⟩

Premises used: Exists.intro, RingHom.IsStandardSmoothOfRelativeDimension.isStandardSmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
n : ℕ
X Y : Scheme
f : X ⟶ Y
inst : SmoothOfRelativeDimension n f
x : ↥X
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:
exact ⟨U, hU, V, hV, hx, e, hf.isStandardSmooth⟩