awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
        (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X))
    (H : ¬CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
wlog :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
⊢ Dense (↑(smoothLocus f) : Set ↥X)

Tactic:
wlog H : CompactSpace X generalizing X

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, CompactSpace, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
inr : ∀ (U : X.Opens) (hU : U ∈ X.affineOpens) (hxU : x ∈ (↑U : Set ↥X)), x ∈ closure (↑(smoothLocus f) : Set ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)

Tactic:
obtain ⟨_, ⟨U : X.Opens, hU, rfl⟩, hxU, -⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Premises used: isOpen_univ, Set.mem_univ, AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.Opens, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
⊢ Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))

Tactic:
have := this (U.ι ≫ f) (isCompact_iff_compactSpace.mp hU.isCompact) ⟨x, hxU⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
this_1 :
  ∀ {X : Scheme.{u}} [IsReduced X] (f : X ⟶ Spec (CommRingCat.of K)) [inst_5 : LocallyOfFinitePresentation f]
    (H : CompactSpace.{u} ↥X), Dense (↑(smoothLocus f) : Set ↥X)
H : ¬CompactSpace.{u} ↥X
x : ↥X
U : X.Opens
hU : U ∈ X.affineOpens
hxU : x ∈ (↑U : Set ↥X)
this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(smoothLocus (U.ι ≫ f)) : Set ↥(↑U : Scheme))
inr :
  ∀ (this : Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU ∈ closure (↑(U.ι ⁻¹ᵁ smoothLocus f) : Set ↥(↑U : Scheme))),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
inr₁ :
  ∀
    (this :
      Membership.mem (γ := Set ↥(↑U : Scheme)) (closure (⇑U.ι ⁻¹' (↑(smoothLocus f) : Set ↥X)))
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
inr₂ :
  ∀
    (this :
      Membership.mem (γ := Set ↥(↑U : Scheme)) (⇑U.ι ⁻¹' closure (↑(smoothLocus f) : Set ↥X))
        (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU)),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
inr₃ :
  ∀
    (this :
      Membership.mem (α := ↥X) (closure (↑(smoothLocus f) : Set ↥X))
        (U.ι (Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) : ↥X)),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
inr₄ inr₅ inr₆ inr₇ :
  ∀ (this : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) : ↥X) ∈ closure (↑(smoothLocus f) : Set ↥X)),
    x ∈ closure (↑(smoothLocus f) : Set ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)

Tactic:
rwa [← preimage_smoothLocus_eq, Scheme.Hom.coe_preimage,
      ← U.ι.isOpenEmbedding.isOpenMap.preimage_closure_eq_closure_preimage U.ι.continuous,
      Set.mem_preimage, U.ι_apply] at this

Premises used: Topology.IsOpenEmbedding.isOpenMap, IsOpenMap.preimage_closure_eq_closure_preimage, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq, AlgebraicGeometry.Scheme.Hom.isOpenEmbedding, AlgebraicGeometry.Scheme.Hom.coe_preimage, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Opens.ι_apply, AlgebraicGeometry.Scheme.Hom.continuous, Set.mem_preimage
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
⊢ IsNoetherian X

Tactic:
have : IsNoetherian X := { __ := LocallyOfFiniteType.isLocallyNoetherian f }
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this : IsNoetherian X
x : ↥X
rw :
  IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X),
      ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {irreducibleComponent x}) i), i)
⊢ IsOpen (X := ↥X) (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ

Tactic:
rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]

Premises used: Set.sUnion_eq_biUnion, isOpen_compl_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this : IsNoetherian X
x : ↥X
⊢ IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X),
      ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {irreducibleComponent x}) i), i)

Tactic:
TopologicalSpace.NoetherianSpace.finite_irreducibleComponents.diff.isClosed_biUnion
        fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Set.Finite.isClosed_biUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this : IsNoetherian X
x : ↥X
⊢ IsClosed.{u} (X := ↥X)
    (⋃ (i : Set ↥X),
      ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {irreducibleComponent x}) i), i)

Tactic:
exact TopologicalSpace.NoetherianSpace.finite_irreducibleComponents.diff.isClosed_biUnion
        fun W hW ↦ isClosed_of_mem_irreducibleComponents W hW.1

Premises used: isClosed_of_mem_irreducibleComponents, Set.Finite.diff, And.left, TopologicalSpace.NoetherianSpace.finite_irreducibleComponents, Set.Finite.isClosed_biUnion
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
⊢ closure (↑U : Set ↥X) = irreducibleComponent x

