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

Tactic:
wlog h : ∃ S, X = Spec S generalizing f X
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
inr : ∀ (i : X.affineCover.I₀), Smooth (X.affineCover.f i ≫ f)
⊢ Smooth f

Tactic:
rw [IsZariskiLocalAtSource.iff_of_openCover (P := @Smooth) X.affineCover]

Premises used: AlgebraicGeometry.IsZariskiLocalAtSource.iff_of_openCover, AlgebraicGeometry.Scheme.affineCover
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
i : X.affineCover.I₀
⊢ ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))

Tactic:
have _ (y) : Smooth (pullback.snd f ((Spec R).fromSpecResidueField y)) :=
      inferInstanceAs <| Smooth (f.fiberToSpecResidueField y)
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
⊢ Smooth (X.affineCover.f i ≫ f)

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

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
inr : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) y)
⊢ Smooth (X.affineCover.f i ≫ f)

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

Premises used: Exists.intro, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
inr :
  Smooth (X := Scheme.Hom.fiber (X.affineCover.f i ≫ f) y)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback f ((Spec R).fromSpecResidueField y)) (X.affineCover.f i)
          (pullback.fst f ((Spec R).fromSpecResidueField y)))
        (Iso.inv (pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)))
        (pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
          pullback.snd f ((Spec R).fromSpecResidueField y)) :
      pullback (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField y) ⟶ Spec ((Spec R).residueField y))
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField (X.affineCover.f i ≫ f) y)

Tactic:
rw [Scheme.Hom.fiberToSpecResidueField, ← pullbackRightPullbackFstIso_inv_snd_snd]

Premises used: AlgebraicGeometry.Scheme.Hom.fiberToSpecResidueField, CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
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_1 : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
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
i : X.affineCover.I₀
h_2 :
  ∀ (y : ↥(Spec R)),
    Smooth (X := pullback f ((Spec R).fromSpecResidueField y)) (pullback.snd f ((Spec R).fromSpecResidueField y))
y : ↥(Spec R)
⊢ Smooth (X := Scheme.Hom.fiber (X.affineCover.f i ≫ f) y)
    (CategoryStruct.comp (Y :=
        pullback (Y := pullback f ((Spec R).fromSpecResidueField y)) (X.affineCover.f i)
          (pullback.fst f ((Spec R).fromSpecResidueField y)))
        (Iso.inv (pullbackRightPullbackFstIso f ((Spec R).fromSpecResidueField y) (X.affineCover.f i)))
        (pullback.snd (X.affineCover.f i) (pullback.fst f ((Spec R).fromSpecResidueField y)) ≫
          pullback.snd f ((Spec R).fromSpecResidueField y)) :
      pullback (X.affineCover.f i ≫ f) ((Spec R).fromSpecResidueField y) ⟶ Spec ((Spec R).residueField y))

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

Tactic:
obtain ⟨S, rfl⟩ := h

Premises used: rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f_1 : X ⟶ Y
R S : CommRingCat
f : Spec S ⟶ Spec R
inst : LocallyOfFinitePresentation f
inst_1 : Flat f
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
obtain :
  ∀ (φ : R ⟶ S) [LocallyOfFinitePresentation (Spec.map φ)] [Flat (Spec.map φ)]
    (h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)), Smooth (Spec.map φ)
⊢ Smooth f

Tactic:
obtain ⟨φ, rfl⟩ := Spec.map_surjective f

Premises used: AlgebraicGeometry.Spec.map_surjective, rfl
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst : LocallyOfFinitePresentation (Spec.map φ)
inst_1 : Flat (Spec.map φ)
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
simp : (CommRingCat.Hom.hom φ).FinitePresentation → (CommRingCat.Hom.hom φ).Flat → (CommRingCat.Hom.hom φ).Smooth
⊢ Smooth (Spec.map φ)

Tactic:
simp only [HasRingHomProperty.Spec_iff] at *

Premises used: AlgebraicGeometry.HasRingHomProperty.Spec_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
⊢ Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
⊢ Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)

Tactic:
algebraize [φ.hom]

Premises used: CommRingCat.Hom.hom
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
⊢ (CommRingCat.Hom.hom φ).Smooth

