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

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).f i ≫ f)))

Tactic:
simpa using

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ↑(U i) ⋯))
this :
  ∀ (i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀),
    IsAffine ((X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).X i)
i : (X.openCoverOfIsOpenCover (fun i ↦ ↑(U i)) hU).I₀
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f ⊤ ((↑(U i)).ι ''ᵁ ⊤) ⋯))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : J.FiniteHeight
⊢ I.primeHeight < J.primeHeight

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝³ : CommRing R
I J : Ideal R
inst✝² : I.IsPrime
inst✝¹ : J.IsPrime
h : I < J
inst✝ : J.FiniteHeight
⊢ I.height < J.height
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [inst : IsAffine Y] (𝒰 : X.OpenCover),
    sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
      ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)

Tactic:
intro X Y f _ 𝒰

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Y✝
g : Y✝ ⟶ Z
X Y : Scheme
f : X ⟶ Y
inst✝ : IsAffine Y
𝒰 : X.OpenCover
⊢ sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) f ↔
    ∀ (i : 𝒰.I₀), sourceAffineLocally (fun {R S} [CommRing R] [CommRing S] ↦ Q) (𝒰.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ↑(S ⊓ ↑U) = ↑(⨆ i, ↑↑i)

Tactic:
simpa using

Goal state after:
X : Scheme
U✝ : X.Opens
hU✝ : IsCompact U✝.carrier
S : X.Opens
hS : IsCompact S.carrier
U : ↑X.affineOpens
hU :
  IsQuasiSeparated S.carrier →
    ∀ (f : ↑Γ(X, S)) (x : ↑Γ(X, X.basicOpen f)),
      ∃ n y,
        (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y =
          (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f ^ n * x
hSU : IsQuasiSeparated (S ⊔ ↑U).carrier
f : ↑Γ(X, S ⊔ ↑U)
x : ↑Γ(X, X.basicOpen f)
n₁ : ℕ
y₁ : ↑Γ(X, S)
hy₁ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₁ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₁ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.181).op)) x
n₂ : ℕ
y₂ : ↑Γ(X, ↑U)
hy₂ :
  (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) y₂ =
    (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) ((ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) f) ^
        n₂ *
      (ConcreteCategory.hom (X.presheaf.map (homOfLE ?m.240).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
hs : ↑S ∩ ↑↑U = ⋃ i ∈ s, ↑↑i
this : Finite ↑s
val✝ : Fintype ↑s
⊢ ↑S ∩ ↑↑U = ⋃ i, ⋃ (x : i ∈ X.affineOpens), ⋃ (_ : ⟨i, ⋯⟩ ∈ s), ↑i
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ Order.krullDim ↑(Set.Iic { asIdeal := J, isPrime := inst✝ }) =
    ↑(Order.height { asIdeal := comap (algebraMap R A) J, isPrime := ⋯ })

Tactic:
Order.height_eq_krullDim_Iic

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ Order.krullDim ↑(Set.Iic { asIdeal := J, isPrime := inst✝ }) =
    Order.krullDim ↑(Set.Iic { asIdeal := comap (algebraMap R A) J, isPrime := ⋯ })
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ (comap (algebraMap R A) J).primeHeight = J.primeHeight

Tactic:
simpa using

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
S : Submonoid R
A : Type u_2
inst✝³ : CommRing A
inst✝² : Algebra R A
inst✝¹ : IsLocalization S A
J : Ideal A
inst✝ : J.IsPrime
⊢ (comap (algebraMap R A) J).primeHeight = J.primeHeight
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.refine_2
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
p : LTSeries (PrimeSpectrum R)
⊢ (RelSeries.last p).asIdeal.height ≤ ⨆ I, ⨆ (_ : I ≠ ⊤), I.height

Tactic:
· apply le_trans (b := ⨆ (_ : (p.last).asIdeal ≠ ⊤), p.last.asIdeal.height)
      · exact le_iSup_of_le p.last.isPrime.ne_top' le_rfl
      · exact le_iSup (fun I => ⨆ _, I.height) p.last.asIdeal

Goal state after:
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: case a.inr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Nontrivial R
I : Ideal R
I_top : I ≠ ⊤
⊢ ∃ i', ⨆ (_ : I ≠ ⊤), I.height ≤ ⨆ (_ : i'.IsMaximal), i'.height

Tactic:
· obtain ⟨M, hM, hIM⟩ := exists_le_maximal I I_top
      exact ⟨M, iSup_mono' (fun hI ↦ ⟨hM, height_mono hIM⟩)⟩

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

Goal state before:
pp: X : Scheme
x : ↥X
⊢ x ∈ ⊥ ↔ x ∈ ⋂ U, X.zeroLocus ↑(⊤ U)

Tactic:
simpa using

Goal state after:
X : Scheme
x : ↥X
⊢ ∃ x_1 ∈ X.affineOpens, x ∈ x_1
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst✝ : Finite ι
⊢ (⨅ i, I i).ideal = ⨅ i, (I i).ideal

Tactic:
simpa using

Goal state after:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
inst✝ : Finite ι
⊢ (⨅ i, I i).ideal = ⨅ i, (I i).ideal
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this : x ∈ ⨆ i ∈ s, X.basicOpen i
⊢ ∃ r ∈ s, x ∈ X.basicOpen r

Tactic:
simpa using

Goal state after:
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
X Y : Scheme
f : X ⟶ Y
hQ : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Locally fun {R S} [CommRing R] [CommRing S] ↦ Q
this✝ : P.Respects IsOpenImmersion
x : ↥X
U : Opens ↥Y
hU : U ∈ Y.affineOpens
hfx : f x ∈ U
right✝ : U ≤ ⊤
V : Opens ↥X
hV : V ∈ X.affineOpens
hx : x ∈ V
e : V ≤ f ⁻¹ᵁ U
hf :
  ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    ∃ s,
      ∃ (_ : Ideal.span ↑s = ⊤),
        ∀ t ∈ s,
          ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑V)) Sₜ] [IsLocalization.Away t Sₜ],
            Q ((algebraMap (↑Γ(X, ↑V)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)))
