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

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ ((glueData F).ι j) ((F.map kj) y) = (TopCat.Hom.hom ((glueData F).ι j).base) ((TopCat.Hom.hom (F.map kj).base) y)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Gluing

Goal state before:
pp: J : Type w
inst✝⁴ : Category.{v, w} J
F : J ⥤ Scheme
inst✝³ : ∀ {i j : J} (f : i ⟶ j), IsOpenImmersion (F.map f)
inst✝² : (F ⋙ forget).IsLocallyDirected
inst✝¹ : Quiver.IsThin J
inst✝ : Small.{u, w} J
i j : Shrink.{u, w} J
x : ↥((glueData F).V (i, j))
k : Shrink.{u, w} J
ki : ↓k ⟶ ↓(i, j).1
kj : ↓k ⟶ ↓(i, j).2
y : ↥(F.obj ⟨↓k, (ki, kj)⟩.fst)
hy : (F.map ki) y = ((glueData F).f i j) x
⊢ (TopCat.Hom.hom ((glueData F).ι i).base) ((TopCat.Hom.hom (F.map ki).base) y) =
    (TopCat.Hom.hom ((glueData F).ι i).base) ((F.map ki) y)

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing

Goal state before:
pp: case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
⊢ ∀ {m : s.pt ⟶ (D.vPullbackCone i j).pt},
    m ≫ (D.vPullbackCone i j).fst = s.fst → m ≫ (D.vPullbackCone i j).snd = s.snd → m = lift (D.f i j) s.fst ⋯

Tactic:
intro m e₁ _

Goal state after:
case refine_4
C : Type u
inst✝¹ : Category.{v, u} C
D : GlueData C
inst✝ : HasLimits C
i j : D.J
s : PullbackCone (D.ι i) (D.ι j)
m : s.pt ⟶ (D.vPullbackCone i j).pt
e₁ : m ≫ (D.vPullbackCone i j).fst = s.fst
a✝ : m ≫ (D.vPullbackCone i j).snd = s.snd
⊢ m = lift (D.f i j) s.fst ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.Constructors

Goal state before:
pp: P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
⊢ IsZariskiLocalAtSource P.diagonal

Tactic:
refine IsZariskiLocalAtSource.mk' (fun {X Y} f U hf ↦ ?_) (fun {X Y} f {ι} U hU hf ↦ ?_)

Goal state after:
case refine_1
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
U : X.Opens
hf : P.diagonal f
⊢ P.diagonal (U.ι ≫ f)

case refine_2
P : MorphismProperty Scheme
inst✝² : P.HasOfPostcompProperty IsOpenImmersion
inst✝¹ : P.RespectsRight IsOpenImmersion
inst✝ : IsZariskiLocalAtSource P
g : {X Y : Scheme} → (f : X ⟶ Y) → (U : X.Opens) → pullback (U.ι ≫ f) (U.ι ≫ f) ⟶ pullback f f :=
  fun {X Y} f U ↦ pullback.map (U.ι ≫ f) (U.ι ≫ f) f f U.ι U.ι (𝟙 Y) ⋯ ⋯
X Y : Scheme
f : X ⟶ Y
ι : Type u_1
U : ι → X.Opens
hU : iSup U = ⊤
hf : ∀ (i : ι), P.diagonal ((U i).ι ≫ f)
⊢ P.diagonal f
Module: Mathlib.RingTheory.RingHom.Locally