Tactic:
have hU : closure U = irreducibleComponent x :=
    closure_sUnion_irreducibleComponents_diff_singleton
      TopologicalSpace.NoetherianSpace.finite_irreducibleComponents
      _ (irreducibleComponent_mem_irreducibleComponents x)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
⊢ IsIntegral.{u} (↑U : Scheme)

Tactic:
have : AlgebraicGeometry.IsIntegral U :=
    have : IrreducibleSpace U := isIrreducible_iff_irreducibleSpace.mp
      (isIrreducible_iff_closure.mp (hU ▸ isIrreducible_irreducibleComponent))
    isIntegral_of_irreducibleSpace_of_isReduced _
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this : IsIntegral.{u} (↑U : Scheme)
⊢ genericPoint ↥(↑U : Scheme) ∈ smoothLocus (U.ι ≫ f)

Tactic:
have := (U.ι ≫ f).genericPoint_mem_smoothLocus_of_perfectField
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this_2 : IsIntegral.{u} (↑U : Scheme)
this : genericPoint ↥(↑U : Scheme) ∈ smoothLocus (U.ι ≫ f)
rwa :
  ∀ (this : genericPoint ↥(↑U : Scheme) ∈ U.ι ⁻¹ᵁ smoothLocus f),
    Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)),
    Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
⊢ Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)

Tactic:
rwa [← preimage_smoothLocus_eq, Scheme.Hom.mem_preimage] at this

Premises used: AlgebraicGeometry.Scheme.Hom.mem_preimage, AlgebraicGeometry.Scheme.Hom.preimage_smoothLocus_eq
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this : IsIntegral.{u} (↑U : Scheme)
⊢ Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)

Tactic:
have : U.ι (genericPoint U) ∈ f.smoothLocus := by
    have := (U.ι ≫ f).genericPoint_mem_smoothLocus_of_perfectField
    rwa [← preimage_smoothLocus_eq, Scheme.Hom.mem_preimage] at this
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this_2 : IsIntegral.{u} (↑U : Scheme)
this : Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
rw : x ∈ irreducibleComponent x
⊢ Membership.mem (γ := Set ↥X) (closure (Set.image (α := ↥(↑U : Scheme)) (⇑U.ι) Set.univ)) x

Tactic:
rw [Set.image_univ, U.range_ι, hU]

Premises used: Set.image_univ, AlgebraicGeometry.Scheme.Opens.range_ι
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this_2 : IsIntegral.{u} (↑U : Scheme)
this : Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
⊢ x ∈ irreducibleComponent x

Tactic:
mem_irreducibleComponent

Premises used: mem_irreducibleComponent
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this_2 : IsIntegral.{u} (↑U : Scheme)
this : Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
⊢ x ∈ irreducibleComponent x

Tactic:
exact mem_irreducibleComponent

Premises used: mem_irreducibleComponent
-- Module: Mathlib.AlgebraicGeometry.Morphisms.Smooth
Goal:
X_1 : Scheme
K : Type u
inst : Field K
inst_1 : PerfectField K
X : Scheme
inst_2 : IsReduced X
f : X ⟶ Spec (CommRingCat.of K)
inst_3 : LocallyOfFinitePresentation f
H : CompactSpace.{u} ↥X
this_1 : IsNoetherian X
x : ↥X
U : X.Opens := { carrier := (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ, is_open' := ⋯ }
hU : closure (↑U : Set ↥X) = irreducibleComponent x
this_2 : IsIntegral.{u} (↑U : Scheme)
this : Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)

Tactic:
exact (((genericPoint_spec U).image U.ι.continuous).specializes (y := x)
    (by rw [Set.image_univ, U.range_ι, hU]; exact mem_irreducibleComponent)).mem_closed
    isClosed_closure (subset_closure this)

Premises used: AlgebraicGeometry.PresheafedSpace.carrier, IsGenericPoint.specializes, subset_closure, IsGenericPoint.image, genericPoint_spec, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, TopCat.carrier, AlgebraicGeometry.Scheme.Opens.ι, AlgebraicGeometry.Scheme.Hom.continuous, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, isClosed_closure, AlgebraicGeometry.Scheme.Opens.toScheme, AlgebraicGeometry.Scheme.toLocallyRingedSpace, Specializes.mem_closed
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
inr :
  ∀
    (this :
      ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
        (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
        Smooth f)
    (h : ¬∃ (R : CommRingCat.{u}), Y = Spec R), Smooth f
wlog :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
⊢ Smooth f

Tactic:
wlog h : ∃ R, Y = Spec R
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
inr :
  ∀ (i : Y.affineCover.toPreZeroHypercover.1),
    Smooth (X := (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i)
      (Scheme.Cover.pullbackHom (P := IsOpenImmersion) Y.affineCover f i :
        (Precoverage.ZeroHypercover.pullback₁ f Y.affineCover).X i ⟶ Y.affineCover.X i)
⊢ Smooth f

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Smooth) Y.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
⊢ Smooth (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i))

Tactic:
this _ (fun y ↦ ?_) ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
inr :
  ∀ (y : ↥(Y.affineCover.X i)),
    Smooth (X := Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y)
      (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y)
⊢ Smooth (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i))