s : Finset ↑Γ(X, ↑⟨V, hV⟩)
hfs :
  ∀ t ∈ s,
    ∀ (Sₜ : Type u) [inst : CommRing Sₜ] [inst_1 : Algebra (↑Γ(X, ↑⟨V, hV⟩)) Sₜ] [IsLocalization.Away t Sₜ],
      Q ((algebraMap (↑Γ(X, ↑⟨V, hV⟩)) Sₜ).comp (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑⟨U, hU⟩) (↑⟨V, hV⟩) e)))
hs : ⨆ i ∈ ↑s, X.basicOpen i = ↑⟨V, hV⟩
this : x ∈ ⨆ i ∈ s, X.basicOpen i
⊢ ∃ r ∈ s, x ∈ X.basicOpen r
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
h : ∃ n, s ^ n * f = s ^ n * 0
⊢ ∃ n, s ^ n * f = 0

Tactic:
simpa using

Goal state after:
X : Scheme
U : Opens ↥X
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f s : ↑Γ(X, U)
hf : (f |_ X.basicOpen s) ⋯ = 0
h : ∃ n, s ^ n * f = s ^ n * 0
⊢ ∃ n, s ^ n * f = 0
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)
⊢ (↑U).Nonempty

Tactic:
simpa using

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
⊢ (↑U).Nonempty
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case zero
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Tactic:
simpa using

Goal state after:
case zero
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) 0, ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case succ
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n✝ : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'

Tactic:
simpa using

Goal state after:
case succ
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
x : ↥X
hxV : x ∈ ↑↑V
hxU : x ∈ ↑↑U
hx : ∀ f ∈ I.ideal U, x ∉ X.basicOpen f
s : ↑Γ(X, ↑V)
hfU : s ∈ I.ideal V
hxs : x ∈ X.basicOpen s
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
inst : IsLocalization.Away f ↑Γ(X, X.basicOpen f)
this :
  (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s ∈
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U)
s' : ↥(I.ideal U)
n✝ : ℕ
hs' :
  (x ∈
      X.basicOpen
        ((CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) s *
          (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).2)) =
    (x ∈ X.basicOpen ((algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) ↑(s', ⟨(fun x ↦ f ^ x) (n✝ + 1), ⋯⟩).1))
⊢ x ∈ X.basicOpen ↑s'
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
x : ↥X
U : ↑X.affineOpens
h : x ∈ ↑U
⊢ x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)

Tactic:
simpa using

Goal state after:
X : Scheme
I : X.IdealSheafData
x : ↥X
U : ↑X.affineOpens
h : x ∈ ↑U
⊢ x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)
Module: Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
U : ↥X → Scheme
i : (x : ↥X) → U x ⟶ X
x✝ : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ { I₀ := ↥X, X := U, f := i }.presieve₀ ∈ Scheme.jointlySurjectivePrecoverage.coverings X

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X ⟶ Y
hf : Function.Injective ⇑f
U : ↥X → Scheme
i : (x : ↥X) → U x ⟶ X
x✝ : ∀ (x : ↥X), IsOpenImmersion (i x)
hxi : ∀ (x : ↥X), x ∈ Scheme.Hom.opensRange (i x)
hi : ∀ (x : ↥X), IsOpenImmersion (i x ≫ f)
⊢ ∀ (x : ↥X), ∃ i_1 y, (i i_1) y = x
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
⊢ ∀ (J : Ideal ↑S) (x : J.IsPrime),
    (fun {R S} [CommRing R] [CommRing S] ↦ Q)
      (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) J) J (CommRingCat.Hom.hom φ) ⋯)

Tactic:
intro P hP

