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

Goal state before:
pp: case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U

Tactic:
;

Goal state after:
case refine_2
X : Scheme
I J : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
this : CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op) = algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
x : ↑Γ(X, ↑U)
s : ↥(Submonoid.powers f)
n₁ : ℕ
h₁ : f ^ n₁ * x ∈ I.ideal U
n₂ : ℕ
h₂ : f ^ n₂ * x ∈ J.ideal U
⊢ f ^ n₁ * (f ^ n₂ * x) ∈ J.ideal U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ (Submonoid.powers f).IsLocalizationMap ⇑(algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f))

Tactic:
;

Goal state after:
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ (Submonoid.powers f).IsLocalizationMap ⇑(algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) = I.ideal (X.affineBasicOpen f)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case nonempty
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

pp: case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam

Tactic:
;

Goal state after:
case nonempty
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
⊢ IsDomain ↑Γ(X, U)

Tactic:
have : NoZeroDivisors
      (X.toLocallyRingedSpace.toSheafedSpace.toPresheafedSpace.presheaf.obj (op U)) := by
    refine ⟨fun {a b} e => ?_⟩
    simp_rw [← basicOpen_eq_bot_iff, ← Opens.not_nonempty_iff_eq_bot]
    by_contra! h
    obtain ⟨x, ⟨hxU, hx₁⟩, _, hx₂⟩ :=
      nonempty_preirreducible_inter (X.basicOpen a).2 (X.basicOpen b).2 h.1 h.2
    replace e := congr_arg (X.presheaf.germ U x hxU) e
    rw [map_mul, map_zero] at e
    refine zero_ne_one' (X.presheaf.stalk x) (isUnit_zero_iff.1 ?_)
    convert! hx₁.mul hx₂
    exact e.symm

Goal state after:
case component_integral
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this✝ : ∃ x y, x ≠ y
this : NoZeroDivisors ↑(X.presheaf.obj (op U))
⊢ IsDomain ↑Γ(X, U)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case nonempty
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

pp: case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam

Tactic:
;

Goal state after:
case nonempty
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (Nonempty ↥X) IsIntegral.nonempty._autoParam

case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ autoParam (∀ (U : X.Opens) [Nonempty ↥↑U], IsDomain ↑Γ(X, U)) IsIntegral.component_integral._autoParam
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ Spec.map f = Spec.map (φ ≫ i.inv)

Tactic:
;

Goal state after:
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
H✝ : IsOpenImmersion (Spec.map f)
e : ↑R
he : IsIdempotentElem e
he' : Set.range (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) = PrimeSpectrum.zeroLocus {e}
φ : R ⟶ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
this : IsOpenImmersion (Spec.map φ)
H : Set.range ⇑(Spec.map φ) = Set.range ⇑(Spec.map f)
i : S ≅ CommRingCat.of (↑R ⧸ Ideal.span {e}) := ⋯
hi : Function.Injective ⇑(CommRingCat.Hom.hom i.inv)
⊢ Spec.map f = Spec.map (φ ≫ i.inv)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

Tactic:
;

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ x✝¹ ∈ (⨆ i, (𝒰.f i ≫ f) ''ᵁ 𝒰.f i ⁻¹ᵁ { carrier := U, is_open' := hU }).carrier
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ ∃ i x, (𝒰.f i) x ∈ U ∧ (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f i).base) x) = x✝¹

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x✝¹ : ↥Y
x✝ : x✝¹ ∈ ⇑f '' U
x : ↥X
left✝ : x ∈ U
right✝ : f x = x✝¹
this : ∃ i y, (𝒰.f i) y = x
⊢ ∃ i x, (𝒰.f i) x ∈ U ∧ (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f i).base) x) = x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊤ * I).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊤ * I).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊤).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊤).ideal x✝¹ ↔ x✝ ∈ I.ideal x✝¹
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ ∀ (x_1 : 𝒰.I₀) (x_2 : ↥(𝒰.X x_1)),
    (𝒰.f x_1) x_2 ∈ U → (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f x_1).base) x_2) = x → ∃ x_3 ∈ U, f x_3 = x

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
𝒰 : X.OpenCover
hf : Function.Injective ⇑f
h𝒰 : ∀ (i : 𝒰.I₀), IsOpenImmersion (𝒰.f i ≫ f)
U : Set ↥X
hU : IsOpen U
x : ↥Y
⊢ ∀ (x_1 : 𝒰.I₀) (x_2 : ↥(𝒰.X x_1)),
    (𝒰.f x_1) x_2 ∈ U → (TopCat.Hom.hom f.base) ((TopCat.Hom.hom (𝒰.f x_1).base) x_2) = x → ∃ x_3 ∈ U, f x_3 = x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊥ * I).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (⊥ * I).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊥).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (I * ⊥).ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U