Tactic:
refine this _ (fun y ↦ ?_) ⟨_, rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
inr :
  IsPullback (P := Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y)
    (pullback.map (pullback.snd f (Y.affineCover.f i)) ((Y.affineCover.X i).fromSpecResidueField y) f
      (Y.fromSpecResidueField ((Y.affineCover.f i) y)) (pullback.fst f (Y.affineCover.f i))
      (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y)) (Y.affineCover.f i) ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y)
    (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))
    (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y))
inr₁ :
  Smooth (X :=
    pullback (Y := Spec (Y.residueField ((Y.affineCover.f i) y))) f (Y.fromSpecResidueField ((Y.affineCover.f i) y)))
    (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))
inr₂ inr₃ : Scheme
inr₄ : Spec ((Y.affineCover.X i).residueField y) ⟶ Spec (Y.residueField ((Y.affineCover.f i) y))
inr₅ :
  pullback (Y := Spec (Y.residueField ((Y.affineCover.f i) y))) f (Y.fromSpecResidueField ((Y.affineCover.f i) y)) ⟶
    Spec (Y.residueField ((Y.affineCover.f i) y))
inr₆ :
  Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y ⟶
    pullback (Y := Spec (Y.residueField ((Y.affineCover.f i) y))) f (Y.fromSpecResidueField ((Y.affineCover.f i) y))
⊢ Smooth (X := Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y)
    (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y)

Tactic:
apply MorphismProperty.of_isPullback

Premises used: CategoryTheory.MorphismProperty.of_isPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ IsPullback (P := Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y)
    (pullback.map (pullback.snd f (Y.affineCover.f i)) ((Y.affineCover.X i).fromSpecResidueField y) f
      (Y.fromSpecResidueField ((Y.affineCover.f i) y)) (pullback.fst f (Y.affineCover.f i))
      (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y)) (Y.affineCover.f i) ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y)
    (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))
    (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y))

Tactic:
isPullback_fiberToSpecResidueField_of_isPullback (IsPullback.of_hasPullback _ _) _

Premises used: AlgebraicGeometry.isPullback_fiberToSpecResidueField_of_isPullback, AlgebraicGeometry.Scheme.Hom.fiber, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ IsPullback (P := Scheme.Hom.fiber (X := pullback f (Y.affineCover.f i)) (pullback.snd f (Y.affineCover.f i)) y)
    (pullback.map (pullback.snd f (Y.affineCover.f i)) ((Y.affineCover.X i).fromSpecResidueField y) f
      (Y.fromSpecResidueField ((Y.affineCover.f i) y)) (pullback.fst f (Y.affineCover.f i))
      (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y)) (Y.affineCover.f i) ⋯ ⋯)
    (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y)
    (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))
    (Spec.map (Scheme.Hom.residueFieldMap (Y.affineCover.f i) y))

Tactic:
exact isPullback_fiberToSpecResidueField_of_isPullback (IsPullback.of_hasPullback _ _) _

Premises used: AlgebraicGeometry.isPullback_fiberToSpecResidueField_of_isPullback, CategoryTheory.IsPullback.of_hasPullback
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme.{u}} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (R : CommRingCat.{u}), Y = Spec R),
    Smooth f
h : ¬∃ (R : CommRingCat.{u}), Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth (X :=
    pullback (Y := Spec (Y.residueField ((Y.affineCover.f i) y))) f (Y.fromSpecResidueField ((Y.affineCover.f i) y)))
    (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X_1 Y_1 : Scheme
f_1 : X_1 ⟶ Y_1
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h_1 : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
h : ∃ (R : CommRingCat.{u}), Y = Spec R
obtain :
  ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)), Smooth f
⊢ Smooth f

Tactic:
obtain ⟨R, rfl⟩ := h

Premises used: rfl