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

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥

Tactic:
[

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ X.basicOpen x ≠ ⊥ → U ⊓ X.basicOpen x ≠ ⊥
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
x : ↥X
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

Tactic:
wlog h : ∃ R, X = Spec R

Goal state after:
case inr
X : Scheme
x : ↥X
this : ∀ {X : Scheme} (x : ↥X), (∃ R, X = Spec R) → ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
h : ¬∃ R, X = Spec R
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)

X : Scheme
x : ↥X
h : ∃ R, X = Spec R
⊢ ringKrullDim ↑(X.presheaf.stalk x) = ↑(coheight x)
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ IsOpenImmersion (Spec.map f) ↔ ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
constructor
  · intro H
    obtain ⟨e, he, he'⟩ := PrimeSpectrum.isClopen_iff_zeroLocus.mp
      ⟨PrimeSpectrum.isClosed_range_comap_of_surjective _ _ hf,
        (Spec.map f).isOpenEmbedding.isOpen_range⟩
    refine ⟨e, he, ?_⟩
    let φ : R ⟶ _ := (CommRingCat.ofHom (Ideal.Quotient.mk (.span {e})))
    have : IsOpenImmersion (Spec.map φ) :=
      have : IsLocalization.Away (1 - e) (↑R ⧸ Ideal.span {e}) :=
        IsLocalization.away_of_isIdempotentElem he.one_sub (by simp) Ideal.Quotient.mk_surjective
      IsOpenImmersion.of_isLocalization (1 - e)
    have H : Set.range (Spec.map φ) = Set.range (Spec.map f) :=
      ((range_comap_of_surjective _ _
        Ideal.Quotient.mk_surjective).trans (by simp)).trans he'.symm
    let i : S ≅ .of _ := (Scheme.Spec.preimageIso
      (IsOpenImmersion.isoOfRangeEq (Spec.map φ) (Spec.map f) H)).unop
    have hi : Function.Injective i.inv.hom := (ConcreteCategory.bijective_of_isIso i.inv).1
    have : f = φ ≫ i.inv := by apply Spec.map_injective; simp [i, ← Scheme.Spec_map]
    rw [this, CommRingCat.hom_comp, RingHom.ker_eq_comap_bot, ← Ideal.comap_comap,
      ← RingHom.ker_eq_comap_bot, (RingHom.injective_iff_ker_eq_bot i.inv.hom).mp hi,
      ← RingHom.ker_eq_comap_bot]
    simp [φ]
  · rintro ⟨e, he, he'⟩
    let := f.hom.toAlgebra
    have : IsLocalization.Away (1 - e) S :=
      IsLocalization.away_of_isIdempotentElem he.one_sub (by simpa using! he') hf
    exact IsOpenImmersion.of_isLocalization (1 - e)

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

Goal state before:
pp: case hf
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Function.Surjective ⇑(CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))

Tactic:
exact Ideal.Quotient.mk_surjective

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hU.fromSpec

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U x hxU) ≫ hU.fromSpec =
    Spec.map (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.germ U' x h₂) ≫ hU.fromSpec
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.germ U' x h₂) ≫ Spec.map (X.presheaf.map (homOfLE ⋯).op) ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X : Scheme
U V : X.Opens
hU : IsAffineOpen U
hV : IsAffineOpen V
x : ↥X
hxU : x ∈ U
hxV : x ∈ V
U' : Opens ↥X
h₁ : U' ∈ X.affineOpens
h₂ : x ∈ U'
h₃ : U' ≤ U ⊓ V
⊢ Spec.map (X.presheaf.map (homOfLE ⋯).op ≫ X.presheaf.germ U' x h₂) ≫ hV.fromSpec =
    Spec.map (X.presheaf.germ V x hxV) ≫ hV.fromSpec
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map (CommRingCat.ofHom (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    I.glueDataObjι U ≫ X.homOfLE h

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Spec.map
        (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V)) ≫
          CommRingCat.ofHom (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯)) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    I.glueDataObjι U ≫ X.homOfLE h
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (Hom.stalkMap f x) ≫ Spec.map (Y.presheaf.germ U (f x) hxU) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : f x ∈ ↑U
V : TopologicalSpace.Opens ↥X
hV : V ∈ X.affineOpens
hxV : x ∈ ↑V
hVU : ↑V ⊆ (f ⁻¹ᵁ U).carrier
⊢ Spec.map (Y.presheaf.germ U (f x) hxU ≫ Hom.stalkMap f x) ≫ IsAffineOpen.fromSpec hU =
    IsAffineOpen.fromSpecStalk hV hxV ≫ f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      (RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s))))

