Module: Mathlib.AlgebraicGeometry.Morphisms.SmoothFiber

Goal state before:
pp: case inr.sq
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ IsPullback ?inr.f' (Scheme.Hom.fiberToSpecResidueField (pullback.snd f (Y.affineCover.f i)) y) ?g ?inr.f

pp: case inr.hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth ?g

pp: case inr.Y
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Scheme

pp: case inr.S
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Scheme

pp: case inr.f
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Spec ((Y.affineCover.X i).residueField y) ⟶ ?inr.S

pp: case g
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ ?inr.Y ⟶ ?inr.S

pp: case inr.f'
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Scheme.Hom.fiber (pullback.snd f (Y.affineCover.f i)) y ⟶ ?inr.Y

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

Goal state after:
case inr.hg
X Y : Scheme
f : X ⟶ Y
inst✝¹ : LocallyOfFinitePresentation f
inst✝ : Flat f
h✝ : ∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f] [Flat f],
    (∀ (y : ↥Y), Smooth (Scheme.Hom.fiberToSpecResidueField f y)) → (∃ R, Y = Spec R) → Smooth f
h : ¬∃ R, Y = Spec R
i : Y.affineCover.toPreZeroHypercover.1
y : ↥(Y.affineCover.X i)
⊢ Smooth (Scheme.Hom.fiberToSpecResidueField f ((Y.affineCover.f i) y))