mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁷ : CommRing R
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
S : Type u
inst✝² : CommRing S
N : Type u
inst✝¹ : AddCommGroup N
inst✝ : Module S N
σ : R →+* S
f : M →ₛₗ[σ] N
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap σ ⁻¹' U.carrier
r : R
m : (structureSheafInType R M).obj.obj (op U)
x✝ : ↥(unop (op V))
⊢ (algebraMap S S) (σ r) • (Localizations.comapFun f ↑x✝) (↑m ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩) =
    (algebraMap S S) (σ r) • (Localizations.comapFun f ↑x✝) (↑m ⟨PrimeSpectrum.comap σ ↑x✝, ⋯⟩)

Tactic:
]

Goal state after:
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v, u₁} C
C' : Type u₂
inst✝³ : Category.{v, u₂} C'
D : GlueData C
F : C ⥤ C'
inst✝² : HasMulticoequalizer D.diagram
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
i : D.J
⊢ (D.mapGlueData F).ι i = (D.mapGlueData F).ι i

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) 1) x✝ = ↑1 x✝

Tactic:
simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ (Localization.localRingHom (Ideal.comap f (↑x✝).asIdeal) (↑x✝).asIdeal f ⋯) (↑1 ⟨PrimeSpectrum.comap f ↑x✝, ⋯⟩) =
    ↑1 x✝
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) (r * s)) p =
    ↑((comapₗ f.toSemilinearMap U V hUV) r) p * ↑((comapₗ f.toSemilinearMap U V hUV) s) p

Tactic:
simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
r s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑(r * s) ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) =
    (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑r ⟨PrimeSpectrum.comap f ↑p, ⋯⟩) *
      (Localization.localRingHom (Ideal.comap f (↑p).asIdeal) (↑p).asIdeal f ⋯) (↑s ⟨PrimeSpectrum.comap f ↑p, ⋯⟩)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ ↑((comapₗ f.toSemilinearMap U V hUV) 0) x✝ = ↑0 x✝

Tactic:
simp only [comapₗ_eq_localRingHom, PrimeSpectrum.comap_asIdeal]

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f✝ : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
x✝ : ↥(unop (op V))
⊢ (Localization.localRingHom (Ideal.comap f (↑x✝).asIdeal) (↑x✝).asIdeal f ⋯) (↑0 ⟨PrimeSpectrum.comap f ↑x✝, ⋯⟩) =
    ↑0 x✝
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
    Submodule.restrictScalars (↑Γ(X, U))
      (Ideal.map (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I)

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : ↑Γ(X, U)
I : Ideal ↑Γ(X, U)
H :
  ∀ (x : ↥X) (h : x ∈ U),
    (ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I
this✝ : (x : ↥(Spec Γ(X, U))) → Algebra ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec x)) :=
  fun x ↦ X.presheaf.algebra_section_stalk ((Scheme.Hom.toLRSHom hU.isoSpec.inv).base.hom' x)
this :
  ∀ (P : Ideal ↑Γ(X, U)) [hP : P.IsPrime],
    IsLocalization.AtPrime (↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := hP }))) P
P : Ideal ↑Γ(X, U)
hP : P.IsMaximal
⊢ (Algebra.linearMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) s ∈
    Submodule.restrictScalars (↑Γ(X, U))
      (Ideal.map (algebraMap ↑Γ(X, U) ↑(X.presheaf.stalk (hU.fromSpec { asIdeal := P, isPrime := ⋯ }))) I)
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (LocalizedModule.mk a ⟨b, ⋯⟩) =
    LocalizedModule.mk (f a) ⟨f b, ⋯⟩

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
V : Opens ↑(PrimeSpectrum.Top S)
hUV : V.carrier ⊆ PrimeSpectrum.comap f ⁻¹' U.carrier
a b : R
hb : ∀ x ∈ U, b ∈ x.asIdeal.primeCompl
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑p).asIdeal (↑p).asIdeal f ⋯) (LocalizedModule.mk a ⟨b, ⋯⟩) =
    LocalizedModule.mk (f a) ⟨f b, ⋯⟩
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨PrimeSpectrum.comap (RingHom.id R) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
iVU : V ⟶ U
s : ↑((structureSheaf R).obj.obj (op U))
p : ↥(unop (op V))
⊢ (Localization.localRingHom (PrimeSpectrum.comap (RingHom.id R) ↑p).asIdeal (↑p).asIdeal (RingHom.id R) ⋯)
      (↑s ⟨PrimeSpectrum.comap (RingHom.id R) ↑p, ⋯⟩) =
    ↑((CommRingCat.Hom.hom ((structureSheaf R).obj.map iVU.op)) s) p
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ (fun x ↦ x) ⁻¹' V.carrier

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
p : ↑(PrimeSpectrum.Top R)
hpV : p ∈ V.carrier
⊢ p ∈ (fun x ↦ x) ⁻¹' V.carrier
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ (structureSheaf R).obj.obj (op V) = (structureSheaf R).obj.obj (op V)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U V : Opens ↑(PrimeSpectrum.Top R)
hUV : U = V
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = CommRingCat.Hom.hom (eqToHom ⋯)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ (fun x ↦ x) ⁻¹' U.carrier

