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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this : SurjectiveOnStalks (pullback.fst f g)
⊢ IsPreimmersion (pullback.fst f g)

Tactic:
constructor

Goal state after:
X Y Z : Scheme
f : X ⟶ Z
g : Y ⟶ Z
x✝¹ : HasPullback f g
x✝ : IsPreimmersion g
this : SurjectiveOnStalks (pullback.fst f g)
⊢ IsEmbedding ⇑(pullback.fst f g)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ QuasiCompact f

Tactic:
constructor

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsIso f
⊢ ∀ (U : Set ↥Y), IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

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

Tactic:
constructor

Goal state after:
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : QuasiCompact f
inst✝ : QuasiCompact g
⊢ ∀ (U : Set ↥Z), IsOpen U → IsCompact U → IsCompact (⇑(f ≫ g) ⁻¹' U)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
constructor

Goal state after:
case mp
X : Scheme
⊢ (∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)) →
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

case mpr
X : Scheme
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ (U V : Set ↥X), IsOpen U → IsCompact U → IsOpen V → IsCompact V → IsCompact (U ∩ V)
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ AffineTargetMorphismProperty.IsLocal fun X x x_1 x_2 ↦ CompactSpace ↥X

Tactic:
constructor

Goal state after:
case respectsIso
X Y : Scheme
f : X ⟶ Y
⊢ (AffineTargetMorphismProperty.toProperty fun X x x_1 x_2 ↦ CompactSpace ↥X).RespectsIso

case to_basicOpen
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (r : ↑Γ(Y, ⊤)), CompactSpace ↥X → CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen r)

case of_basicOpenCover
X Y : Scheme
f : X ⟶ Y
⊢ ∀ {X Y : Scheme} [IsAffine Y] (f : X ⟶ Y) (s : Finset ↑Γ(Y, ⊤)),
    Ideal.span ↑s = ⊤ → (∀ (r : ↥s), CompactSpace ↥↑(f ⁻¹ᵁ Y.basicOpen ↑r)) → CompactSpace ↥X
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) ⋯) ↔
    ∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)

Tactic:
constructor

Goal state after:
case mp
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)

case mpr
X Y : Scheme
inst✝ : IsAffine Y
f : X ⟶ Y
⊢ (∀ (U V : ↑X.affineOpens), IsCompact (↑↑U ∩ ↑↑V)) →
    ∀ ⦃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) ⋯
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ CompactSpace ↥X

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : QuasiCompact f
inst✝ : CompactSpace ↥Y
⊢ IsCompact Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: ⊢ @QuasiSeparated = MorphismProperty.diagonal @QuasiCompact

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ QuasiSeparated x✝ ↔ MorphismProperty.diagonal (@QuasiCompact) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
⊢ (AffineTargetMorphismProperty.diagonal fun X x x_1 x_2 ↦ CompactSpace ↥X) = fun X x x_1 x_2 ↦ QuasiSeparatedSpace ↥X

Tactic:
ext

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
inst✝ : IsAffine Y✝
⊢ AffineTargetMorphismProperty.diagonal (fun X x x_1 x_2 ↦ CompactSpace ↥X) f✝ ↔ QuasiSeparatedSpace ↥X✝
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiSeparated

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥Y
f g : X ⟶ Y
⊢ CompactSpace ↥(equalizer f g)

Tactic:
constructor

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥Y
f g : X ⟶ Y
⊢ IsCompact Set.univ
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ((fun a ↦ U.ι a) ∘ ⇑(IsOpenImmersion.lift U.ι f ⋯)) = ↑U

Tactic:
← TopCat.coe_comp,

Goal state after:
X : Scheme
U : X.Opens
x✝ : ∃ R f, Set.range ⇑f = ↑U
R : CommRingCat
f : Spec R ⟶ X
hf : Set.range ⇑f = ↑U
⊢ Set.range ⇑(ConcreteCategory.hom ((IsOpenImmersion.lift U.ι f ⋯).base ≫ U.ι.base)) = ↑U
Module: Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact

Goal state before:
pp: X : Scheme
U : X.Opens
hU : IsCompact U.carrier
x f : ↑Γ(X, U)
H : (x |_ X.basicOpen f) ⋯ = 0
⊢ ∃ n, f ^ n * x = 0

Tactic:
obtain ⟨s, hs, e⟩ := isCompact_and_isOpen_iff_finite_and_eq_biUnion_affineOpens.mp ⟨hU, U.2⟩

Goal state after:
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.carrier = ⋃ i ∈ s, ↑↑i
⊢ ∃ n, f ^ n * x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
⊢ IsReduced S

Tactic:
constructor

Goal state after:
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
⊢ ∀ (x : S), IsNilpotent x → x = 0
Module: Mathlib.RingTheory.LocalProperties.Reduced

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ IsReduced R

Tactic:
constructor

Goal state after:
R : Type u_1
inst✝ : CommRing R
h : ∀ (J : Ideal R) (x : J.IsMaximal), (fun R x ↦ IsReduced R) (Localization.AtPrime J) OreLocalization.instCommRing
⊢ ∀ (x : R), IsNilpotent x → x = 0
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
hI :
  (∃ i, (∃ (i_1 : i ∈ I.minimalPrimes), i.primeHeight = ↑n) ∧ ∀ (i_1 : i ∈ I.minimalPrimes), ↑n ≤ i.primeHeight) ∧
    ∀ (i : Ideal R), ↑n ≤ ⨅ (h : i ∈ I.minimalPrimes), i.primeHeight
⊢ ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n

Tactic:
rcases hI with ⟨⟨p, ⟨⟨⟨hpp, hIp⟩, _⟩, h⟩, -⟩, -⟩

Goal state after:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
n : ℕ
p : Ideal R
right✝ : ∀ ⦃y : Ideal R⦄, (fun q ↦ q.IsPrime ∧ I ≤ q) y → y ≤ p → p ≤ y
hpp : p.IsPrime
hIp : I ≤ p
h : p.primeHeight = ↑n
⊢ ∃ p, ∃ (_ : p.IsPrime) (_ : I ≤ p), p.height = ↑n
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
this : I.FiniteHeight
⊢ I.height < J.height

Tactic:
exact Ideal.height_strict_mono_of_isPrime h

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height = ringKrullDim R ↔ I = IsLocalRing.maximalIdeal R

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ ↑I.height = ringKrullDim R → I = IsLocalRing.maximalIdeal R

case mpr
R : Type u_1
inst✝³ : CommRing R
inst✝² : FiniteRingKrullDim R
inst✝¹ : IsLocalRing R
I : Ideal R
inst✝ : I.IsPrime
⊢ I = IsLocalRing.maximalIdeal R → ↑I.height = ringKrullDim R
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.PropertyIsLocal fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

Tactic:
constructor

Goal state after:
case localizationAwayPreserves
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.LocalizationAwayPreserves fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

case ofLocalizationSpanTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpanTarget fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

case ofLocalizationSpan
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.OfLocalizationSpan fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))

case StableUnderCompositionWithLocalizationAwayTarget
P : MorphismProperty Scheme
inst✝¹ : IsZariskiLocalAtTarget P
inst✝ : IsZariskiLocalAtSource P
hP : RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] f ↦ P (Spec.map (CommRingCat.ofHom f))
⊢ RingHom.StableUnderCompositionWithLocalizationAwayTarget fun {R S} [CommRing R] [CommRing S] f ↦
    P (Spec.map (CommRingCat.ofHom f))
Module: Mathlib.RingTheory.Ideal.Height

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n) ↔
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n

