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

Goal state before:
pp: R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ (Spec R).presheaf.germ ⊤ ((Spec.map φ) (closedPoint ↑S)) trivial ≫ stalkClosedPointTo (Spec.map φ) =
    (ΓSpecIso R).hom ≫ φ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y.Hom Z
⊢ g.ker ≤ ker (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : X.Opens
hU : f (closedPoint ↑R) ∈ U
⊢ X.presheaf.germ U (f (closedPoint ↑R)) hU ≫ stalkClosedPointTo f =
    Hom.app f U ≫ (Functor.mapIso (Spec R).presheaf (eqToIso ⋯).op ≪≫ ΓSpecIso R).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f✝¹ : X ⟶ Y
U✝ V : X.Opens
hU✝ : IsAffineOpen U✝
hV : IsAffineOpen V
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
f✝ : Spec R ⟶ X
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
⊢ x ∈ U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : IsEmpty ↥X
U : ↑Y.affineOpens
x : ↑Γ(Y, ↑U)
x✝ : x ∈ ⊤.ideal U
⊢ x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
⊢ (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ker f = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsIso f
⊢ ker (inv f ≫ f ≫ g) ≤ ker g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ RingHom.ker (CommRingCat.Hom.hom (Hom.app f ↑⟨⊤, ⋯⟩)) ≤
    (ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))).ideal ⟨⊤, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝¹ : IsLocalRing ↑R
x : ↥X
f : X.presheaf.stalk x ⟶ R
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
U : X.Opens
hU : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) ∈ U
⊢ X.presheaf.germ U ((Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R)) hU ≫
      stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f✝ : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