Tactic:
]

Goal state after:
R M A : Type u
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : CommRing A
inst✝⁵ : Algebra R A
S✝ : Type u
inst✝⁴ : CommRing S✝
N : Type u
inst✝³ : AddCommGroup N
inst✝² : Module S✝ N
σ : R →+* S✝
f : M →ₛₗ[σ] N
S : Type u
inst✝¹ : CommRing S
P : Type u
inst✝ : CommRing P
U : Opens ↑(PrimeSpectrum.Top R)
p : ↑(PrimeSpectrum.Top R)
hpU : p ∈ U.carrier
⊢ p ∈ (fun x ↦ x) ⁻¹' U.carrier
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).obj.obj (op U))

Tactic:
]

Goal state after:
R : Type u
inst✝ : CommRing R
U : Opens ↑(PrimeSpectrum.Top R)
⊢ CommRingCat.Hom.hom (eqToHom ⋯) = RingHom.id ↑((structureSheaf R).obj.obj (op U))
Module: Mathlib.AlgebraicGeometry.StructureSheaf

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑x).asIdeal (↑x).asIdeal f ⋯)
      (↑((algebraMap R ↑((structureSheaf R).obj.obj (op U))) x✝) ⟨PrimeSpectrum.comap f ↑x, ⋯⟩) =
    ↑((algebraMap S
            ↑((structureSheaf S).obj.obj
                (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
          (f x✝))
      x

Tactic:
]

Goal state after:
R : Type u
inst✝¹ : CommRing R
S : Type u
inst✝ : CommRing S
f : R →+* S
U : Opens ↑(PrimeSpectrum.Top R)
x✝ : ↑(CommRingCat.of R)
x : ↥(unop (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U)))
⊢ (Localization.localRingHom (PrimeSpectrum.comap f ↑x).asIdeal (↑x).asIdeal f ⋯)
      (↑((algebraMap R ↑((structureSheaf R).obj.obj (op U))) x✝) ⟨PrimeSpectrum.comap f ↑x, ⋯⟩) =
    ↑((algebraMap S
            ↑((structureSheaf S).obj.obj
                (op ((Opens.comap { toFun := PrimeSpectrum.comap f, continuous_toFun := ⋯ }) U))))
          (f x✝))
      x
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
                (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
            (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)) ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.inv =
    Scheme.Hom.stalkMap f x

Tactic:
]

Goal state after:
case refine_3
X Y : Scheme
U✝ : X.Opens
hU✝ : IsAffineOpen U✝
f✝ : ↑Γ(X, U✝)
f : X ⟶ Y
x : ↥X
U : Y.Opens
hU : IsAffineOpen U
V : X.Opens
hV : IsAffineOpen V
hVU : V ≤ f ⁻¹ᵁ U
hx : x ∈ V
this✝² : Algebra ↑(Y.presheaf.obj (op U)) ↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩) := Y.presheaf.algebra_section_stalk ⟨f x, ⋯⟩
this✝¹ : IsLocalization.AtPrime (↑(Y.presheaf.stalk ↑⟨f x, ⋯⟩)) (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal
this✝ : Algebra ↑(X.presheaf.obj (op V)) ↑(X.presheaf.stalk ↑⟨x, hx⟩) := X.presheaf.algebra_section_stalk ⟨x, hx⟩
this : IsLocalization.AtPrime (↑(X.presheaf.stalk ↑⟨x, hx⟩)) (hV.primeIdealOf ⟨x, hx⟩).asIdeal
⊢ ((IsLocalization.algEquiv (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal.primeCompl (↑(Y.presheaf.stalk (f x)))
                (Localization.AtPrime (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal)).toRingEquiv.toCommRingCatIso.hom ≫
        CommRingCat.ofHom
          (Localization.localRingHom (hU.primeIdealOf ⟨f x, ⋯⟩).asIdeal (hV.primeIdealOf ⟨x, hx⟩).asIdeal
            (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V hVU)) ⋯)) ≫
      (IsLocalization.algEquiv (hV.primeIdealOf ⟨x, hx⟩).asIdeal.primeCompl (↑(X.presheaf.stalk x))
              (Localization.AtPrime (hV.primeIdealOf ⟨x, hx⟩).asIdeal)).toRingEquiv.toCommRingCatIso.inv =
    Scheme.Hom.stalkMap f x
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom (F.map (D.ι i))) y = (ConcreteCategory.hom (𝟙 (F.obj D.glued))) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x

Tactic:
]