case mpr
R : Type u_1
inst✝² : CommRing R
p : Ideal R
n : ℕ
inst✝¹ : p.IsPrime
inst✝ : IsNoetherianRing R
⊢ (∀ (q : Ideal R), q.IsPrime → q < p → (∀ (q' : Ideal R), q'.IsPrime → q < q' → ¬q' < p) → q.height < ↑n) →
    ∀ (q : Ideal R), q.IsPrime → q < p → q.height < ↑n
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'
⊢ ((affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q') =
    affineLocally fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f

Tactic:
ext

Goal state after:
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✝
⊢ ((affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q) ⊓ affineLocally fun {R S} [CommRing R] [CommRing S] ↦ Q')
      f✝ ↔
    affineLocally (fun {R S} [CommRing R] [CommRing S] f ↦ Q f ∧ Q' f) f✝
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
x : ↥X
⊢ _root_.IsReduced ↑(X.presheaf.stalk x)

Tactic:
constructor

Goal state after:
X : Scheme
inst✝ : IsReduced X
x : ↥X
⊢ ∀ (x_1 : ↑(X.presheaf.stalk x)), IsNilpotent x_1 → x_1 = 0
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ IsReduced X

Tactic:
constructor

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) IsReduced.component_reduced._autoParam
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
⊢ ⊤ = ⋂ U, X.zeroLocus ↑(⊥ U)

Tactic:
ext

Goal state after:
X : Scheme
x✝ : ↥X
⊢ x✝ ∈ ⊤ ↔ x✝ ∈ ⋂ U, X.zeroLocus ↑(⊥ U)
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)
⊢ IsField ↑(X.presheaf.stalk ((X.affineCover.f i) x))

Tactic:
refine (asIso <| (X.affineCover.f i).stalkMap x).commRingCatIsoToRingEquiv.isField
      (this _ x ?_ ⟨_, rfl⟩)

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)
⊢ closure {x} ∈ irreducibleComponents ↥(X.affineCover.X i)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
⊢ IsReduced X

Tactic:
constructor

Goal state after:
X : Scheme
inst✝ : IsIntegral X
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) IsReduced.component_reduced._autoParam
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case refine_1
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
⊢ x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) ↔ x ∈ ↑⊥

Tactic:
constructor

Goal state after:
case refine_1.mp
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
⊢ x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ }) → x ∈ ↑⊥

case refine_1.mpr
X : Scheme
inst✝ : IsIntegral X
S T : Set ↥X
hS : IsClosed S
hT : IsClosed T
h₁ : Set.univ ⊆ S ∪ T
h₂ : ∃ a, a ∉ S
h₃ : ∃ a, a ∉ T
this✝¹ : Nonempty ↥↑{ carrier := Sᶜ, is_open' := ⋯ }
this✝ : Nonempty ↥↑{ carrier := Tᶜ, is_open' := ⋯ }
this : Nonempty ↥↑({ carrier := Sᶜ, is_open' := ⋯ } ⊔ { carrier := Tᶜ, is_open' := ⋯ })
x : ↥X
⊢ x ∈ ↑⊥ → x ∈ ↑({ carrier := Sᶜ, is_open' := ⋯ } ⊓ { carrier := Tᶜ, is_open' := ⋯ })
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)
⊢ IsLocalization.Away f ↑Γ(X, X.basicOpen f)

Tactic:
constructor

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.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:
constructor

Goal state after:
case map_units
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (y : ↥(Submonoid.powers f)), IsUnit ((algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑y)

case surj
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ (z : ↑Γ(X, X.basicOpen f)),
    ∃ x, z * (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) ↑x.2 = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x.1

case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f : ↑Γ(X, U)
⊢ ∀ {x y : ↑Γ(X, U)},
    (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) x = (algebraMap ↑Γ(X, U) ↑Γ(X, X.basicOpen f)) y → ∃ c, ↑c * x = ↑c * y
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
⊢ IsIntegral X

Tactic:
constructor

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.Morphisms.QuasiSeparated

Goal state before:
pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsLocalization ?M ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)

pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsLocalization ?M ↑Γ(X, X.basicOpen f)

pp: case hf
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ?R ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) =
    algebraMap ?R ↑Γ(X, X.basicOpen f)