Tactic:
;

Goal state after:
X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ (I * (J ⊔ K)).ideal U = (I * J ⊔ I * K).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U

Tactic:
;

Goal state after:
X : Scheme
I J K : X.IdealSheafData
U : ↑X.affineOpens
⊢ ((I ⊔ J) * K).ideal U = (I * K ⊔ J * K).ideal U
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ I J K x✝² : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (x✝² ^ 0).ideal x✝¹ ↔ x✝ ∈ ideal 1 x✝¹

Tactic:
;

Goal state after:
X : Scheme
I✝ I J K x✝² : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (x✝² ^ 0).ideal x✝¹ ↔ x✝ ∈ ideal 1 x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ I J K : X.IdealSheafData
x✝³ : ℕ
x✝² : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (x✝² ^ (x✝³ + 1)).ideal x✝¹ ↔ x✝ ∈ (x✝² ^ x✝³ * x✝²).ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
I✝ I J K : X.IdealSheafData
x✝³ : ℕ
x✝² : X.IdealSheafData
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ (x✝² ^ (x✝³ + 1)).ideal x✝¹ ↔ x✝ ∈ (x✝² ^ x✝³ * x✝²).ideal x✝¹
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) I =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I

Tactic:
;

Goal state after:
X : Scheme
I✝ : X.IdealSheafData
I : Ideal ↑Γ(X, ⊤)
U : ↑X.affineOpens
f : ↑Γ(X, ↑U)
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) I =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) I
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))))

pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
;

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

X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv ''
      PrimeSpectrum.zeroLocus ↑(RingHom.ker (CommRingCat.Hom.hom (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))))) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
h : X.affineBasicOpen f ≤ V
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑(X.affineBasicOpen f)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f ↑Γ(X, ↑(X.affineBasicOpen f))

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
h : X.affineBasicOpen f ≤ V
this✝ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f)) :=
  (Ideal.quotientMap (I.ideal (X.affineBasicOpen f)) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑(X.affineBasicOpen f)) :=
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
⊢ IsLocalization.Away f ↑Γ(X, ↑(X.affineBasicOpen f))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ (Ideal.Quotient.mk (I.ideal U)).comp (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) =
    (Ideal.Quotient.mk (I.ideal U)).comp (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))

Tactic:
;

Goal state after:
case refine_1
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
f : ↑Γ(X, ↑V)
hU : U = X.affineBasicOpen f
this✝¹ : Algebra (↑Γ(X, ↑V) ⧸ I.ideal V) (↑Γ(X, ↑U) ⧸ I.ideal U) :=
  (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) ⋯).toAlgebra
this✝ : Algebra ↑Γ(X, ↑V) ↑Γ(X, ↑U) := (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)).toAlgebra
this : IsLocalization.Away f ↑Γ(X, ↑U)
⊢ (Ideal.Quotient.mk (I.ideal U)).comp (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) =
    (Ideal.Quotient.mk (I.ideal U)).comp (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑V)
⊢ Hom.opensRange (I.glueDataObjMap ⋯) = I.glueDataObjι V ⁻¹ᵁ (↑V).ι ⁻¹ᵁ X.basicOpen f

