awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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 φ ≫ IsAffineOpen.fromSpecStalk hV hyV
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
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
⊢ 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.fromSpecStalk y
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 ≫ φ'
⊢ (W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV) ≫ sY = W.ι ≫ sX
have refine_2 : W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
Tactic: simp only [Category.assoc]
-- 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 ≫ φ'
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2 : W.toSpecΓ ≫ Spec.map φ' ≫ Spec.map (Scheme.Hom.appLE sY U V iVU) ≫ IsAffineOpen.fromSpec hU = 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]
-- 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_2 : W.toSpecΓ ≫ Spec.map φ' ≫ Spec.map (Scheme.Hom.appLE sY U V iVU) ≫ IsAffineOpen.fromSpec hU = W.ι ≫ sX
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₁ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.appLE sY U V iVU ≫ φ') ≫ IsAffineOpen.fromSpec hU = 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₂ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.app sX U ≫ X.presheaf.map i.hom.op) ≫ IsAffineOpen.fromSpec hU = 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₃ : W.toSpecΓ ≫ Spec.map (Scheme.Hom.appLE sX U W i) ≫ IsAffineOpen.fromSpec hU = 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₄ : hW.isoSpec.hom ≫ Spec.map (Scheme.Hom.appLE sX U W i) ≫ IsAffineOpen.fromSpec hU = 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₅ : hW.isoSpec.hom ≫ hW.fromSpec ≫ sX = 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₆ : hW.fromSpec ≫ sX = hW.isoSpec.inv ≫ 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]
-- 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_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
⊢ W.toSpecΓ ≫ Spec.map φ' ≫ IsAffineOpen.fromSpec hV ≫ sY = W.ι ≫ sX
have refine_2₇ : hW.fromSpec ≫ sX = hW.fromSpec ≫ 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]
-- 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
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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
Tactic: have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
-- 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
φ : 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
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have refine_1 : Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
Tactic: have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
-- 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
φ : 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)
⊢ ∃ (U : X.Opens) (hxU : x ∈ U) (f : (↑U : Scheme) ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX
have 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 sorry ≫ Scheme.Hom.stalkMap sX x)
Tactic: have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
-- 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
φ : Spec (X.presheaf.stalk x) ⟶ Y
h : φ ≫ sY = X.fromSpecStalk x ≫ sX
⊢ Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
have refine_1 : Eq (α := ↥S) (sX x : ↥S) ((φ ≫ sY) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]
-- 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
φ : 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)
⊢ Eq (α := ↥S) (sX x : ↥S) (sY (φ (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥Y) : ↥S)
have refine_1₁ : Eq (α := ↥S) (sX x : ↥S) ((X.fromSpecStalk x ≫ sX) (IsLocalRing.closedPoint (↑(X.presheaf.stalk x) : Type u)) : ↥S)
Tactic: rw [← Scheme.Hom.comp_apply, h, Scheme.Hom.comp_apply, Scheme.fromSpecStalk_closedPoint]