Tactic:
[

Goal state after:
case refine_1.a
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s x : ↑Γ(Y, ↑U)
hx : x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))
⊢ x ∈
    Ideal.comap (CommRingCat.Hom.hom (Y.presheaf.map (homOfLE ⋯).op))
      (RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s))))
Module: Mathlib.AlgebraicGeometry.Stalk

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

Tactic:
[

Goal state after:
R S : CommRingCat
inst✝ : IsLocalRing ↑S
φ : R ⟶ S
⊢ φ ≫
      (ΓSpecIso S).inv ≫
        (Spec S).presheaf.germ (Spec.map φ ⁻¹ᵁ ⊤) (closedPoint ↑S) trivial ≫ (stalkClosedPointIso S).hom =
    φ
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
this : (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x = 0
⊢ (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯)) x = 0

Tactic:
[

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
F : pullback (I.glueDataObjι U) (X.homOfLE ⋯) ⟶ ↑(↑U ⊓ ↑V) := pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)
x : ↑Γ(X, ↑V)
hx : x ∈ I.ideal V
this : (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.app (I.glueDataObjι U) ((↑U).ι ⁻¹ᵁ ↑V))) x = 0
⊢ (CommRingCat.Hom.hom (Hom.app (↑U).ι ↑V ≫ Hom.appLE (F ≫ X.homOfLE ⋯) ((↑U).ι ⁻¹ᵁ ↑V) ⊤ ⋯)) x = 0
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
  refine ofIdeals_mono fun U ↦ ?_
  rw [Scheme.Hom.comp_app f g U, CommRingCat.hom_comp, ← RingHom.comap_ker]
  exact Ideal.ker_le_comap _

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
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f

Tactic:
[

Goal state after:
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
this✝ : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint ↑R) = x
this : x ∈ U
⊢ X.presheaf.germ U x this ≫ (ΓSpecIso (X.presheaf.stalk x)).inv ≫ Hom.appLE (Spec.map f) ⊤ ⊤ ⋯ ≫ (ΓSpecIso R).hom =
    X.presheaf.germ U x ⋯ ≫ f
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:
have : (Spec.map f ≫ X.fromSpecStalk x) (closedPoint R) = x := by
    rw [Hom.comp_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
  have : x ∈ U := this ▸ hU
  simp only [germ_stalkClosedPointTo, Hom.comp_app,
    fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom, Functor.mapIso_hom,
      (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]
  simp_rw [← Opens.map_top (Spec.map f).base]
  rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (stalkClosedPointTo f) ≫ Spec.map (X.presheaf.germ U (f (closedPoint ↑R)) hxU) ≫ IsAffineOpen.fromSpec hU = f

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X : Scheme
R : CommRingCat
inst✝ : IsLocalRing ↑R
f : Spec R ⟶ X
U : TopologicalSpace.Opens ↥X
hU : U ∈ X.affineOpens
hxU : f (closedPoint ↑R) ∈ ↑U
this : Spec.map (ΓSpecIso R).hom ≫ Spec.map (Hom.appLE f U ⊤ ⋯) ≫ IsAffineOpen.fromSpec hU = f
⊢ Spec.map (X.presheaf.germ U (f (closedPoint ↑R)) hxU ≫ stalkClosedPointTo f) ≫ IsAffineOpen.fromSpec hU = f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
𝒰 : X.OpenCover
U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
hs : s ∈ ⨅ i, (ker (𝒰.f i ≫ f)).ideal U
i : 𝒰.I₀
x : ↥(𝒰.X i)
hxU : (𝒰.f i) x ∈ Opposite.unop (Opposite.op (f ⁻¹ᵁ ↑U))
⊢ (CommRingCat.Hom.hom (appLE (𝒰.f i ≫ f) (↑U) (𝒰.f i ⁻¹ᵁ f ⁻¹ᵁ ↑U) ⋯)) s = 0

Tactic:
simpa [Scheme.Hom.appLE] using! ideal_ker_le _ _ (Ideal.mem_iInf.mp hs i)

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Spec.map (Y.residue (f x) ≫ residueFieldMap f x) ≫ Y.fromSpecStalk (f x) =
    Spec.map (X.residue x) ≫ Spec.map (stalkMap f x) ≫ Y.fromSpecStalk (f x)
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.app f (iV ''ᵁ ↑W) = ((Hom.appIso iV ↑W).hom ≫ Hom.app f' ↑W) ≫ e.inv

Tactic:
Iso.eq_comp_inv

Goal state after:
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.app f (iV ''ᵁ ↑W) ≫ e.hom = (Hom.appIso iV ↑W).hom ≫ Hom.app f' ↑W
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₀
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.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x

Tactic:
[

Goal state after:
case h₀
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.map T.tensorInl) ≫
      X.fromSpecResidueField T.x =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInl) ≫ X.fromSpecResidueField T.x
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case h₁
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.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y

Tactic:
[

Goal state after:
case h₁
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.map T.tensorInr) ≫
      Y.fromSpecResidueField T.y =
    ((Spec T.tensor).fromSpecResidueField p ≫ Spec.map T.tensorInr) ≫ Y.fromSpecResidueField T.y
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)
⊢ IsAffine X

Tactic:
have : QuasiSeparatedSpace X := isAffine_of_isAffineOpen_basicOpen_aux s hs hs₂

Goal state after:
X : Scheme
s : Set ↑Γ(X, ⊤)
hs : Ideal.span s = ⊤
hs₂ : ∀ i ∈ s, IsAffineOpen (X.basicOpen i)
this : QuasiSeparatedSpace ↥X
⊢ IsAffine X
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V =
    𝟙 (I.glueData.U U) ≫
      inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V

Tactic:
[

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
this✝ : IsIso (X.homOfLE ⋯)
H : inv (X.homOfLE ⋯) = X.homOfLE ⋯
this :
  inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
      I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V =
    I.glueData.ι U
⊢ I.glueDataObjMap h ≫ I.glueData.ι V =
    𝟙 (I.glueData.U U) ≫
      inv (pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ≫
        I.glueDataT U V ≫ pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯) ≫ I.glueData.ι V
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))