Tactic:
Algebra.Smooth.of_formallySmooth_fiber fun p hp ↦ ?_

Premises used: Algebra.Smooth.of_formallySmooth_fiber, RingHom.Smooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
refine :
  ∀ (p : Ideal (↑R : Type u)) (hp : p.IsPrime), Algebra.FormallySmooth.{u, u} p.ResidueField (p.Fiber (↑S : Type u))
⊢ (CommRingCat.Hom.hom φ).Smooth

Tactic:
refine Algebra.Smooth.of_formallySmooth_fiber fun p hp ↦ ?_

Premises used: Algebra.Smooth.of_formallySmooth_fiber
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
rw :
  RingHom.FormallySmooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
⊢ Algebra.FormallySmooth.{u, u} p.ResidueField (p.Fiber (↑S : Type u))

Tactic:
rw [← RingHom.formallySmooth_algebraMap]

Premises used: RingHom.formallySmooth_algebraMap
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ RingHom.FormallySmooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))

Tactic:
RingHom.Smooth.formallySmooth ?_

Premises used: RingHom.Smooth.formallySmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
refine :
  RingHom.Smooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))
⊢ RingHom.FormallySmooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))

Tactic:
refine RingHom.Smooth.formallySmooth ?_

Premises used: RingHom.Smooth.formallySmooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
rw :
  Smooth (X :=
    Scheme.Hom.fiber (X := Spec (CommRingCat.of (↑S : Type u)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp : PrimeSpectrum (↑R : Type u) })
    (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp })
⊢ RingHom.Smooth.{u, u} (R := p.ResidueField) (S := p.Fiber (↑S : Type u))
    (algebraMap p.ResidueField (p.Fiber (↑S : Type u)))

Tactic:
rw [← CommRingCat.hom_ofHom (algebraMap p.ResidueField (p.Fiber ↑S)),
    ← HasRingHomProperty.Spec_iff (P := @Smooth), ← MorphismProperty.arrow_mk_iso_iff (P := @Smooth)
    (Spec.fiberToSpecResidueFieldIso R S ⟨p, hp⟩)]

Premises used: AlgebraicGeometry.Spec.fiberToSpecResidueFieldIso, PrimeSpectrum.mk, CommRingCat.carrier, Algebra.algebraMap, Ideal.ResidueField, CategoryTheory.MorphismProperty.arrow_mk_iso_iff, CommRingCat.hom_ofHom, AlgebraicGeometry.HasRingHomProperty.Spec_iff, Ideal.Fiber, AlgebraicGeometry.Smooth
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ Smooth (X :=
    Scheme.Hom.fiber (X := Spec (CommRingCat.of (↑S : Type u)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp : PrimeSpectrum (↑R : Type u) })
    (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp })

Tactic:
h ⟨p, hp⟩

Premises used: PrimeSpectrum.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber
Goal:
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
h : ∀ (y : ↥(Spec R)), Smooth (Scheme.Hom.fiberToSpecResidueField (Spec.map φ) y)
inst : (CommRingCat.Hom.hom φ).FinitePresentation
inst_1 : (CommRingCat.Hom.hom φ).Flat
algInst : Algebra (↑R : Type u) (↑S : Type u) := (CommRingCat.Hom.hom φ).toAlgebra
algebraizeInst : Algebra.FinitePresentation.{u, u} (↑R : Type u) (↑S : Type u)
algebraizeInst_1 : Module.Flat.{u, u} (↑R : Type u) (↑S : Type u)
p : Ideal (↑R : Type u)
hp : p.IsPrime
⊢ Smooth (X :=
    Scheme.Hom.fiber (X := Spec (CommRingCat.of (↑S : Type u)))
      (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp : PrimeSpectrum (↑R : Type u) })
    (Scheme.Hom.fiberToSpecResidueField (Spec.map (CommRingCat.ofHom (algebraMap (↑R : Type u) (↑S : Type u))))
      { asIdeal := p, isPrime := hp })

Tactic:
exact h ⟨p, hp⟩

Premises used: PrimeSpectrum.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : IsOpenImmersion f
⊢ SurjectiveOnStalks f

Tactic:
⟨fun _ ↦ (ConcreteCategory.bijective_of_isIso _).2⟩