Goal state before:
pp: P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hPi : RespectsIso fun {R S} [CommRing R] [CommRing S] ↦ P
hPl : LocalizationPreserves fun {R S} [CommRing R] [CommRing S] ↦ P
hPc : StableUnderComposition fun {R S} [CommRing R] [CommRing S] ↦ P
R S T : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
sf : Finset S
hsfone : Ideal.span ↑sf = ⊤
hsf : ∀ t ∈ sf, P ((algebraMap S (Localization.Away t)).comp f)
sg : Finset T
hsgone : Ideal.span ↑sg = ⊤
hsg : ∀ t ∈ sg, P ((algebraMap T (Localization.Away t)).comp g)
a : ↥sf
b : ↥sg
g' : S →+* Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)).comp g
a' : Localization.Away ↑b := (algebraMap T (Localization.Away ↑b)) (g ↑a)
x : R
⊢ (algebraMap T (Localization.Away ((algebraMap T (Localization.Away ↑b)) (g ↑a)))) (g (f x)) =
    (algebraMap (Localization.Away ↑b) (Localization.Away (g' ↑a))) (g' (f x))

Tactic:
rfl

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

Goal state before:
pp: case e'_5.fst
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (Spec.map (CommRingCat.ofHom Algebra.TensorProduct.includeLeftRingHom) ≫ iX) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).1

Tactic:
rfl

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

Goal state before:
pp: x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ SurjectiveOnStalks x✝ ∧ IsEmbedding ⇑x✝ ↔
    (@SurjectiveOnStalks ⊓ topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsEmbedding) x✝

Tactic:
rfl

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

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ IsEmbedding ⇑(Spec.map f) ∧ SurjectiveOnStalks (Spec.map f) ↔
    IsEmbedding (PrimeSpectrum.comap (CommRingCat.Hom.hom f)) ∧ SurjectiveOnStalks (Spec.map f)

Tactic:
rfl

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

Goal state before:
pp: case e'_5.snd
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
inst✝ : SurjectiveOnStalks g
L : ↥(pullback f g) → ↥X × ↥Y := fun x ↦ ((pullback.fst f g) x, (pullback.snd f g) x)
R A B : CommRingCat
iX : Spec A ⟶ X
iY : Spec B ⟶ Y
iS : Spec R ⟶ S
a✝² : IsOpenImmersion iX
a✝¹ : IsOpenImmersion iY
a✝ : IsOpenImmersion iS
φ : R ⟶ A
e₁ : Spec.map φ ≫ iS = iX ≫ f
ψ : R ⟶ B
e₂ : Spec.map ψ ≫ iS = iY ≫ g
H : (CommRingCat.Hom.hom ψ).SurjectiveOnStalks
algInst✝¹ : Algebra ↑R ↑A := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑R ↑B := (CommRingCat.Hom.hom ψ).toAlgebra
e_1✝ :
  ↥(pullback (Spec.map φ) (Spec.map ψ)) =
    ↥(pullback (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑A))) (Spec.map (CommRingCat.ofHom (algebraMap ↑R ↑B))))
x : ↥(Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))
⊢ (Spec.map (CommRingCat.ofHom ↑Algebra.TensorProduct.includeRight) ≫ iY) x =
    (Prod.map (⇑iX) (⇑iY)
        (PrimeSpectrum.tensorProductTo (↑R) (↑A) (↑B) ((𝟙 (Spec (CommRingCat.of (TensorProduct ↑R ↑A ↑B)))) x))).2

Tactic:
rfl

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

Goal state before:
pp: X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    QuasiSeparatedSpace ↥X

Tactic:
rw [quasiSeparatedSpace_iff_forall_affineOpens]

Goal state after:
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ ⦃U₁ U₂ : Scheme⦄ (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) [inst : IsAffine U₁] [inst_1 : IsAffine U₂] [IsOpenImmersion f₁]
      [IsOpenImmersion f₂],
      (fun X x x_1 x_2 ↦ CompactSpace ↥X) (pullback f₁ f₂) (pullback (f₁ ≫ f) (f₂ ≫ f)) (pullback.mapDesc f₁ f₂ f) ⋯) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (U : Y.Opens), IsAffineOpen U → CompactSpace ↑↑(f ⁻¹ᵁ U)) ↔
    ∀ (a : Y.Opens) (b : a ∈ Y.affineOpens), CompactSpace ↥↑(f ⁻¹ᵁ a)

Tactic:
rfl

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

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

Tactic:
let 𝒰 := (Z.affineCover.pullback₁ g).bind fun x => Scheme.affineCover _

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : QuasiSeparated (f ≫ g)
𝒰 : (Scheme.precoverage IsOpenImmersion).ZeroHypercover Y :=
  (Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).bind fun x ↦
    ((Precoverage.ZeroHypercover.pullback₁ g Z.affineCover).X x).affineCover
⊢ QuasiSeparated f
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: case e'_2
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H✝ : (x |_ X.basicOpen f) ⋯ = 0
s : Set ↑X.affineOpens
hs : s.Finite
e : U = ⨆ i, ↑↑i
h₁ : ∀ (i : ↑s), ↑↑i ≤ U
i : ↑s
H : (ConcreteCategory.hom (X.presheaf.map (homOfLE ⋯).op)) x = 0
⊢ (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op))) x =
    (ConcreteCategory.hom (X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ?refine_1.convert_1).op))) x

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
⊢ 1 ≤ ⨅ J ∈ (span {x}).minimalPrimes, J.height

