awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : IsAffine.{u} (↑V : Scheme)
e_a :
  ∀ (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 ⋯

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
-- 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 : IsAffine.{u} (↑V : Scheme)
⊢ Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)

Tactic:
have := ConcreteCategory.mono_of_injective _ HU
-- 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 : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
e_a :
  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)
⊢ Scheme.Hom.appLE f V U ⋯ = Scheme.Hom.appLE g V U ⋯

Tactic:
rw [← cancel_mono (X.presheaf.germ U x hxU)]

Premises used: CategoryTheory.cancel_mono, TopCat.Presheaf.germ, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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 : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
e_a :
  Y.presheaf.germ V (f x) ⋯ ≫ Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x =
    Y.presheaf.germ V (g x) ⋯ ≫ Scheme.Hom.stalkMap g x
⊢ 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)

Tactic:
simp only [Scheme.Hom.appLE, Category.assoc, X.presheaf.germ_res', ← Scheme.Hom.germ_stalkMap, H]

Premises used: CategoryTheory.Category.assoc, TopCat.Presheaf.germ_res', AlgebraicGeometry.Scheme.Hom.appLE, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.Scheme.Hom.germ_stalkMap, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- 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 : Mono (Y := X.presheaf.stalk x) (X.presheaf.germ U x hxU)
⊢ Y.presheaf.germ V (f x) ⋯ ≫ Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x =
    Y.presheaf.germ V (g x) ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
simp only [TopCat.Presheaf.germ_stalkSpecializes_assoc, Scheme.Hom.germ_stalkMap]

Premises used: TopCat.Presheaf.germ_stalkSpecializes_assoc, AlgebraicGeometry.Scheme.Hom.germ_stalkMap
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
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

Tactic:
fapply spread_out_unique_of_isGermInjective

Premises used: AlgebraicGeometry.spread_out_unique_of_isGermInjective
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Eq (α := ↥Y) (f x : ↥Y) (g x : ↥Y)

Tactic:
simpa using congr($e (IsLocalRing.closedPoint _))
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
H : Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)
⊢ Scheme.Hom.stalkMap f x = Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x

Tactic:
apply Spec.map_injective

Premises used: AlgebraicGeometry.Spec.map_injective
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
H :
  Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) =
    CategoryStruct.comp (Y := Spec (Y.presheaf.stalk (f x)))
      (Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)) (Y.fromSpecStalk (f x))
⊢ Spec.map (Scheme.Hom.stalkMap f x) = Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)

Tactic:
rw [← cancel_mono (Y.fromSpecStalk _)]

Premises used: CategoryTheory.cancel_mono, AlgebraicGeometry.Scheme.fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X Y : Scheme
x : ↥X
inst : X.IsGermInjectiveAt x
f g : X ⟶ Y
e : X.fromSpecStalk x ≫ f = X.fromSpecStalk x ≫ g
⊢ Spec.map (Scheme.Hom.stalkMap f x) ≫ Y.fromSpecStalk (f x) =
    CategoryStruct.comp (Y := Spec (Y.presheaf.stalk (f x)))
      (Spec.map (Y.presheaf.stalkSpecializes ⋯ ≫ Scheme.Hom.stalkMap g x)) (Y.fromSpecStalk (f x))

Tactic:
simpa [Scheme.SpecMap_stalkSpecializes_fromSpecStalk]

Premises used: AlgebraicGeometry.Scheme.SpecMap_stalkSpecializes_fromSpecStalk
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
hφRA : (CommRingCat.Hom.hom φRA).FiniteType
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
obtain :
  ∀ (s : Finset (↑A : Type u))
    (hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤),
    ∃ (V : X.Opens) (hxV : x ∈ V),
      V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
⊢ ∃ (V : X.Opens) (hxV : x ∈ V),
    V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))

Tactic:
obtain ⟨s, hs⟩ := hφRA
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
choose :
  ∀ (W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X) (hxW : ∀ (t : (↑A : Type u)), x ∈ W t)
    (f :
      (t : (↑A : Type u)) →
        ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
          (X.presheaf.obj (Opposite.op (W t))))
    (hf :
      ∀ (t : (↑A : Type u)),
        Eq (α := (↑(X.presheaf.stalk x) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
                (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
              (f t) :
            (↑(X.presheaf.stalk x) : Type u))
          ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
                  CommRingCat.carrier) φ :
                (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
              t :
            (↑(X.presheaf.stalk x) : Type u))),
    ∃ (V : X.Opens) (hxV : x ∈ V),
      V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))
⊢ ∃ (V : X.Opens) (hxV : x ∈ V),
    V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))

Tactic:
choose W hxW f hf using fun t ↦ X.presheaf.exists_germ_eq (φ t)

Premises used: CategoryTheory.ConcreteCategory.hom, TopCat.Presheaf.exists_germ_eq, AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace, AlgebraicGeometry.PresheafedSpace.presheaf, AlgebraicGeometry.SheafedSpace.toPresheafedSpace, DFunLike.coe, AlgebraicGeometry.Scheme.toLocallyRingedSpace
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
rw : x ∈ s.inf (SetLike.coe ∘ W) ∩ (↑U : Set ↥X)
⊢ x ∈ s.inf W ⊓ U