Premises used: And.right, AlgebraicGeometry.SurjectiveOnStalks.mk, AlgebraicGeometry.Scheme.Hom.stalkMap, CategoryTheory.ConcreteCategory.bijective_of_isIso
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
⊢ SurjectiveOnStalks (f ≫ g)

Tactic:
⟨fun x ↦ ?_⟩

Premises used: AlgebraicGeometry.SurjectiveOnStalks.mk
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
refine :
  ∀ (x : ↥X),
    Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
      (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
            CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
        (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ SurjectiveOnStalks (f ≫ g)

Tactic:
refine ⟨fun x ↦ ?_⟩
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
rw :
  Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap (f ≫ g) x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
rw [Scheme.Hom.stalkMap_comp]

Premises used: AlgebraicGeometry.Scheme.Hom.stalkMap_comp
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
(f.stalkMap_surjective x).comp (g.stalkMap_surjective (f x))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Surjective.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
hf : SurjectiveOnStalks f
hg : SurjectiveOnStalks g
x : ↥X
⊢ Function.Surjective (α := (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) (β := (↑(X.presheaf.stalk x) : Type u_1))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u_1}) ↦ (↑R : Type u_1) →+* (↑S : Type u_1)) (CC :=
          CommRingCat.carrier) (Scheme.Hom.stalkMap g (f x) ≫ Scheme.Hom.stalkMap f x)) :
      (a : (↑(Z.presheaf.stalk ((f ≫ g) x)) : Type u_1)) → (↑(X.presheaf.stalk x) : Type u_1))

Tactic:
exact (f.stalkMap_surjective x).comp (g.stalkMap_surjective (f x))

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', Function.Surjective.comp, AlgebraicGeometry.PresheafedSpace.Hom.base, DFunLike.coe, AlgebraicGeometry.Scheme.Hom.stalkMap_surjective
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X_1 Y_1 Z_1 : Scheme
f_1 : X_1 ⟶ Y_1
g_1 : Y_1 ⟶ Z_1
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst : SurjectiveOnStalks f
inst_1 : SurjectiveOnStalks g
⊢ SurjectiveOnStalks (f ≫ g)

Tactic:
MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

Premises used: CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem, inferInstance
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
h :
  ∀ (x x_1 : Scheme.{u_1}) (x_2 : x ⟶ x_1),
    SurjectiveOnStalks x_2 ↔
      stalkwise
        (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
          Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
        x_2
⊢ @SurjectiveOnStalks =
    stalkwise fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
      Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S)

Tactic:
ext
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ SurjectiveOnStalks x_2 ↔
    stalkwise
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      x_2

Tactic:
surjectiveOnStalks_iff _

Premises used: AlgebraicGeometry.surjectiveOnStalks_iff, AlgebraicGeometry.stalkwise
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
x x_1 : Scheme
x_2 : x ⟶ x_1
⊢ SurjectiveOnStalks x_2 ↔
    stalkwise
      (fun {R S : Type u_1} [CommRing R] [CommRing S] (x : R →+* S) ↦
        Function.Surjective (α := R) (β := S) (⇑x : (a : R) → S))
      x_2

Tactic:
exact surjectiveOnStalks_iff _

Premises used: AlgebraicGeometry.surjectiveOnStalks_iff
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtTarget @SurjectiveOnStalks

Tactic:
eq_stalkwise ▸ stalkwiseIsZariskiLocalAtTarget_of_respectsIso RingHom.surjective_respectsIso

Premises used: AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise, Eq.rec, AlgebraicGeometry.stalkwiseIsZariskiLocalAtTarget_of_respectsIso, RingHom.surjective_respectsIso, Eq.symm
-- Module: Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
Goal:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ IsZariskiLocalAtSource @SurjectiveOnStalks

Tactic:
eq_stalkwise ▸ stalkwise_isZariskiLocalAtSource_of_respectsIso RingHom.surjective_respectsIso

Premises used: AlgebraicGeometry.SurjectiveOnStalks.eq_stalkwise, Eq.rec, AlgebraicGeometry.stalkwise_isZariskiLocalAtSource_of_respectsIso, RingHom.surjective_respectsIso, Eq.symm