Tactic:
refine le_iInf₂ fun q hq => ?_

Goal state after:
R : Type u_1
inst✝ : CommRing R
x : R
hx : x ∈ nonZeroDivisors R
q : Ideal R
hq : q ∈ (span {x}).minimalPrimes
⊢ 1 ≤ q.height
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
p : Ideal R
n : ℕ
inst✝ : p.IsPrime
a✝¹ : Ideal R
a✝ : a✝¹.IsPrime
⊢ (PrimeSpectrum.equivSubtype R).symm ⟨a✝¹, a✝⟩ < { asIdeal := p, isPrime := inst✝ } →
      Order.height ((PrimeSpectrum.equivSubtype R).symm ⟨a✝¹, a✝⟩) < ↑n ↔
    a✝¹ < p → Order.height { asIdeal := a✝¹, isPrime := a✝ } < ↑n

Tactic:
rfl

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

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ Q (Spec.map φ)

Tactic:
HasRingHomProperty.Spec_iff (P := Q)

Goal state after:
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
Q : MorphismProperty Scheme := affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
this : HasRingHomProperty Q fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
S R : CommRingCat
φ : S ⟶ R
⊢ P (Spec.map φ) ↔ P (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom φ)))

Tactic:
rfl

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

Goal state before:
pp: P P' : MorphismProperty Scheme
Q Q' : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
inst✝ : HasRingHomProperty P' fun {R S} [CommRing R] [CommRing S] ↦ Q'
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ ((∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
        Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))) ∧
      ∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
        Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))) ↔
    ∀ (U : ↑Y✝.affineOpens) (V : ↑X✝.affineOpens) (e : ↑V ≤ f✝ ⁻¹ᵁ ↑U),
      Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e)) ∧
        Q' (CommRingCat.Hom.hom (Scheme.Hom.appLE f✝ (↑U) (↑V) e))

Tactic:
grind

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

Goal state before:
pp: case hcover
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 ⋯).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 ⋯).op)) x
s : Set ↑X.affineOpens
hs' : s.Finite
this : Finite ↑s
val✝ : Fintype ↑s
hs : S ⊓ ↑U = ⨆ i, ↑↑i
hs₁ : ∀ (i : ↑s), ↑↑i ≤ S
hs₂ : ∀ (i : ↑s), ↑↑i ≤ ↑U
n : ↑s → ℕ
hn : ∀ (i : ↑s) (m : ℕ), n i ≤ m → (((f |_ S) ⋯ ^ (m + n₂) * y₁) |_ ↑↑i) ⋯ = (((f |_ ↑U) ⋯ ^ (m + n₁) * y₂) |_ ↑↑i) ⋯
⊢ S ⊓ ↑U ≤ ⨆ i, ↑↑i

Tactic:
exact le_of_eq hs

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

Goal state before:
pp: X : Scheme
s : Set X.IdealSheafData
⊢ sSup (Set.range (ideal ∘ Subtype.val)) = ⨆ i, (↑i).ideal

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case inr
X : Scheme
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx : closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥X
inst : IsReduced (X.affineCover.X i)
⊢ ⇑(X.affineCover.f i) ⁻¹' closure (⇑(X.affineCover.f i) '' {x}) ∈ irreducibleComponents ↥(X.affineCover.X i)

Tactic:
Set.image_singleton

Goal state after:
case inr
X : Scheme
inst✝ : IsReduced X
this :
  ∀ (X : Scheme) (x : ↥X),
    closure {x} ∈ irreducibleComponents ↥X → ∀ [IsReduced X], (∃ R, X = Spec R) → IsField ↑(X.presheaf.stalk x)
hX : ¬∃ R, X = Spec R
i : X.affineCover.I₀
x : ↥(X.affineCover.X i)
hx : closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥X
inst : IsReduced (X.affineCover.X i)
⊢ ⇑(X.affineCover.f i) ⁻¹' closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥(X.affineCover.X i)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ sSup (Set.range (ideal ∘ I)) = sSup (Set.range fun i ↦ (I i).ideal)

Tactic:
Function.comp_def

Goal state after:
X : Scheme
ι : Type u_1
I : ι → X.IdealSheafData
⊢ sSup (Set.range fun x ↦ (I x).ideal) = sSup (Set.range fun i ↦ (I i).ideal)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ ∀ (x : ↥X) (h_1 : x ∈ ↑U),
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1))
        (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
      Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x h_1)) (I.ideal U)