x : ↥X
⊢ Inseparable ((X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x))) x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
U : TopologicalSpace.Opens ↥X
hxU : (X.fromSpecStalk x) (closedPoint ↑(X.presheaf.stalk x)) ∈ U
⊢ X.fromSpecStalk x = Spec.map (𝟙 (X.presheaf.stalk x)) ≫ X.fromSpecStalk x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
⊢ Hom.ker f = ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
x : ↥X
⊢ stalkClosedPointTo (X.fromSpecStalk x) = (X.presheaf.stalkCongr ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ (ker f).ideal ⟨U, hU⟩
hxs : f x ∈ Y.basicOpen s
this : x ∈ f ⁻¹ᵁ Y.basicOpen s
⊢ False

Tactic:
Scheme.preimage_basicOpen,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
s : ↑Γ(Y, U)
hs : s ∈ (ker f).ideal ⟨U, hU⟩
hxs : f x ∈ Y.basicOpen s
this : x ∈ X.basicOpen ((ConcreteCategory.hom (app f U)) s)
⊢ False
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ Set.range ⇑f ⊆ ↑(ker f).support

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
H : f.ker = ⊤
⊢ IsEmpty ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk (f (closedPoint ↑R)) = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
f₁ f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
h₁ : f₁.fst = f₂.fst
⊢ Inseparable f₁.fst f₂.fst

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
f₁ f₂ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ f₁ = f₂ ↔ ∃ (h₁ : f₁.fst = f₂.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₂.snd

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
U : X.Opens
x : ↥X
hx : x ∈ U
f : ↑Γ(X, U)
⊢ (ConcreteCategory.hom (X.evaluation U x hx)) f ≠ 0 ↔ x ∈ X.basicOpen f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.residue (f x) ≫ Hom.residueFieldMap f x = Hom.stalkMap f x ≫ X.residue x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
R : CommRingCat
inst✝ : IsLocalRing ↑R
xf : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ (fun f ↦ ⟨f (closedPoint ↑R), ⟨Scheme.stalkClosedPointTo f, ⋯⟩⟩)
      ((fun xf ↦ Spec.map ↑xf.snd ≫ X.fromSpecStalk xf.fst) xf) =
    xf

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ residueDegree (𝟙 X) x = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f : X ⟶ Y
x y : ↥X
h : x = y
⊢ X.residueField x = X.residueField y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ residueFieldCongr e ≪≫ residueFieldCongr e' = residueFieldCongr ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y z : ↥X
e : x = y
e' : y = z
⊢ (residueFieldCongr e).hom ≫ (residueFieldCongr e').hom = (residueFieldCongr ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
⊢ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U = f.ker.ideal U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y : ↥X
h : x = y
⊢ X.residue x ≫ (residueFieldCongr h).hom = (X.presheaf.stalkCongr ⋯).hom ≫ X.residue y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f g : X ⟶ Y
e : f = g
x : ↥X
⊢ f x = g x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ ↑U ⊓ ↑V ≤ ↑V ⊓ ↑U

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
⊢ ⨅ i, ker (𝒰.f i ≫ f) = ker f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f g : X ⟶ Y
e : f = g
x : ↥X
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap g x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x₁ x₂ : ↥X
e : x₁ = x₂
⊢ residueFieldMap f x₁ ≫ (residueFieldCongr e).hom = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
x : ↥X
⊢ IsPreimmersion (X.fromSpecResidueField x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x y : ↥X
h : x = y
⊢ Spec.map (residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
h✝ : Nonempty 𝒰.I₀
this : ∀ (U : ↑Y.affineOpens), (⋃ i, ↑(ker (𝒰.f i ≫ f)).support) ∩ ↑↑U = ↑f.ker.support ∩ ↑↑U
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (residueFieldMap f x) ≫ Y.fromSpecResidueField (f x) = X.fromSpecResidueField x ≫ f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
s : ↥(Spec (X.residueField x))
⊢ (X.fromSpecResidueField x) s = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X : Scheme
x : ↥X
⊢ Set.range ⇑(X.fromSpecResidueField x) = {x}

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
X : Scheme
x : ↥X
f : X.presheaf.stalk x ⟶ CommRingCat.of K
inst✝ : IsLocalHom (CommRingCat.Hom.hom f)
⊢ Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝¹ : QuasiCompact f
𝒰 : X.OpenCover
inst✝ : Finite 𝒰.I₀
⊢ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support = ↑f.ker.support

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U : Y.Opens
V : ↑(↑U).affineOpens
⊢ (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨U.ι ''ᵁ ↑V, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (descResidueField (stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f (closedPoint K)) = f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
⊢ I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueDataObjι V =
    pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯) ≫ X.homOfLE ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    (ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ x trivial ≫ (Spec R).residue x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₁ t₂ : Triplet f g
ex : t₁.x = t₂.x
ey : t₁.y = t₂.y
⊢ t₁ = t₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : Triplet f g
e : T₁ = T₂
⊢ T₁.tensor = T₂.tensor

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ Spec.map (residueFieldIso R x).inv ≫ Spec.map (CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField)) =
    (Spec R).fromSpecResidueField x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
this✝¹ : QuasiCompact f'
this✝ : IsOpenImmersion iU
x : ↑Γ(V, ↑W)
this : iU ''ᵁ f' ⁻¹ᵁ ↑W = f ⁻¹ᵁ iV ''ᵁ ↑W
e : Γ(X, f ⁻¹ᵁ iV ''ᵁ ↑W) ≅ Γ(U, f' ⁻¹ᵁ ↑W) := Functor.mapIso X.presheaf (eqToIso this).op ≪≫ Hom.appIso iU (f' ⁻¹ᵁ ↑W)
⊢ (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ tensorCongr e ≪≫ tensorCongr e' = tensorCongr ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x y z : Triplet f g
e : x = y
e' : y = z
⊢ (tensorCongr e).hom ≫ (tensorCongr e').hom = (tensorCongr ⋯).hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: K : Type u_1
inst✝ : Field K
X : Scheme
f₁ f₂ : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ f₁ = f₂ ↔ ∃ (e : f₁.fst = f₂.fst), f₁.snd = (residueFieldCongr e).hom ≫ f₂.snd

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range ⇑(↑U ⊓ ↑V).ι ⊆ ↑↑V

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y U V : Scheme
f : X ⟶ Y
f' : U ⟶ V
iU : U ⟶ X
iV : V ⟶ Y
inst✝¹ : IsOpenImmersion iV
inst✝ : QuasiCompact f
H : IsPullback f' iU iV f
W : ↑V.affineOpens
⊢ (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨iV ''ᵁ ↑W, ⋯⟩)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X✝¹ : Scheme
U : X✝¹.Opens
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
K : Type u
inst✝ : Field K
X : Scheme
f : (x : ↥X) × (X.residueField x ⟶ CommRingCat.of K)
⊢ (fun f ↦ ⟨f (closedPoint ↑(CommRingCat.of K)), descResidueField (stalkClosedPointTo f)⟩)
      ((fun xf ↦ Spec.map xf.snd ≫ X.fromSpecResidueField xf.fst) f) =
    f

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
K : Type u
inst✝ : Field K
g : Spec (CommRingCat.of K) ⟶ X
⊢ descResidueField (stalkClosedPointTo (g ≫ f)) =
    Hom.residueFieldMap f (g (closedPoint K)) ≫ descResidueField (stalkClosedPointTo g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (Spec.map T.tensorInl ≫ X.fromSpecResidueField T.x) ≫ f = (Spec.map T.tensorInr ≫ Y.fromSpecResidueField T.y) ≫ g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : IsAffineHom f
inst✝ : IsAffineHom g
⊢ IsAffineHom (f ≫ g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
⊢ IsAffineHom (X.basicOpen r).ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range ⇑(↑U ⊓ ↑W).ι ⊆ ↑↑U₀

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.fst f g) (T.SpecTensorTo p) = T.x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ Set.range
      ⇑(pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U).ι) ⊆
    Set.range ⇑(↑V ⊓ ↑U₀).ι

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.snd f g) (T.SpecTensorTo p) = T.y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ ofPoint (T.SpecTensorTo p) = T

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x) ≫ Hom.residueFieldMap (pullback.fst f g) t =
    ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫ Hom.residueFieldMap (pullback.snd f g) t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ Spec.map (ofPointTensor t) ≫ (Triplet.ofPoint t).SpecTensorTo = (pullback f g).fromSpecResidueField t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↥(pullback f g)
⊢ (Triplet.ofPoint t).SpecTensorTo (SpecOfPoint t) = t

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T T' : Triplet f g
h : T = T'
⊢ Spec.map (Triplet.tensorCongr h).hom ≫ T.SpecTensorTo = T'.SpecTensorTo

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V W U₀ : ↑X.affineOpens
hU₀ : ↑U ⊓ ↑W ≤ ↑U₀
⊢ (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) ≫
      I.glueDataObjι V =
    IsOpenImmersion.lift (↑V ⊓ ↑U₀).ι
        (pullback.fst (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
          pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯) ≫ I.glueDataObjι U ≫ (↑U).ι)
        ⋯ ≫
      X.homOfLE ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ ↑i ≤ ↑i ⊓ ↑i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑(↑i ⊓ ↑i)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ X.homOfLE ⋯ ≫ X.homOfLE ⋯ = 𝟙 ↑↑i

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case h₀
X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ (I.glueDataT i i ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i =
    (𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2) ≫ pullback.fst (I.glueDataObjι i) (X.homOfLE ⋯)) ≫ I.glueDataObjι i

Tactic:
simp [pullback.condition]

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i : ↑X.affineOpens
⊢ I.glueDataT i i = 𝟙 (I.glueDataObjPullback (i, i).1 (i, i).2)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯) =
    I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯ ≫ pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ Spec.map (Hom.residueFieldMap T.SpecTensorTo p) ≫
      Spec.map (ofPointTensor (T.SpecTensorTo p)) ≫ Spec.map (tensorCongr ⋯).hom =
    (Spec T.tensor).fromSpecResidueField p

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
⊢ QuasiSeparatedSpace ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
i j k : ↑X.affineOpens
⊢ pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯)
        (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯ ≫
      pullback.snd (pullback.fst (I.glueDataObjι (j, k).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (j, i).1) (X.homOfLE ⋯)) =
    pullback.fst (pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯))
        (pullback.fst (I.glueDataObjι (i, k).1) (X.homOfLE ⋯)) ≫
      I.glueDataT i j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : QuasiCompact f
this : ∀ {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f], (∃ S, Y = Spec S) → ↑(ker f).support ⊆ closure (Set.range ⇑f)
hY : ¬∃ S, Y = Spec S
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
x : ↥(𝒰.X i)
hx : (𝒰.f i) x ∈ ↑(ker f).support
inst : QuasiCompact (Cover.pullbackHom 𝒰 f i)
⊢ (𝒰.f i) x ∈ ↑↑⟨𝒰.f i ''ᵁ ↑⟨⊤, ⋯⟩, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T₁ T₂ : (T : Triplet f g) × ↥(Spec T.tensor)
⊢ T₁ = T₂ ↔ ∃ (e : T₁.fst = T₂.fst), (Spec.map (Triplet.tensorCongr e).inv) T₁.snd = T₂.snd

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ Function.RightInverse (fun T ↦ T.fst.SpecTensorTo T.snd) fun t ↦ ⟨Triplet.ofPoint t, SpecOfPoint t⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.fst f g) (carrierEquiv.symm ⟨T, p⟩) = T.x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
p : ↥(Spec T.tensor)
⊢ (pullback.snd f g) (carrierEquiv.symm ⟨T, p⟩) = T.y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
⊢ CompactSpace ↥X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (pullback.fst f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.x ∧ (pullback.snd f g) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
⊢ IsEmpty ↥(pullback f g) ↔ Disjoint (Set.range ⇑f) (Set.range ⇑g)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝² : Nonempty ↥X
inst✝¹ : Nonempty ↥Y
inst✝ : Subsingleton ↥S
⊢ Nonempty ↥(pullback f g)

Tactic:
by

Goal state after: