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

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
this :
  ∀ {X Y : Scheme} [IsAffine Y] (a : ↑Γ(Y, ⊤)) (f : X ⟶ ↑(Y.basicOpen a)), P f → IsAffine X → P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f ≫ (Y.basicOpen a).ι)

Tactic:
]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
this :
  ∀ {X Y : Scheme} [IsAffine Y] (a : ↑Γ(Y, ⊤)) (f : X ⟶ ↑(Y.basicOpen a)), P f → IsAffine X → P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
⊢ ∀ (i : ↑X.affineOpens), P ((↑i).ι ≫ f ≫ (Y.basicOpen a).ι)
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
this :
  ∀ {X Y : Scheme} [IsAffine Y] (a : ↑Γ(Y, ⊤)) (f : X ⟶ ↑(Y.basicOpen a)), P f → IsAffine X → P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : ↑X.affineOpens
⊢ P (((↑V).ι ≫ f) ≫ (Y.basicOpen a).ι)

Tactic:
]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝¹ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : P f
this :
  ∀ {X Y : Scheme} [IsAffine Y] (a : ↑Γ(Y, ⊤)) (f : X ⟶ ↑(Y.basicOpen a)), P f → IsAffine X → P (f ≫ (Y.basicOpen a).ι)
hX : ¬IsAffine X
V : ↑X.affineOpens
⊢ P (((↑V).ι ≫ f) ≫ (Y.basicOpen a).ι)
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: 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)
⊢ Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) =
    Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal U)

Tactic:
]

Goal state after:
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)
⊢ Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U ⊓ J.ideal U) =
    Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (I.ideal U) ⊓
      Ideal.map (algebraMap ↑Γ(X, ↑U) ↑Γ(X, X.basicOpen f)) (J.ideal 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)
⊢ ⇑(X.affineCover.f i) ⁻¹' closure {(X.affineCover.f i) x} ∈ irreducibleComponents ↥(X.affineCover.X i)

Tactic:
]

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.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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))

Tactic:
]

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y : Scheme
inst✝ : IsAffine Y
a : ↑Γ(Y, ⊤)
f : X ⟶ ↑(Y.basicOpen a)
hf : Q (CommRingCat.Hom.hom (Scheme.Hom.appTop f))
hX : IsAffine X
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appTop (f ≫ (Y.basicOpen a).ι)))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ closure {x} ∈ irreducibleComponents (PrimeSpectrum ↑R)

Tactic:
]

Goal state after:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
hx : closure {x} ∈ irreducibleComponents ↥(Spec R)
inst✝ : IsReduced (Spec R)
⊢ closure {x} ∈ irreducibleComponents (PrimeSpectrum ↑R)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst✝ : IsReduced (Spec R)
hx : x.asIdeal ∈ minimalPrimes ↑R
⊢ Subsingleton (PrimeSpectrum ↑((Spec R).presheaf.stalk x))

Tactic:
]

Goal state after:
X : Scheme
R : CommRingCat
x : ↥(Spec R)
inst✝ : IsReduced (Spec R)
hx : x.asIdeal ∈ minimalPrimes ↑R
⊢ Subsingleton (PrimeSpectrum ↑((Spec R).presheaf.stalk x))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: case refine_1
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) ∈ I.ideal U

Tactic:
]

Goal state after:
case refine_1
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) ∈ I.ideal U
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
⊢ ∀ (i_1 : ↑Z.affineOpens), P ((f ≫ i) ∣_ ↑i_1)

Tactic:
]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
⊢ ∀ (i_1 : ↑Z.affineOpens), P ((f ≫ i) ∣_ ↑i_1)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: 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
⊢ False

Tactic:
]

Goal state after:
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
⊢ False
Module: Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties

Goal state before:
pp: case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ i ⁻¹ᵁ ↑U ≫ i ∣_ ↑U)

Tactic:
]

Goal state after:
case inr
P : MorphismProperty Scheme
Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
inst✝ : HasRingHomProperty P Q
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
this : ∀ {X Y Z : Scheme} (i : Y ⟶ Z), IsOpenImmersion i → ∀ (f : X ⟶ Y), P f → IsAffine Z → P (f ≫ i)
hZ : ¬IsAffine Z
U : ↑Z.affineOpens
⊢ P (f ∣_ i ⁻¹ᵁ ↑U ≫ i ∣_ ↑U)
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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)

Tactic:
]

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P ((f ≫ e.hom) ≫ (Scheme.Hom.opensRange i).ι)
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.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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P f

Tactic:
]

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
hQ : RingHom.StableUnderCompositionWithLocalizationAwaySource fun {R S} [CommRing R] [CommRing S] ↦ Q
X Y Z : Scheme
i : Y ⟶ Z
hi : IsOpenImmersion i
f : X ⟶ Y
hf : P f
hZ : IsAffine Z
e : Y ≅ ↑(Scheme.Hom.opensRange i) := IsOpenImmersion.isoOfRangeEq i (Scheme.Hom.opensRange i).ι ⋯
⊢ P f
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

Tactic:
]

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

Goal state before:
pp: case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y