Goal state after:
P✝ : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P✝ Q
X Y : Scheme
f : X ⟶ Y
hQ : OfLocalizationPrime fun {R S} [CommRing R] [CommRing S] ↦ Q
hQi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ Q
R S : CommRingCat
hY : IsAffine (Spec R)
hX : IsAffine (Spec S)
φ : R ⟶ S
H : ∀ (x : ↥(Spec S)), Q (CommRingCat.Hom.hom (Scheme.Hom.stalkMap (Spec.map φ) x))
P : Ideal ↑S
hP : P.IsPrime
⊢ Q (Localization.localRingHom (Ideal.comap (CommRingCat.Hom.hom φ) P) P (CommRingCat.Hom.hom φ) ⋯)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ vanishingIdeal ⊥.support = X.nilradical

Tactic:
vanishingIdeal_support,

Goal state after:
X : Scheme
⊢ ⊥.radical = X.nilradical
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n✝ : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n✝, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ (fun x ↦ s ^ x) n * x ∈ RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : QuasiCompact f
U✝ U : ↑Y.affineOpens
s : ↑Γ(Y, ↑U)
this : IsLocalization.Away s ↑Γ(Y, Y.basicOpen s)
x : ↑Γ(Y, ↑U)
n✝ : ℕ
hx :
  IsLocalization.mk' (↑Γ(Y, Y.basicOpen s)) x ⟨(fun x ↦ s ^ x) n✝, ⋯⟩ ∈
    RingHom.ker (CommRingCat.Hom.hom (f.app ↑(Y.affineBasicOpen s)))
H : ((CommRingCat.Hom.hom (f.app ↑U)) x |_ X.basicOpen ((CommRingCat.Hom.hom (f.app ↑U)) s)) ⋯ = 0
n : ℕ
hn : (ConcreteCategory.hom (f.app ↑U)) s ^ n * (ConcreteCategory.hom (f.app ↑U)) x = 0
⊢ (CommRingCat.Hom.hom (f.app ↑U)) s ^ n * (CommRingCat.Hom.hom (f.app ↑U)) x = 0
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
x : ↥(pullback (I.glueDataObjι U) (X.homOfLE ⋯))
x✝ : x ∈ ⊤
⊢ x ∈ (F ≫ (↑U ⊓ ↑V).ι) ⁻¹ᵁ ↑V

Tactic:
simpa using

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
x : ↥(pullback (I.glueDataObjι U) (X.homOfLE ⋯))
x✝ : x ∈ ⊤
⊢ ↑((TopCat.Hom.hom F.base) x) ∈ ↑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 ⋯)
x✝¹ : ↑Γ(X, ↑V)
hx : x✝¹ ∈ I.ideal V
x : ↥↑(↑U ⊓ ↑V)
x✝ : x ∈ ⊤
⊢ x ∈ (↑U ⊓ ↑V).ι ⁻¹ᵁ ↑V

Tactic:
simpa using

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
x : ↥↑(↑U ⊓ ↑V)
x✝ : x ∈ ⊤
⊢ ↑x ∈ ↑V
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:
simpa using

Goal state after:
X Y : Scheme
f : X.Hom Y
inst✝ : IsEmpty ↥X
U : ↑Y.affineOpens
x : ↑Γ(Y, ↑U)
x✝ : x ∈ ⊤.ideal U
⊢ (CommRingCat.Hom.hom (f.app ↑U)) x = 0
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:
simpa using

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
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
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
simpa using

Goal state after:
X Y : Scheme
f : X.Hom Y
H : f.ker = ⊤
⊢ IsEmpty ↥X
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
x : ↥Y
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ ⋃ i, ↑(ker (𝒰.f i ≫ f)).support ↔ x ∈ ↑f.ker.support

Tactic:
simpa using

Goal state after:
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
x : ↥Y
U : TopologicalSpace.Opens ↥Y
hU : U ∈ Y.affineOpens
hxU : x ∈ ↑U
⊢ (∃ i, x ∈ (ker (𝒰.f i ≫ f)).support) ↔ x ∈ f.ker.support
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)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ (CommRingCat.Hom.hom (Hom.app f' ↑W)) x = 0 ↔ (CommRingCat.Hom.hom (Hom.app f' ↑W ≫ e.inv)) x = 0

Tactic:
simpa using

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)
this : (Hom.appIso iV ↑W).inv ≫ Hom.app f (iV ''ᵁ ↑W) = Hom.app f' ↑W ≫ e.inv
⊢ (CommRingCat.Hom.hom (Hom.app f' ↑W)) x = 0 ↔
    (CommRingCat.Hom.hom e.inv) ((CommRingCat.Hom.hom (Hom.app f' ↑W)) x) = 0
Module: Mathlib.AlgebraicGeometry.Morphisms.Affine

Goal state before:
pp: X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ ↑((X.basicOpen r).ι ''ᵁ (X.basicOpen r).ι ⁻¹ᵁ U) = ↑(U ⊓ X.basicOpen r)

Tactic:
refine Set.image_preimage_eq_inter_range.trans ?_

Goal state after:
X✝ Y Z : Scheme
f : X✝ ⟶ Y
g : Y ⟶ Z
X : Scheme
r : ↑Γ(X, ⊤)
U : X.Opens
hU : IsAffineOpen U
⊢ U.1 ∩ Set.range ⇑(X.basicOpen r).ι = ↑(U ⊓ X.basicOpen r)