Tactic:
[

Goal state after:
case hs₂
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
x✝ : IsAffine Y
f : X ⟶ Y
s : Finset ↑Γ(Y, ⊤)
hs : Ideal.span ↑s = ⊤
hf : ∀ (r : ↥s), IsAffine ↑(f ⁻¹ᵁ Y.basicOpen ↑r) ∧ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ∣_ Y.basicOpen ↑r)))
r : ↑Γ(Y, ⊤)
hr : r ∈ ↑s
⊢ IsAffineOpen (X.basicOpen ((ConcreteCategory.hom (Scheme.Hom.appTop f)) r))
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
X' Y' S' : Scheme
f' : X' ⟶ S'
g' : Y' ⟶ S'
i₁ : X ⟶ X'
i₂ : Y ⟶ Y'
i₃ : S ⟶ S'
e₁ : f ≫ i₃ = i₁ ≫ f'
e₂ : g ≫ i₃ = i₂ ≫ g'
inst✝ : Mono i₃
⊢ Set.range ⇑(pullback.map f g f' g' i₁ i₂ i₃ e₁ e₂) =
    ⇑(pullback.fst f' g') ⁻¹' Set.range ⇑i₁ ∩ ⇑(pullback.snd f' g') ⁻¹' Set.range ⇑i₂

Tactic:
by
  ext z
  constructor
  · rintro ⟨t, rfl⟩
    constructor
    · use pullback.fst f g t
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
      simp
    · use pullback.snd f g t
      rw [← Scheme.Hom.comp_apply, ← Scheme.Hom.comp_apply]
      simp
  · intro ⟨⟨x, hx⟩, ⟨y, hy⟩⟩
    let T₁ : Triplet (pullback.fst f' g') i₁ := Triplet.mk' z x hx.symm
    obtain ⟨w₁, hw₁⟩ := T₁.exists_preimage
    let T₂ : Triplet (pullback.snd f' g') i₂ := Triplet.mk' z y hy.symm
    obtain ⟨w₂, hw₂⟩ := T₂.exists_preimage
    let T : Triplet (pullback.fst (pullback.fst f' g') i₁) (pullback.fst (pullback.snd f' g') i₂) :=
      Triplet.mk' w₁ w₂ <| by simp [hw₁.left, hw₂.left, T₁, T₂]
    obtain ⟨t, _, ht₂⟩ := T.exists_preimage
    use (pullbackFstFstIso f g f' g' i₁ i₂ i₃ e₁ e₂).hom t
    rw [pullback_map_eq_pullbackFstFstIso_inv, ← Scheme.Hom.comp_apply, Iso.hom_inv_id_assoc]
    simp [ht₂, T, hw₂.left, T₂]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
      (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv ≫
        (Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯).unop).op ≫
          (Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯)
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv

Tactic:
[

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
this✝ :
  I.subschemeCover.f U ≫ I.subschemeι =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ IsAffineOpen.fromSpec ⋯
this :
  Hom.app I.subschemeι ↑U ≫ Hom.app (I.subschemeCover.f U) (I.subschemeι ⁻¹ᵁ ↑U) =
    CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫
      (ΓSpecIso (CommRingCat.of (↑Γ(X, ↑U) ⧸ I.ideal U))).inv ≫
        (Spec (I.subschemeCover.X U)).presheaf.map
            ((Opens.map (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))).base).map (eqToHom ⋯).unop).op ≫
          (Spec (I.subschemeCover.X U)).presheaf.map (eqToHom ⋯)
⊢ Hom.app I.subschemeι ↑U = CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ (I.subschemeObjIso U).inv
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ IsEmpty ↥⊤.subscheme

Tactic:
← (subschemeι _).ker_eq_top_iff_isEmpty,

Goal state after:
X : Scheme
I : X.IdealSheafData
⊢ Hom.ker ⊤.subschemeι = ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv

Tactic:
← Spec.map_comp_assoc,

Goal state after:
X : Scheme
I J : X.IdealSheafData
h : I ≤ J
U : ↑X.affineOpens
⊢ Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)) ≫ CommRingCat.ofHom (Ideal.Quotient.factor ⋯)) ≫
      (IsAffineOpen.isoSpec ⋯).inv =
    Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (J.ideal U))) ≫ (IsAffineOpen.isoSpec ⋯).inv
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: case pos
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
y : ↥Y
hy : y ∈ Set.range ⇑f
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

pp: case neg
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
y : ↥Y
hy : y ∉ Set.range ⇑f
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)

Tactic:
· obtain ⟨x, rfl⟩ := hy
    obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
      Y.isBasis_affineOpens.exists_subset_of_mem_open (Set.mem_univ (f x)) isOpen_univ
    obtain ⟨_, ⟨V, hV, rfl⟩, hxV, hVU⟩ :=
      X.isBasis_affineOpens.exists_subset_of_mem_open hxU (f ⁻¹ᵁ U).isOpen
    obtain ⟨U', hU'U, rfl⟩ : ∃ U' : Y.Opens, U' ≤ U ∧ f ⁻¹ᵁ U' = V := by
      obtain ⟨U', hU', e⟩ := hf₁.isOpen_iff.mp V.2
      exact ⟨⟨U', hU'⟩ ⊓ U, inf_le_right, Opens.ext (by simpa [e] using hVU)⟩
    obtain ⟨r, hrU', hxr⟩ := hU.exists_basicOpen_le ⟨f x, hxV⟩ hxU
    refine ⟨_, hxr, hU.basicOpen r, ?_⟩
    convert hV.basicOpen (f.app _ (Y.presheaf.map (homOfLE hU'U).op r))
    simp only [Scheme.preimage_basicOpen, ← CommRingCat.comp_apply, f.naturality]
    simpa using ((Opens.map f.base).map (homOfLE hrU')).le

Goal state after:
case neg
X Y : Scheme
f : X ⟶ Y
hf₁ : Topology.IsInducing ⇑f
hf₂ : IsClosed (Set.range ⇑f)
y : ↥Y
hy : y ∉ Set.range ⇑f
⊢ ∃ U, y ∈ U ∧ IsAffineOpen U ∧ IsAffineOpen (f ⁻¹ᵁ U)
Module: Mathlib.AlgebraicGeometry.Morphisms.AffineAnd

Goal state before:
pp: Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))

Tactic:
[

Goal state after:
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
P : MorphismProperty Scheme
hQi : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
hQl : RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] ↦ Q
hQs : RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ HasAffineProperty P (affineAnd fun {R S} [CommRing R] [CommRing S] ↦ Q) ↔
    ∀ {X Y : Scheme} (f : X ⟶ Y),
      P f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → Q (CommRingCat.Hom.hom (Scheme.Hom.app f U))