Tactic:
]

Goal state after:
case exists_of_eq
X : Scheme
U : X.Opens
hU : IsCompact U.carrier
hU' : IsQuasiSeparated U.carrier
f x y : ↑Γ(X, U)
⊢ (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (x - y) = 0 → ∃ c, ↑c * x = ↑c * y
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:
]

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

Goal state before:
pp: X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op))

Tactic:
]

Goal state after:
X Y Z : Scheme
f✝ : X ⟶ Y
inst✝¹ : CompactSpace ↥X
inst✝ : QuasiSeparatedSpace ↥X
f : ↑Γ(X, ⊤)
⊢ Function.Bijective
    ⇑(ConcreteCategory.hom (Scheme.Hom.app X.toSpecΓ (PrimeSpectrum.basicOpen f) ≫ X.presheaf.map (eqToHom ⋯).op))
Module: Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)
⊢ 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)

Tactic:
]

Goal state after:
X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
x : ↥X
hxU : x ∈ ↑U
f : ↑Γ(X, ↑U)
g : ↑Γ(X, ↑V)
hfg : X.basicOpen f = X.basicOpen g
hxf : x ∈ X.basicOpen f
this :
  Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal U) =
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE ⋯).op)) (I.ideal V)
⊢ 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.IdealSheaf.Basic

Goal state before:
pp: X : Scheme
I : X.IdealSheafData
U V : ↑X.affineOpens
h : U ≤ V
⊢ Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V) ≤
    Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (homOfLE h).op)) (I.ideal V)

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) a * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ False

Tactic:
]

Goal state after:
X : Scheme
inst✝ : IsReduced X
H : IrreducibleSpace ↥X
U : X.Opens
hU : Nonempty ↥↑U
this : ∃ x y, x ≠ y
a b : ↑(X.presheaf.obj (op U))
h : (↑(X.basicOpen a)).Nonempty ∧ (↑(X.basicOpen b)).Nonempty
x : ↥X
hxU : x ∈ U
hx₁ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x hxU)) a)
w✝ : x ∈ U
hx₂ : IsUnit ((ConcreteCategory.hom (X.toRingedSpace.presheaf.germ U x w✝)) b)
e : (ConcreteCategory.hom (X.presheaf.germ U x hxU)) a * (ConcreteCategory.hom (X.presheaf.germ U x hxU)) b = 0
⊢ False
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)
⊢ ↑V ≤ ⨆ f, X.basicOpen ↑f

Tactic:
]

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

Goal state before:
pp: case refine_1
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 : ↑Γ(X, ↑⟨V, hV⟩)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))

Tactic:
]

Goal state after:
case refine_1
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 : ↑Γ(X, ↑⟨V, hV⟩)
hr : r ∈ s
hrs : x ∈ X.basicOpen r
⊢ Q (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e ≫ X.presheaf.map (homOfLE ⋯).op))
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
U : X.Opens
hU : Nonempty ↥↑U
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
]

Goal state after:
case component_integral
X Y : Scheme
f : X ⟶ Y
inst✝² : IsOpenImmersion f
inst✝¹ : IsIntegral Y
inst✝ : Nonempty ↥X
U : X.Opens
hU : Nonempty ↥↑U
⊢ IsDomain ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)
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)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
j : ↥↑V
⊢ Submodule.restrictScalars (↑Γ(X, ↑V)) (I.ideal ⟨X.basicOpen (r j), ⋯⟩) ≤
    Submodule.restrictScalars (↑Γ(X, ↑V)) (J.ideal ⟨X.basicOpen (r j), ⋯⟩)

Tactic:
]

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)
this : Ideal.span (Set.range r) = ⊤
inst : ∀ (f : ↑Γ(X, ↑V)), IsLocalization.Away f ↑Γ(X, X.basicOpen f)
j : ↥↑V
⊢ Submodule.restrictScalars (↑Γ(X, ↑V)) (I.ideal ⟨X.basicOpen (r j), ⋯⟩) ≤
    Submodule.restrictScalars (↑Γ(X, ↑V)) (J.ideal ⟨X.basicOpen (r j), ⋯⟩)
Module: Mathlib.AlgebraicGeometry.Properties

Goal state before:
pp: X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
⊢ ∀ (a : ↑Γ(X, V)), (ConcreteCategory.hom (X.presheaf.map i.op)) a = 0 → a = 0

Tactic:
]

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
⊢ ∀ (a : ↑Γ(X, V)), (ConcreteCategory.hom (X.presheaf.map i.op)) a = 0 → a = 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)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥

Tactic:
]

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : X.basicOpen ((ConcreteCategory.hom (X.presheaf.map i.op)) x) = ⊥
⊢ X.basicOpen x = ⊥
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)
hx : U ⊓ X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥

Tactic:
]

Goal state after:
X : Scheme
inst✝ : IsIntegral X
U V : X.Opens
i : U ⟶ V
H : Nonempty ↥↑U
x : ↑Γ(X, V)
hx : U ⊓ X.basicOpen x = ⊥
⊢ X.basicOpen x = ⊥
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 H

Goal state after: