awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have 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)
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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have inr₄ : ∀ (this : (↑(Subtype.mk (p := fun (x : ↥X) ↦ x ∈ U) x hxU) : ↥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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ Dense (↑(smoothLocus f) : Set ↥X)
have this : IsNoetherian X
Tactic: have : IsNoetherian X := { __ := LocallyOfFiniteType.isLocallyNoetherian f }
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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
⊢ IsOpen (X := ↥X) (⋃₀ (irreducibleComponents ↥X \ {irreducibleComponent x}))ᶜ
have rw : IsClosed.{u} (X := ↥X)
  (⋃ (i : Set ↥X),
    ⋃ (_ : Membership.mem (γ := Set (Set ↥X)) (irreducibleComponents ↥X \ {irreducibleComponent x}) i), i)
Tactic: rw [Set.sUnion_eq_biUnion, isOpen_compl_iff]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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' := ⋯ }
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have hU : 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)
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have this₁ : 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 _
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)
have this₁ : genericPoint ↥(↑U : Scheme) ∈ smoothLocus (U.ι ≫ f)
Tactic: have := (U.ι ≫ f).genericPoint_mem_smoothLocus_of_perfectField
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
have rwa : ∀ (this : genericPoint ↥(↑U : Scheme) ∈ U.ι ⁻¹ᵁ smoothLocus f),
  Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
Tactic: rwa [← preimage_smoothLocus_eq, Scheme.Hom.mem_preimage] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ Membership.mem (α := ↥X) (smoothLocus f) (U.ι (genericPoint ↥(↑U : Scheme)) : ↥X)
have rwa₁ : ∀ (this : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (hypothesis)
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)
⊢ x ∈ closure (↑(smoothLocus f) : Set ↥X)
have this₁ : 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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.Smooth (goal)
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)
⊢ Membership.mem (γ := Set ↥X) (closure (Set.image (α := ↥(↑U : Scheme)) (⇑U.ι) Set.univ)) x
have rw : x ∈ irreducibleComponent x
Tactic: rw [Set.image_univ, U.range_ι, hU]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X Y : Scheme
f : X ⟶ Y
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
⊢ Smooth f
have 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
Tactic: wlog h : ∃ R, Y = Spec R
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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
⊢ Smooth f
have 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
Tactic: wlog h : ∃ R, Y = Spec R
Cleared hypotheses: inst, inst_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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
⊢ Smooth f
have 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)
Tactic: rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @Smooth) Y.affineCover]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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))
have 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)
Tactic: refine this _ (fun y ↦ ?_) ⟨_, rfl⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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 := 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)
have 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) sorry sorry)
  (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: apply MorphismProperty.of_isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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))
⊢ 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)
have 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))
Tactic: apply MorphismProperty.of_isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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
⊢ 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)
have inr₄ : Spec ((Y.affineCover.X i).residueField y) ⟶ Spec (Y.residueField ((Y.affineCover.f i) y))
Tactic: apply MorphismProperty.of_isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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))
⊢ 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)
have 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))
Tactic: apply MorphismProperty.of_isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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))
⊢ 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)
have 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))
Tactic: apply MorphismProperty.of_isPullback
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
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
⊢ Smooth f
have obtain : ∀ (R : CommRingCat.{u}) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
  (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)), Smooth f
Tactic: obtain ⟨R, rfl⟩ := h
Cleared hypotheses: Y, f, inst, inst_1, h_1, h
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
⊢ Smooth f
have inr : ∀
  (this :
    ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
      (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y))
      (h : ∃ (S : CommRingCat.{u}), X = Spec S), Smooth f)
  (h : ¬∃ (S : CommRingCat.{u}), X = Spec S), Smooth f
Tactic: wlog h : ∃ S, X = Spec S generalizing f X
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber (goal)
Goal:
X_1 Y : Scheme
f_1 : X_1 ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
inr :
  ∀
    (this :
      ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
        (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y))
        (h : ∃ (S : CommRingCat.{u}), X = Spec S), Smooth f)
    (h : ¬∃ (S : CommRingCat.{u}), X = Spec S), Smooth f
⊢ Smooth f
have wlog : ∀ {X : Scheme.{u}} (f : X ⟶ Spec R) [LocallyOfFinitePresentation f] [Flat f]
  (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) (h : ∃ (S : CommRingCat.{u}), X = Spec S),
  Smooth f
Tactic: wlog h : ∃ S, X = Spec S generalizing f X
Cleared hypotheses: X, f, inst, inst_1, h