awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
⊢ J ≤
    Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)))
have rw : (↑s : Set (↑R : Type u)) ⊆
  (↑(Submodule.annihilator (M := (↑R : Type u))
        ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) sorry) : (↑R : Type u)))) :
    Set (↑R : Type u))
Tactic: rw [← hs, Ideal.span_le]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
i : (↑R : Type u)
hi : i ∈ (↑s : Set (↑R : Type u))
⊢ i ∈
    (↑(Submodule.annihilator (M := (↑R : Type u))
          ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)))) :
      Set (↑R : Type u))
have rw : Membership.mem (γ := Ideal (↑R : Type u)) (Submodule.annihilator (M := (↑R : Type u)) ((↑R : Type u) ∙ i))
  (∏ i ∈ s.attach, (↑(f (↑i : (↑R : Type u)) sorry) : (↑R : Type u)))
Tactic: rw [SetLike.mem_coe, Submodule.mem_annihilator_span_singleton, smul_eq_mul,
    mul_comm, ← smul_eq_mul, ← Submodule.mem_annihilator_span_singleton, Submonoid.coe_finsetProd]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
i : (↑R : Type u)
hi : i ∈ (↑s : Set (↑R : Type u))
⊢ Membership.mem (γ := Ideal (↑R : Type u)) (Submodule.annihilator (M := (↑R : Type u)) ((↑R : Type u) ∙ i))
    (∏ i ∈ s.attach, (↑(f (↑i : (↑R : Type u)) ⋯) : (↑R : Type u)))
have refine : Membership.mem (γ := Ideal (↑R : Type u)) (Submodule.annihilator (M := (↑R : Type u)) ((↑R : Type u) ∙ i))
  (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) sorry) : (↑R : Type u))
Tactic: refine Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y S : Scheme
f_1 : X ⟶ Y
sX : X ⟶ S
sY : Y ⟶ S
R_1 A : CommRingCat
inst : IsLocallyNoetherian X
R : CommRingCat
hR : IsNoetherianRing.{u} (↑R : Type u)
I : Ideal (↑R : Type u)
hI : I.IsPrime
J : Ideal (↑R : Type u) :=
  RingHom.ker (F := (↑R : Type u) →+* Localization.AtPrime I) (algebraMap (↑R : Type u) (Localization.AtPrime I))
hJ : ∀ (x : (↑R : Type u)), x ∈ J ↔ ∃ (y : ↥I.primeCompl), (↑y : (↑R : Type u)) * x = 0
f : (x : (↑R : Type u)) → x ∈ J → ↥I.primeCompl
hf : ∀ (x : (↑R : Type u)) (a : x ∈ J), (↑(f x a) : (↑R : Type u)) * x = 0
s : Finset (↑R : Type u)
hs : Ideal.span (↑s : Set (↑R : Type u)) = J
hs' : (↑s : Set (↑R : Type u)) ⊆ (↑J : Set (↑R : Type u))
x y : (↑R : Type u)
e : y * x = 0
hy : y ∉ I
i : (↑R : Type u)
hi : i ∈ (↑s : Set (↑R : Type u))
⊢ Membership.mem (γ := Ideal (↑R : Type u)) (Submodule.annihilator (M := (↑R : Type u)) ((↑R : Type u) ∙ i))
    (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) ⋯) : (↑R : Type u))
have rw : (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) sorry) : (↑R : Type u)) * i = 0
Tactic: rw [Submodule.mem_annihilator_span_singleton, smul_eq_mul]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
have obtain : ∀ (V : Y.Opens) (hV : V ∈ Y.affineOpens) (hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)),
  ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
Tactic: obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hxV, -⟩ :=
    Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
have hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
Tactic: have hxV' : g x ∈ V := e ▸ hxV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
have obtain : ∀ (U : X.Opens) (hxU : x ∈ U),
  IsAffineOpen U →
    ∀ (hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V)
      (HU :
        Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
            (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))),
      ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
Tactic: obtain ⟨U, hxU, _, hUV, HU⟩ := X.exists_le_and_germ_injective x (f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V) ⟨hxV, hxV'⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
have refine : U.ι ≫ f = U.ι ≫ g
Tactic: refine ⟨U, hxU, ?_⟩
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ U.ι ≫ f = U.ι ≫ g
have rw : Scheme.Hom.resLE f V U sorry ≫ V.ι = Scheme.Hom.resLE g V U sorry ≫ V.ι
Tactic: rw [← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_left),
    ← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Scheme.Hom.resLE f V U ⋯ ≫ V.ι = Scheme.Hom.resLE g V U ⋯ ≫ V.ι