pp: case R
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Type ?u.56

pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ CommSemiring ?R

pp: case M
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Submonoid ?R

pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Algebra ?R ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)

pp: case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Algebra ?R ↑Γ(X, X.basicOpen f)

Tactic:
· exact StructureSheaf.IsLocalization.to_basicOpen _ _

Goal state after:
case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ IsLocalization (Submonoid.powers f) ↑Γ(X, X.basicOpen f)

case hf
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ (ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op)).comp
      (algebraMap ↑Γ(X, ⊤) ↑Γ(Spec Γ(X, ⊤), PrimeSpectrum.basicOpen f)) =
    algebraMap ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)

case inst
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Algebra ↑Γ(X, ⊤) ↑Γ(X, X.basicOpen f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
⊢ Ideal.span (Set.range r) = ⊤

Tactic:
← V.2.self_le_iSup_basicOpen_iff

Goal state after:
X : Scheme
I J : X.IdealSheafData
ι : Type u_1
U : ι → ↑X.affineOpens
hU : ⨆ i, ↑(U i) = ⊤
H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)
V : ↑X.affineOpens
i : ↥↑V → ι
r : ↥↑V → ↑Γ(X, ↑V)
rU : (x : ↥↑V) → ↑Γ(X, ↑(U (i x)))
e : ∀ (x : ↥↑V), X.basicOpen (r x) = X.basicOpen (rU x)
hxr : ∀ (x : ↥↑V), ↑x ∈ X.basicOpen (r x)
⊢ ↑V ≤ ⨆ f, X.basicOpen ↑f
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
⊢ IsIntegral X

Tactic:
constructor

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)
⊢ IsOpenImmersion (Spec.map f) ↔ ∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}

Tactic:
constructor

Goal state after:
case mp
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}

case mpr
R S : CommRingCat
f : R ⟶ S
hf : Function.Surjective ⇑(CommRingCat.Hom.hom f)
⊢ (∃ e, IsIdempotentElem e ∧ RingHom.ker (CommRingCat.Hom.hom f) = Ideal.span {e}) → IsOpenImmersion (Spec.map f)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case zero
X : Scheme
I✝¹ I✝ J K I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
⊢ x ∈ X.zeroLocus ↑((I.ideal ^ 0) U) ↔ x ∈ if 0 = 0 then ∅ else I.supportSet

Tactic:
simp_all [-mem_zeroLocus_iff, zeroLocus_mul,
      pow_succ, mem_support_iff_of_mem hxU]

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

Goal state before:
pp: case succ
X : Scheme
I✝¹ I✝ J K I : X.IdealSheafData
U : ↑X.affineOpens
x : ↥X
hxU : x ∈ ↑U
n✝ : ℕ
a✝ : x ∈ X.zeroLocus ↑((I.ideal ^ n✝) U) ↔ x ∈ if n✝ = 0 then ∅ else I.supportSet
⊢ x ∈ X.zeroLocus ↑((I.ideal ^ (n✝ + 1)) U) ↔ x ∈ if n✝ + 1 = 0 then ∅ else I.supportSet

Tactic:
simp_all [-mem_zeroLocus_iff, zeroLocus_mul,
      pow_succ, mem_support_iff_of_mem hxU]

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

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
⊢ ⊤ * I = I

Tactic:
ext

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
⊢ I * ⊤ = I

Tactic:
ext

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
⊢ ⊥ * I = ⊥

Tactic:
ext

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
⊢ I * ⊥ = ⊥

Tactic:
ext

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✝ I J K x✝ : X.IdealSheafData
⊢ x✝ ^ 0 = 1

Tactic:
ext

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✝¹