awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
x : ↥X
inst : X.IsGermInjectiveAt x
U : X.Opens
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e_1 : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
V : X.Opens
hxV : x ∈ V
iVU : V ≤ U
hV : (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
V' : X.Opens
hxV' : x ∈ V'
hV' : IsAffineOpen V'
iV'V : V' ≤ V
H :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op V')) : Type u)) (β := (↑(X.presheaf.stalk x) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
          CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV')) :
      (a : (↑(X.presheaf.obj (Opposite.op V')) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
f : X.presheaf.obj (Opposite.op V') ⟶ X.presheaf.stalk x := X.presheaf.germ V' x hxV'
hf' : RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV)) ≤ (CommRingCat.Hom.hom f).range
e : (↑(X.presheaf.obj (Opposite.op V')) : Type u) ≃+*
  ↥(RingHom.range
      (ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ V' x hxV'))) :=
  RingEquiv.ofLeftInverse ⋯
a : (↑R : Type u)
⊢ Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ U x ⋯) :
          (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        ((φRX.hom' : (a : (↑R : Type u)) → (↑Γ(X, U) : Type u)) a : (↑Γ(X, U) : Type u)) :
      (↑(X.presheaf.stalk x) : Type u))
    ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
            CommRingCat.carrier) (Y := X.presheaf.stalk x) (φRX ≫ X.presheaf.germ U x hxU) :
          (a : (↑R : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        a :
      (↑(X.presheaf.stalk x) : Type u))

Tactic:
rfl
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
obtain :
  ∀ (U : TopologicalSpace.Opens ↥S) (hU : U ∈ S.affineOpens) (hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)),
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
      Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

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

Premises used: CategoryTheory.ConcreteCategory.hom, AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', isOpen_univ, Set.mem_univ, AlgebraicGeometry.PresheafedSpace.Hom.base, AlgebraicGeometry.Scheme.isBasis_affineOpens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
⊢ Membership.mem (α := ↥S) U (sY y : ↥S)

Tactic:
have hyU : sY y ∈ U := e ▸ hxU
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
obtain :
  ∀ (V : Y.Opens) (hV : V ∈ Y.affineOpens) (hyV : y ∈ (↑V : Set ↥Y)) (iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier),
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
      Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hyV, iVU⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open hyU (sY ⁻¹ᵁ U).2

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, TopologicalSpace.Opens.is_open', AlgebraicGeometry.Scheme.isBasis_affineOpens, AlgebraicGeometry.Scheme.Opens, CategoryTheory.Functor.obj, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
rw :
  S.presheaf.germ U (sY y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
⊢ Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
rw [Scheme.Hom.appLE, Category.assoc, Y.presheaf.germ_res_assoc,
      ← Scheme.Hom.germ_stalkMap_assoc, h]

Premises used: AlgebraicGeometry.Scheme.Hom.germ_stalkMap_assoc, CategoryTheory.Category.assoc, TopCat.Presheaf.germ_res_assoc, AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
⊢ S.presheaf.germ U (sY y) ⋯ ≫ S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x =
    Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
⊢ Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU

Tactic:
have : sY.appLE U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ =
      sX.app U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU := by
    rw [Scheme.Hom.appLE, Category.assoc, Y.presheaf.germ_res_assoc,
      ← Scheme.Hom.germ_stalkMap_assoc, h]
    simp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
obtain :
  ∀ (W : X.Opens) (hxW : x ∈ W) (φ' : Γ(Y, V) ⟶ Γ(X, W)) (i : W ≤ sX ⁻¹ᵁ U) (hW : IsAffineOpen W)
    (h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW)
    (h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'),
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
      Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
obtain ⟨W, hxW, φ', i, hW, h₁, h₂⟩ :=
    exists_lift_of_germInjective (R := Γ(S, U)) (A := Γ(Y, V)) (U := sX ⁻¹ᵁ U) (x := x) hxU
    (Y.presheaf.germ _ y hyV ≫ φ) (sY.appLE U V iVU) (sX.app U)
    (sY.finiteType_appLE hU hV _) this

Premises used: AlgebraicGeometry.Scheme.Hom.appLE, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.app, AlgebraicGeometry.Scheme.Hom.finiteType_appLE, CategoryTheory.CategoryStruct.comp, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace, AlgebraicGeometry.exists_lift_of_germInjective
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩

Premises used: AlgebraicGeometry.Spec.map, AlgebraicGeometry.IsAffineOpen.fromSpec, And.intro, AlgebraicGeometry.Scheme.Opens.toSpecΓ, Exists.intro, CategoryTheory.CategoryStruct.comp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
refine_1 :
  Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
refine_2 : (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
refine ⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
refine_1 : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (X.presheaf.germ W x hxW) ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
refine_1₁ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (φ' ≫ X.presheaf.germ W x hxW) ≫ IsAffineOpen.fromSpec hV
refine_1₂ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (Y.presheaf.germ V y hyV ≫ φ) ≫ IsAffineOpen.fromSpec hV
refine_1₃ :
  Spec.map φ ≫ Y.fromSpecStalk y = (Spec.map φ ≫ Spec.map (Y.presheaf.germ V y hyV)) ≫ IsAffineOpen.fromSpec hV
refine_1₄ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map φ ≫ Spec.map (Y.presheaf.germ V y hyV) ≫ IsAffineOpen.fromSpec hV
refine_1₅ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map φ ≫ IsAffineOpen.fromSpecStalk hV hyV
refine_1₆ refine_1₇ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map φ ≫ Y.fromSpecStalk y
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV

Tactic:
rw [W.fromSpecStalkOfMem_toSpecΓ_assoc x hxW, ← Spec.map_comp_assoc, ← h₁,
      Spec.map_comp, Category.assoc, ← IsAffineOpen.fromSpecStalk,
      IsAffineOpen.fromSpecStalk_eq_fromSpecStalk]

Premises used: CategoryTheory.Category.assoc, AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Spec.map_comp, AlgebraicGeometry.IsAffineOpen.fromSpecStalk, AlgebraicGeometry.Scheme.Opens.fromSpecStalkOfMem_toSpecΓ_assoc, AlgebraicGeometry.IsAffineOpen.fromSpecStalk_eq_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
refine_2 : W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
⊢ (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
y : ↥Y
e : Eq (α := ↥S) (sX x : ↥S) (sY y : ↥S)
φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x
h : Scheme.Hom.stalkMap sY y ≫ φ = S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x
U : TopologicalSpace.Opens ↥S
hU : U ∈ S.affineOpens
hxU : Membership.mem (α := ↥S) (↑U : Set ↥S) (sX x : ↥S)
hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
V : Y.Opens
hV : V ∈ Y.affineOpens
hyV : y ∈ (↑V : Set ↥Y)
iVU : (↑V : Set ↥Y) ⊆ (sY ⁻¹ᵁ U).carrier
this :
  Scheme.Hom.appLE sY U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = Scheme.Hom.app sX U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU
W : X.Opens
hxW : x ∈ W
φ' : Γ(Y, V) ⟶ Γ(X, W)
i : W ≤ sX ⁻¹ᵁ U
hW : IsAffineOpen W
h₁ : Y.presheaf.germ V y hyV ≫ φ = φ' ≫ X.presheaf.germ W x hxW
h₂ : Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op = Scheme.Hom.appLE sY U V iVU ≫ φ'
refine_2 : W.toSpecΓ ≫ Spec.map φ' ≫ Spec.map (Scheme.Hom.appLE sY U V iVU) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
refine_2₁ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.appLE sY U V iVU ≫ φ') ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
refine_2₂ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
refine_2₃ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.appLE sX U W i) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
refine_2₄ : hW.isoSpec.hom ≫ Spec.map (Scheme.Hom.appLE sX U W i) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
refine_2₅ : hW.isoSpec.hom ≫ hW.fromSpec ≫ sX = W.ι ≫ sX
refine_2₆ : hW.fromSpec ≫ sX = hW.isoSpec.inv ≫ W.ι ≫ sX
refine_2₇ refine_2₈ : hW.fromSpec ≫ sX = hW.fromSpec ≫ sX
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX

Tactic:
rw [← IsAffineOpen.SpecMap_appLE_fromSpec sY hU hV iVU, ← Spec.map_comp_assoc, ← h₂,
      ← Scheme.Hom.appLE, ← hW.isoSpec_hom, IsAffineOpen.SpecMap_appLE_fromSpec sX hU hW i,
      ← Iso.eq_inv_comp, IsAffineOpen.isoSpec_inv_ι_assoc]

Premises used: AlgebraicGeometry.Spec.map_comp_assoc, AlgebraicGeometry.Scheme.Hom.appLE, CategoryTheory.Iso.eq_inv_comp, AlgebraicGeometry.IsAffineOpen.SpecMap_appLE_fromSpec, AlgebraicGeometry.IsAffineOpen.isoSpec_hom, AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
refine_3 :
  ∀
    (this :
      ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
        CategoryStruct.comp (Y :=
              Spec (Y.presheaf.stalk (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)))))
              (Spec.map (Scheme.stalkClosedPointTo φ))
              (Y.fromSpecStalk (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)))) =
            U.fromSpecStalkOfMem x hxU ≫ f ∧
          f ≫ sY = U.ι ≫ sX),
    ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
refine_1 : Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
refine_2 :
  Eq (α :=
    S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)) ⟶ X.presheaf.stalk x)
    (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
      Scheme.stalkClosedPointTo φ)
    (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x)
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
this :
  ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    CategoryStruct.comp (Y := Spec (Y.presheaf.stalk (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)))))
          (Spec.map (Scheme.stalkClosedPointTo φ))
          (Y.fromSpecStalk (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)))) =
        U.fromSpecStalkOfMem x hxU ≫ f ∧
      f ≫ sY = U.ι ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX

Tactic:
simpa only [Scheme.Spec_stalkClosedPointTo_fromSpecStalk] using this

Premises used: AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
refine_1 : Eq (α := ↥S) (sX x : ↥S) ((φ ≫ sY) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
refine_1₁ :
  Eq (α := ↥S) (sX x : ↥S) ((X.fromSpecStalk x ≫ sX) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
refine_1₂ :
  Eq (α := ↥S) (sX x : ↥S)
    (sX ((X.fromSpecStalk x) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥X) : ↥S)
refine_1₃ refine_1₄ : Eq (α := ↥S) (sX x : ↥S) (sX x : ↥S)
⊢ Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)

Tactic:
rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]

Premises used: AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint, AlgebraicGeometry.Scheme.Hom.comp_apply
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y S : Scheme
sX : X ⟶ S
sY : Y ⟶ S
inst : LocallyOfFiniteType sY
x : ↥X
inst_1 : X.IsGermInjectiveAt x
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
refine_2 :
  Eq (α :=
    Spec (X.presheaf.stalk x) ⟶
      Spec (S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y))))
    (Spec.map
      (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
        Scheme.stalkClosedPointTo φ))
    (Spec.map (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x))
⊢ Eq (α :=
    S.presheaf.stalk (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y)) ⟶ X.presheaf.stalk x)
    (Scheme.Hom.stalkMap sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u))) ≫
      Scheme.stalkClosedPointTo φ)
    (S.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap sX x)

Tactic:
apply Spec.map_injective

Premises used: AlgebraicGeometry.Spec.map_injective