Tactic:
rw [← SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_finset_inf]

Premises used: TopologicalSpace.Opens.coe_finset_inf, SetLike.mem_coe, TopologicalSpace.Opens.coe_inf
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
⊢ x ∈ s.inf (SetLike.coe ∘ W)

Tactic:
simpa using fun x _ ↦ hxW x
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
⊢ x ∈ s.inf (SetLike.coe ∘ W) ∩ (↑U : Set ↥X)

Tactic:
exact ⟨by simpa using fun x _ ↦ hxW x, hxU⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
⊢ x ∈ s.inf W ⊓ U

Tactic:
have H : x ∈ s.inf W ⊓ U := by
    rw [← SetLike.mem_coe, TopologicalSpace.Opens.coe_inf, TopologicalSpace.Opens.coe_finset_inf]
    exact ⟨by simpa using fun x _ ↦ hxW x, hxU⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
H : x ∈ s.inf W ⊓ U
⊢ ∃ (V : X.Opens) (hxV : x ∈ V),
    V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))

Tactic:
⟨s.inf W ⊓ U, H, inf_le_right, ?_⟩

Premises used: inf_le_right, And.intro, Exists.intro, Finset.inf, Min.min
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
H : x ∈ s.inf W ⊓ U
refine : (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H))
⊢ ∃ (V : X.Opens) (hxV : x ∈ V),
    V ≤ U ∧ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ V x hxV))

Tactic:
refine ⟨s.inf W ⊓ U, H, inf_le_right, ?_⟩
-- Module: Mathlib.AlgebraicGeometry.SpreadingOut
Goal:
X : Scheme
R A : CommRingCat
U : X.Opens
x : ↥X
hxU : x ∈ U
φ : A ⟶ X.presheaf.stalk x
φRA : R ⟶ A
φRX : R ⟶ Γ(X, U)
e : φRA ≫ φ = φRX ≫ X.presheaf.germ U x hxU
this_1 : Algebra (↑R : Type u) (↑A : Type u) := (CommRingCat.Hom.hom φRA).toAlgebra
s : Finset (↑A : Type u)
hs : Eq (α := Subalgebra (↑R : Type u) (↑A : Type u)) (Algebra.adjoin (↑R : Type u) (↑s : Set (↑A : Type u))) ⊤
W : (t : (↑A : Type u)) → TopologicalSpace.Opens ↥X
hxW : ∀ (t : (↑A : Type u)), x ∈ W t
f :
  (t : (↑A : Type u)) →
    ToType (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC := CommRingCat.carrier)
      (X.presheaf.obj (Opposite.op (W t)))
hf :
  ∀ (t : (↑A : Type u)),
    Eq (α := (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) (Y := X.presheaf.stalk x) (X.presheaf.germ (W t) x ⋯) :
            (a : (↑(X.presheaf.obj (Opposite.op (W t))) : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          (f t) :
        (↑(X.presheaf.stalk x) : Type u))
      ((ConcreteCategory.hom (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
              CommRingCat.carrier) φ :
            (a : (↑A : Type u)) → (↑(X.presheaf.stalk x) : Type u))
          t :
        (↑(X.presheaf.stalk x) : Type u))
H : x ∈ s.inf W ⊓ U
this_2 : Algebra (↑R : Type u) (↑Γ(X, U) : Type u) := (CommRingCat.Hom.hom φRX).toAlgebra
this_3 : Algebra (↑R : Type u) (↑(X.presheaf.stalk x) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (φRX ≫ X.presheaf.germ U x hxU))
this : Algebra (↑R : Type u) (↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) : Type u) :=
  RingHom.toAlgebra (CommRingCat.Hom.hom (φRX ≫ X.presheaf.map (Quiver.Hom.op (homOfLE ⋯))))
φ' : (↑A : Type u) →ₐ[(↑R : Type u)] (↑(X.presheaf.stalk x) : Type u) :=
  let __src := CommRingCat.Hom.hom φ;
  { toRingHom := __src, commutes' := ⋯ }
ψ : (↑Γ(X, s.inf W ⊓ U) : Type u) →ₐ[(↑R : Type u)] (↑(X.presheaf.stalk x) : Type u) :=
  let __src : (↑(X.presheaf.obj (Opposite.op (s.inf W ⊓ U))) : Type u) →+* (↑(X.presheaf.stalk x) : Type u) :=
    CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H);
  { toRingHom := __src, commutes' := ⋯ }
change : φ'.range ≤ ψ.range
⊢ (CommRingCat.Hom.hom φ).range ≤ RingHom.range (CommRingCat.Hom.hom (X.presheaf.germ (s.inf W ⊓ U) x H))

Tactic:
change AlgHom.range φ' ≤ AlgHom.range ψ

Premises used: AlgHom.range