Tactic:
intro x hxU

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU))
      (Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ (↑U) x hxU)) (I.ideal U)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case e
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 : StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
inst : HasRingHomProperty P fun {R S} [CommRing R] [CommRing S] ↦ Q
⊢ P = P

Tactic:
rfl

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

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

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

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

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

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

Goal state before:
pp: ⊢ IsOpenImmersion =
    (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenEmbedding) ⊓
      stalkwise fun {R S} [CommRing R] [CommRing S] x ↦ Function.Bijective ⇑x

Tactic:
by
  ext
  exact IsOpenImmersion.iff_isIso_stalkMap.trans
    (and_congr Iff.rfl (forall_congr' fun x ↦ ConcreteCategory.isIso_iff_bijective _))

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

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
⊢ IsOpenImmersion f✝ ∧ Surjective f✝ ↔ (IsOpenImmersion ⊓ @Surjective) f✝

Tactic:
rfl

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(IsAffineOpen.isoSpec ⋯).inv '' PrimeSpectrum.zeroLocus ↑(I.ideal U) =
    (fun a ↦ (IsAffineOpen.isoSpec ⋯).inv a) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
rfl

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

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
V : ↑X.affineOpens
f : ↑Γ(X, ↑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 ⋯).op)) ⋯).toAlgebra
f' : ↑Γ(X, ↑V) ⧸ I.ideal V := (Ideal.Quotient.mk (I.ideal V)) f
this :
  IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f)
    (↑Γ(X, ↑(X.affineBasicOpen f)) ⧸ I.ideal (X.affineBasicOpen f))
⊢ ↑((Opens.comap { toFun := comap (Ideal.Quotient.mk (I.ideal V)), continuous_toFun := ⋯ })
        (IsAffineOpen.fromSpec ⋯ ⁻¹ᵁ X.basicOpen f)) =
    ↑((Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal V))) ≫ IsAffineOpen.fromSpec ⋯) ⁻¹ᵁ X.basicOpen f)

Tactic:
rfl

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

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
I : X.IdealSheafData
⊢ I ≤ X.nilradical ↔ I = ⊥

Tactic:
nilradical_eq_bot,

Goal state after:
X : Scheme
inst✝ : IsReduced X
I : X.IdealSheafData
⊢ I ≤ ⊥ ↔ I = ⊥
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Y.residue ((ConcreteCategory.hom f.base) x) ≫
      CommRingCat.ofHom (IsLocalRing.ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x

Tactic:
rfl

Goal state after:
Module: Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField

Goal state before:
pp: X Y : LocallyRingedSpace
f : X ⟶ Y
V : Opens ↑Y.toTopCat
x : ↥((Opens.map f.base).obj V)
a : ↑(Y.presheaf.obj (op V))
⊢ (IsLocalRing.residue ↑(X.presheaf.stalk ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a)) =
    (ConcreteCategory.hom (X.residue ↑x))
      ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj V) ↑x ⋯))
        ((ConcreteCategory.hom (f.c.app (op V))) a))

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.Stalk

Goal state before:
pp: R : CommRingCat
inst✝ : IsLocalRing ↑R
⊢ StructureSheaf.toStalk (↑R) (closedPoint ↑R) =
    (Scheme.ΓSpecIso R).inv ≫ (Spec R).presheaf.germ ⊤ (closedPoint ↑R) trivial

Tactic:
rfl

Goal state after:
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
H : ⊤ ≤ X.homOfLE ⋯ ⁻¹ᵁ (↑U).ι ⁻¹ᵁ ↑V
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE ⋯).op) ≫ Hom.appLE F ⊤ (F ⁻¹ᵁ ⊤) ⋯ =
    X.presheaf.map ((homOfLE ⋯).op ≫ (homOfLE ⋯).op ≫ (homOfLE ⋯).op) ≫ Hom.appLE F ⊤ ⊤ ⋯

Tactic:
rfl

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 x

Tactic:
rfl

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:
rfl

Goal state after:
Module: Mathlib.AlgebraicGeometry.ResidueField

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
x : ↥X
⊢ Y.residue (f x) ≫ CommRingCat.ofHom (ResidueField.map (CommRingCat.Hom.hom (Hom.stalkMap f x))) =
    Hom.stalkMap f x ≫ X.residue x

Tactic:
rfl

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

Goal state after: