awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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
rw :
  (↑s : Set (↑R : Type u)) ⊆
    (↑(Submodule.annihilator (M := (↑R : Type u))
          ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)))) :
      Set (↑R : Type u))
⊢ J ≤
    Submodule.annihilator (M := (↑R : Type u))
      ((↑R : Type u) ∙ (↑(∏ x ∈ s.attach, f (↑x : (↑R : Type u)) ⋯) : (↑R : Type u)))

Tactic:
rw [← hs, Ideal.span_le]

Premises used: Ideal.span_le
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
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)) ⋯) : (↑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))

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]

Premises used: Submonoid.coe_finsetProd, SetLike.mem_coe, mul_comm, smul_eq_mul, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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)))

Tactic:
Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_

Premises used: Finset.dvd_prod_of_mem, Finset.mem_attach, Ideal.mem_of_dvd, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
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)) ⋯) : (↑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)))

Tactic:
refine Ideal.mem_of_dvd _ (Finset.dvd_prod_of_mem _ (s.mem_attach ⟨i, hi⟩)) ?_

Premises used: Finset.dvd_prod_of_mem, Finset.mem_attach, Ideal.mem_of_dvd, Subtype.mk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
rw : (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) ⋯) : (↑R : Type u)) * i = 0
⊢ 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))

Tactic:
rw [Submodule.mem_annihilator_span_singleton, smul_eq_mul]

Premises used: smul_eq_mul, Submodule.mem_annihilator_span_singleton
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
⊢ (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) ⋯) : (↑R : Type u)) * i = 0

Tactic:
hf i _
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
⊢ (↑(f (↑(Subtype.mk (p := fun (x : (↑R : Type u)) ↦ x ∈ s) i hi) : (↑R : Type u)) ⋯) : (↑R : Type u)) * i = 0

Tactic:
exact hf i _
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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
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
⊢ ∃ (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

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, AlgebraicGeometry.Scheme.Opens, DFunLike.coe, rfl, TopologicalSpace.IsTopologicalBasis.exists_subset_of_mem_open
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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)
⊢ Membership.mem (α := ↥Y) V (g x : ↥Y)

Tactic:
have hxV' : g x ∈ V := e ▸ hxV
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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)
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
⊢ ∃ (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'⟩

Premises used: AlgebraicGeometry.LocallyRingedSpace.Hom.toHom, AlgebraicGeometry.Scheme.Hom.toLRSHom', And.intro, AlgebraicGeometry.PresheafedSpace.Hom.base, TopologicalSpace.Opens.map, AlgebraicGeometry.Scheme.exists_le_and_germ_injective, CategoryTheory.Functor.obj, Min.min
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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

Tactic:
⟨U, hxU, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
refine : U.ι ≫ f = U.ι ≫ g
⊢ ∃ (U : X.Opens), x ∈ U ∧ U.ι ≫ f = U.ι ≫ g

Tactic:
refine ⟨U, hxU, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
rw : Scheme.Hom.resLE f V U ⋯ ≫ V.ι = Scheme.Hom.resLE g V U ⋯ ≫ V.ι
⊢ U.ι ≫ f = U.ι ≫ g

Tactic:
rw [← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_left),
    ← Scheme.Hom.resLE_comp_ι _ (hUV.trans inf_le_right)]

Premises used: inf_le_right, AlgebraicGeometry.Scheme.Hom.resLE_comp_ι, inf_le_left, LE.le.trans
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
e_a : Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯
⊢ Scheme.Hom.resLE f V U ⋯ ≫ V.ι = Scheme.Hom.resLE g V U ⋯ ≫ V.ι

Tactic:
congr 1
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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))
⊢ IsAffine.{u} (↑V : Scheme)

Tactic:
have : IsAffine V := hV
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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₀ ⋯
rw : Scheme.Hom.resLE f V U ⋯ ≫ Iso.hom (↑V : Scheme).isoSpec = Scheme.Hom.resLE g V U ⋯ ≫ Iso.hom (↑V : Scheme).isoSpec
⊢ Scheme.Hom.resLE f V U ⋯ = Scheme.Hom.resLE g V U ⋯

Tactic:
rw [← cancel_mono V.toScheme.isoSpec.hom]

Premises used: AlgebraicGeometry.Scheme.isoSpec, CategoryTheory.cancel_mono, CategoryTheory.Iso.hom, AlgebraicGeometry.Scheme.Opens.toScheme
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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₀ ⋯
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 ⋯ ⁻¹ᵁ ⊤) ⋯))
    ((↑U : Scheme).toSpecΓ ≫ Spec.map (Scheme.Hom.appLE g (V.ι ''ᵁ ⊤) (U.ι ''ᵁ Scheme.Hom.resLE 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

Tactic:
simp only [Scheme.isoSpec, asIso_hom, Scheme.toSpecΓ_naturality,
      Scheme.Hom.app_eq_appLE, Scheme.Hom.resLE_appLE]

Premises used: AlgebraicGeometry.Scheme.toSpecΓ_naturality, AlgebraicGeometry.Scheme.isoSpec, AlgebraicGeometry.Scheme.Hom.app_eq_appLE, CategoryTheory.asIso_hom, AlgebraicGeometry.Scheme.Hom.resLE_appLE
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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 :
  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 ⋯ ⁻¹ᵁ ⊤) ⋯)
⊢ 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 ⋯ ⁻¹ᵁ ⊤) ⋯))

Tactic:
congr 2
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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 ⋯ ⁻¹ᵁ ⊤
e_a₁ : V = V.ι ''ᵁ ⊤
⊢ 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 ⋯ ⁻¹ᵁ ⊤) ⋯)

Tactic:
apply this
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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₀ ⋯
⊢ U = U.ι ''ᵁ Scheme.Hom.resLE f V U ⋯ ⁻¹ᵁ ⊤

Tactic:
simp
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
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₀ ⋯
⊢ V = V.ι ''ᵁ ⊤

Tactic:
simp