Tactic:
by
  let := (Ideal.quotientMap _ _ (I.ideal_le_comap_ideal (X.affineBasicOpen_le f))).toAlgebra
  let f' : Γ(X, V) ⧸ I.ideal V := Ideal.Quotient.mk _ f
  have := I.isLocalization_away (X.affineBasicOpen_le f) f rfl
  ext1
  refine (localization_away_comap_range _ f').trans ?_
  rw [← comap_basicOpen, ← V.2.fromSpec_preimage_basicOpen,
    ← Scheme.Hom.comp_preimage, glueDataObjι_ι]
  rfl

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

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ X.nilradical.ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹

Tactic:
;

Goal state after:
X : Scheme
inst✝ : IsReduced X
x✝¹ : ↑X.affineOpens
x✝ : ↑Γ(X, ↑x✝¹)
⊢ x✝ ∈ X.nilradical.ideal x✝¹ ↔ x✝ ∈ ⊥.ideal x✝¹
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ ⊤

Tactic:
;

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ x ∈ ⊤
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ ⊤

Tactic:
;

Goal state after:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
a : ↑(Y.presheaf.obj (op ⊤))
⊢ x ∈ ⊤
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: 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
⊢ ⊤ ≤ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V

Tactic:
;

Goal state after:
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
⊢ ⊤ ≤ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: 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 ⋯)
| I.glueDataObjι V

Tactic:
;

Goal state after:
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 ⋯)
| I.glueDataObjι V
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 x

Tactic:
;

Goal state after:
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 x
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:
;

Goal state after:
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
Module: Mathlib.AlgebraicGeometry.Stalk

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

Tactic:
;

Goal state after:
case mp
X : Scheme
R : CommRingCat
f₁ : (x : ↥X) × { f // IsLocalHom (CommRingCat.Hom.hom f) }
⊢ ∃ (h₁ : f₁.fst = f₁.fst), ↑f₁.snd = (X.presheaf.stalkCongr ⋯).hom ≫ ↑f₁.snd
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
;

Goal state after:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ X.residueField x = X.residueField x
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
;

Goal state after:
X✝ : Scheme
U : X✝.Opens
X Y : Scheme
f✝ f : X ⟶ Y
x : ↥X
⊢ f x = f x
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
;

Goal state after:
X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ residueFieldMap f x = (residueFieldCongr ⋯).hom ≫ residueFieldMap f x
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| I.glueDataObjι V

Tactic:
;

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
| I.glueDataObjι V
Module: Mathlib.AlgebraicGeometry.ResidueField

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

Tactic:
;

Goal state after:
X : Scheme
x : ↥X
⊢ Spec.map (residueFieldCongr ⋯).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField x
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
  simp [fromSpecResidueField, ← Spec.map_comp_assoc]

Goal state after:
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂

Tactic:
;

Goal state after:
case mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t₂ : Triplet f g
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x = t₂.x
ey : { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y = t₂.y
⊢ { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ } = t₂
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (Spec.stalkIso R x).inv ≫ (Spec R).residue x

Tactic:
;

Goal state after:
R : CommRingCat
x : ↥(Spec R)
⊢ CommRingCat.ofHom (algebraMap (↑R) x.asIdeal.ResidueField) ≫ (residueFieldIso R x).inv =
    CommRingCat.ofHom (algebraMap (↑R) (Localization.AtPrime x.asIdeal)) ≫ (Spec.stalkIso R x).inv ≫ (Spec R).residue x
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }

Tactic:
;

Goal state after:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ } = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }
Module: Mathlib.AlgebraicGeometry.PullbackCarrier

Goal state before:
pp: case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ x✝¹ = x✝ ∧ y✝¹ = y✝ ∧ s✝¹ = s✝

Tactic:
;

Goal state after:
case mk.mk
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
x✝¹ : ↥X
y✝¹ : ↥Y
s✝¹ : ↥S
hx✝¹ : f x✝¹ = s✝¹
hy✝¹ : g y✝¹ = s✝¹
x✝ : ↥X
y✝ : ↥Y
s✝ : ↥S
hx✝ : f x✝ = s✝
hy✝ : g y✝ = s✝
ex : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.x = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.x
ey : { x := x✝¹, y := y✝¹, s := s✝¹, hx := hx✝¹, hy := hy✝¹ }.y = { x := x✝, y := y✝, s := s✝, hx := hx✝, hy := hy✝ }.y
⊢ x✝¹ = x✝ ∧ y✝¹ = y✝ ∧ s✝¹ = s✝