Goal state after:
C : Type u₁
inst✝³ : Category.{v, u₁} C
D : GlueData C
inst✝² : HasMulticoequalizer D.diagram
F : C ⥤ Type v
inst✝¹ : PreservesColimit D.diagram.multispan F
inst✝ : ∀ (i j k : D.J), PreservesLimit (cospan (D.f i j) (D.f i k)) F
x : F.obj D.glued
e : F.obj D.glued ≅ (D.mapGlueData F).glued := D.gluedIso F
i : (D.mapGlueData F).J
y : (D.mapGlueData F).U i
eq : (ConcreteCategory.hom (F.map (D.ι i))) y = (ConcreteCategory.hom (𝟙 (F.obj D.glued))) x
⊢ ∃ i y, (ConcreteCategory.hom (F.map (D.ι i))) y = x
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ IsOpen (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
]

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
U : Set ↑D.glued
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen
        (⇑(ConcreteCategory.hom (colimit.ι (Discrete.functor D.diagram.right) j)) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) ⁻¹'
            ⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U)) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
]

Goal state after:
D : GlueData
U : Set ↑D.glued
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen
        (⇑(ConcreteCategory.hom (colimit.ι (Discrete.functor D.diagram.right) j)) ⁻¹'
          ⇑(ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) ⁻¹'
            ⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U)) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)
Module: Mathlib.CategoryTheory.GlueData

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v, u₁} C
C' : Type u₂
inst✝ : Category.{v, u₂} C'
D : GlueData' C
i j k : D.J
hij : ¬i = j
hik : ¬i = k
hjk : ¬j = k
this : j ≠ i
⊢ D.V i k hik = D.V i k hik

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
a b : (i : D.J) × ↑(D.U i)
x : ↑(D.V (a.fst, b.fst))
e₁ : (ConcreteCategory.hom (D.f a.fst b.fst)) x = a.snd
e₂ : (ConcreteCategory.hom (D.f b.fst a.fst)) ((ConcreteCategory.hom (D.t a.fst b.fst)) x) = b.snd
⊢ (ConcreteCategory.hom (D.f a.fst b.fst)) x = (ConcreteCategory.hom (D.f a.fst b.fst)) x

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i : D.J
a : ↑(D.U i)
j : D.J
b : ↑(D.U j)
k : D.J
c : ↑(D.U k)
x : ↑(D.V (⟨i, a⟩.fst, ⟨j, b⟩.fst))
e₁ : (ConcreteCategory.hom (D.f ⟨i, a⟩.fst ⟨j, b⟩.fst)) x = ⟨i, a⟩.snd
e₂ :
  (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨i, a⟩.fst)) ((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x) = ⟨j, b⟩.snd
y : ↑(D.V (⟨j, b⟩.fst, ⟨k, c⟩.fst))
e₃ : (ConcreteCategory.hom (D.f ⟨j, b⟩.fst ⟨k, c⟩.fst)) y = ⟨j, b⟩.snd
e₄ :
  (ConcreteCategory.hom (D.f ⟨k, c⟩.fst ⟨j, b⟩.fst)) ((ConcreteCategory.hom (D.t ⟨j, b⟩.fst ⟨k, c⟩.fst)) y) = ⟨k, c⟩.snd
z : ↑(pullback (D.f j i) (D.f j k)) :=
  (ConcreteCategory.hom (pullbackIsoProdSubtype (D.f j i) (D.f j k)).inv)
    ⟨((ConcreteCategory.hom (D.t ⟨i, a⟩.fst ⟨j, b⟩.fst)) x, y), ⋯⟩
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ⨆ f, X.basicOpen ↑f = U
⊢ ⇑hU.fromSpec ⁻¹' U.carrier = ⇑hU.fromSpec ⁻¹' U.carrier

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : (⨆ f, X.basicOpen ↑f).carrier ∩ ↑U = U.carrier ∩ ↑U
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : (⨆ f, X.basicOpen ↑f).carrier ∩ ↑U = U.carrier ∩ ↑U
⊢ ⨆ f, X.basicOpen ↑f = U
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j

Tactic:
]

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
⊢ D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = D.t' j i k ≫ pullback.snd (D.f i k) (D.f i j) ≫ D.f i j
Module: Mathlib.Topology.Gluing

Goal state before:
pp: D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j

Tactic:
]

Goal state after:
D : GlueData
i j k : D.J
z : ↑(pullback (D.f j i) (D.f j k))
e₂ :
  (ConcreteCategory.hom (D.f j i))
      ((ConcreteCategory.hom (D.t i j))
        ((ConcreteCategory.hom (D.t j i)) ((ConcreteCategory.hom (pullback.fst (D.f j i) (D.f j k))) z))) =
    (ConcreteCategory.hom (D.f j k)) ((ConcreteCategory.hom (pullback.snd (D.f j i) (D.f j k))) z)
h₁ : D.t' j i k ≫ pullback.fst (D.f i k) (D.f i j) ≫ D.f i k = pullback.fst (D.f j i) (D.f j k) ≫ D.t j i ≫ D.f i j
⊢ D.t' j i k ≫ D.t' i k j ≫ pullback.snd (D.f k j) (D.f k i) ≫ D.f k i =
    pullback.snd (D.f j i) (D.f j k) ≫ D.t j k ≫ D.f k j
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅
Module: Mathlib.AlgebraicGeometry.AffineScheme

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f

Tactic:
]

Goal state after:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ U ≤ ⨆ f, X.basicOpen ↑f ↔ U = ⨆ f, X.basicOpen ↑f