have e_a : Scheme.Hom.resLE f V U sorry = Scheme.Hom.resLE g V U sorry
Tactic: congr 1
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯
have this : IsAffine.{u} (↑V : Scheme)
Tactic: have : IsAffine V := hV
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯
have rw : Scheme.Hom.resLE f V U sorry ≫ Iso.hom (↑V : Scheme).isoSpec = Scheme.Hom.resLE g V U sorry ≫ Iso.hom (↑V : Scheme).isoSpec
Tactic: rw [← cancel_mono V.toScheme.isoSpec.hom]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ Iso.hom (↑V : Scheme).isoSpec = Scheme.Hom.resLE g V U ⋯ ≫ Iso.hom (↑V : Scheme).isoSpec
have simp : Eq.{u + 1} (α := (↑U : Scheme) ⟶ Spec Γ((↑V : Scheme), ⊤))
  ((↑U : Scheme).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U sorry ⁻¹ᵁ ⊤) sorry))
  ((↑U : Scheme).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U sorry ⁻¹ᵁ ⊤) sorry))
Tactic: simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Eq.{u + 1} (α := (↑U : Scheme) ⟶ Spec Γ((↑V : Scheme), ⊤))
    ((↑U : Scheme).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤) ⋯))
    ((↑U : Scheme).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U ⋯ ⁻¹ᵁ ⊤) ⋯))
have e_a : Eq (α := Γ((↑V : Scheme), ⊤) ⟶ Γ((↑U : Scheme), ⊤))
  (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U sorry ⁻¹ᵁ ⊤) sorry)
  (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U sorry ⁻¹ᵁ ⊤) sorry)
Tactic: congr 2
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
⊢ Eq (α := Γ((↑V : Scheme), ⊤) ⟶ Γ((↑U : Scheme), ⊤))
    (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤) ⋯)
    (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U ⋯ ⁻¹ᵁ ⊤) ⋯)
have e_a : U = U.ι ''ᵁ Scheme.Hom.resLE f V U sorry ⁻¹ᵁ ⊤
Tactic: apply this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this :
  ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ ⋯ = Scheme.Hom.appLE g V₀ U₀ ⋯
e_a : U = U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤
⊢ Eq (α := Γ((↑V : Scheme), ⊤) ⟶ Γ((↑U : Scheme), ⊤))
    (Scheme.Hom.appLE f (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤) ⋯)
    (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE g V U ⋯ ⁻¹ᵁ ⊤) ⋯)
have e_a₁ : V = V.ι ''ᵁ ⊤
Tactic: apply this
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this : IsAffine.{u} (↑V : Scheme)
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯
have e_a : ∀ (U₀ : X.Opens) (V₀ : Y.Opens) (eU : U = U₀) (eV : V = V₀), Scheme.Hom.appLE f V₀ U₀ sorry = Scheme.Hom.appLE g V₀ U₀ sorry
Tactic: suffices ∀ (U₀ V₀) (eU : U = U₀) (eV : V = V₀),
      f.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_left) =
        g.appLE V₀ U₀ (eU ▸ eV ▸ hUV.trans inf_le_right) by
    rw [← cancel_mono V.toScheme.isoSpec.hom]
    simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]
    congr 2
    apply this <;> simp
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (hypothesis)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this : IsAffine.{u} (↑V : Scheme)
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE g V U ⋯
have this₁ : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
Tactic: have := ConcreteCategory.mono_of_injective _ HU
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE g V U ⋯
have e_a : Eq (α := Γ(Y, V) ⟶ X.presheaf.stalk x) (Scheme.Hom.appLE f V U sorry ≫ X.presheaf.germ U x hxU)
  (Scheme.Hom.appLE g V U sorry ≫ X.presheaf.germ U x hxU)
Tactic: rw [← cancel_mono (X.presheaf.germ U x hxU)]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
H : Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x
V : Y.Opens
hV : V ∈ Y.affineOpens
hxV : Membership.mem (α := ↥Y) (↑V : Set ↥Y) (f x : ↥Y)
hxV' : Membership.mem (α := ↥Y) V (g x : ↥Y)
U : X.Opens
hxU : x ∈ U
left : IsAffineOpen U
hUV : U ≤ f ⁻¹ᵁ V ⊓ g ⁻¹ᵁ V
HU :
  Function.Injective (α := (↑(X.presheaf.obj (Opposite.op 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) (X.presheaf.germ U x hxU)) :
      (a : (↑(X.presheaf.obj (Opposite.op U)) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
this_1 : IsAffine.{u} (↑V : Scheme)
this : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
⊢ Eq (α := Γ(Y, V) ⟶ X.presheaf.stalk x) (Scheme.Hom.appLE f V U ⋯ ≫ X.presheaf.germ U x hxU)
    (Scheme.Hom.appLE g V U ⋯ ≫ X.presheaf.germ U x hxU)
have e_a : Y.presheaf.germ V (f x) sorry ≫ Y.presheaf.stalkSpecializes sorry ≫ Scheme.Hom.stalkMap g x =
  Y.presheaf.germ V (g x) sorry ≫ Scheme.Hom.stalkMap g x
Tactic: simp only [Scheme.Hom.appLE, Category.assoc, X.presheaf.germ_res', ← Scheme.Hom.germ_stalkMap, H]
-- Lean 4 proof step from Mathlib.AlgebraicGeometry.SpreadingOut (goal)
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g
have e₁ : Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)
Tactic: fapply spread_out_unique_of_isGermInjective