awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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 ⋯
⊢ φ =
    CommRingCat.ofHom
        (e.symm.toRingHom.comp
          ((CommRingCat.Hom.hom φ).codRestrict
            (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')))
            ⋯)) ≫
      X.presheaf.germ V' x hxV'
have refine_1 : ∀ (a : (↑A : Type u)),
  Eq (α := (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom φ : (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u)) a :
      (↑(X.presheaf.stalk x) : Type u))
    ((CommRingCat.Hom.hom
            (CommRingCat.ofHom
                (e.symm.toRingHom.comp
                  ((CommRingCat.Hom.hom φ).codRestrict
                    (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')))
                    sorry)) ≫
              X.presheaf.germ V' x hxV') :
          (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
        a :
      (↑(X.presheaf.stalk x) : Type u))
Tactic: ext a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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 ⋯
⊢ φRX ≫ X.presheaf.map ⋯.hom.op =
    φRA ≫
      CommRingCat.ofHom
        (e.symm.toRingHom.comp
          ((CommRingCat.Hom.hom φ).codRestrict
            (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')))
            ⋯))
have refine_2 : ∀ (a : (↑R : Type u)),
  Eq (α := (↑Γ(X, V') : Type u))
    ((CommRingCat.Hom.hom (φRX ≫ X.presheaf.map sorry.hom.op) : (a : (↑R : Type u)) → (↑Γ(X, V') : Type u)) a :
      (↑Γ(X, V') : Type u))
    ((CommRingCat.Hom.hom
            (φRA ≫
              CommRingCat.ofHom
                (e.symm.toRingHom.comp
                  ((CommRingCat.Hom.hom φ).codRestrict
                    (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')))
                    sorry))) :
          (a : (↑R : Type u)) → (↑Γ(X, V') : Type u))
        a :
      (↑Γ(X, V') : Type u))
Tactic: ext a
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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 : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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
Tactic: obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
    S.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (sX x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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)
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have hyU : Membership.mem (α := ↥S) U (sY y : ↥S)
Tactic: have hyU : sY y ∈ U := e ▸ hxU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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)
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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
Tactic: obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hyV, iVU⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open hyU (sY ⁻¹ᵁ U).2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have rw : S.presheaf.germ U (sY y) sorry ≫ S.presheaf.stalkSpecializes sorry ≫ Scheme.Hom.stalkMap sX x =
  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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
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
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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
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
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
have refine_1 : Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
Tactic: refine ⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y),
    Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have refine_2 : (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX
Tactic: refine ⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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 ≫ φ'
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
have refine_1 : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (X.presheaf.germ W x hxW) ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
have refine_1₁ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (φ' ≫ X.presheaf.germ W x hxW) ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
have refine_1₂ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map (Y.presheaf.germ V y hyV ≫ φ) ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
have refine_1₃ : Spec.map φ ≫ Y.fromSpecStalk y = (Spec.map φ ≫ Spec.map (Y.presheaf.germ V y hyV)) ≫ 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]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
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
⊢ Spec.map φ ≫ Y.fromSpecStalk y = W.fromSpecStalkOfMem x hxW ≫ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV
have refine_1₄ : Spec.map φ ≫ Y.fromSpecStalk y = Spec.map φ ≫ Spec.map (Y.presheaf.germ V y hyV) ≫ 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]