mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
⊢ ((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
      (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)) =
    map (algebraMap R x.asIdeal.ResidueField)

Tactic:
ext

Goal state after:
case hC
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
x✝ : R
m✝ : σ →₀ ℕ
⊢ coeff m✝
      (((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
              (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField))).comp
          C)
        x✝) =
    coeff m✝ (((map (algebraMap R x.asIdeal.ResidueField)).comp C) x✝)

case hX
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
f : MvPolynomial σ R
x : PrimeSpectrum R
e : x.asIdeal.ResidueField ⊗[R] MvPolynomial σ R ≃ₐ[x.asIdeal.ResidueField] MvPolynomial σ x.asIdeal.ResidueField :=
  scalarRTensorAlgEquiv
i✝ : σ
m✝ : σ →₀ ℕ
⊢ coeff m✝
      ((((↑e).comp (Algebra.TensorProduct.comm R (MvPolynomial σ R) x.asIdeal.ResidueField).toRingEquiv.toRingHom).comp
          (algebraMap (MvPolynomial σ R) (MvPolynomial σ R ⊗[R] x.asIdeal.ResidueField)))
        (X i✝)) =
    coeff m✝ ((map (algebraMap R x.asIdeal.ResidueField)) (X i✝))
Module: Mathlib.AlgebraicGeometry.Artinian

Goal state before:
pp: X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
⊢ ⨆ x, { carrier := {x}, is_open' := ⋯ } = ⊤

Tactic:
ext

Goal state after:
X✝ Y : Scheme
f : X✝ ⟶ Y
X : Scheme
inst✝¹ : DiscreteTopology ↥X
inst✝ : IsReduced X
this : ∀ {X : Scheme} [DiscreteTopology ↥X] [IsReduced X], Subsingleton ↥X → IsLocallyArtinian X
hX : ¬Subsingleton ↥X
x✝ : ↥X
⊢ x✝ ∈ ↑(⨆ x, { carrier := {x}, is_open' := ⋯ }) ↔ x✝ ∈ ↑⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Polynomial

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
⊢ (eval₂Hom (RingHom.id R) 0).comp C = RingHom.id R

Tactic:
ext

Goal state after:
R : Type u_2
inst✝ : CommRing R
σ : Type u_1
x : PrimeSpectrum R
x✝ : R
⊢ ((eval₂Hom (RingHom.id R) 0).comp C) x✝ = (RingHom.id R) x✝
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ IsNoetherian X ↔ ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))

Tactic:
constructor

Goal state after:
case mp
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ IsNoetherian X → ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))

case mpr
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
⊢ (∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))) → IsNoetherian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ CompactSpace ↥X

Tactic:
constructor

Goal state after:
case mpr.convert_3
X : Scheme
ι : Sort u_1
inst✝ : Finite ι
S : ι → ↑X.affineOpens
hS : ⨆ i, ↑(S i) = ⊤
h : ∀ (i : ι), IsNoetherianRing ↑Γ(X, ↑(S i))
⊢ IsCompact Set.univ
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsNoetherian X ↔ ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

Tactic:
constructor

Goal state after:
case mp
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ IsNoetherian X → ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)

case mpr
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
⊢ (∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)) → IsNoetherian X
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: ⊢ @GeometricallyReduced = geometrically IsReduced

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyReduced x✝ ↔ geometrically IsReduced x✝
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: ⊢ @GeometricallyIrreducible = geometrically fun x ↦ IrreducibleSpace ↥x

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyIrreducible x✝ ↔ geometrically (fun x ↦ IrreducibleSpace ↥x) x✝
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ @GeometricallyIntegral = geometrically IsIntegral

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ GeometricallyIntegral x✝ ↔ geometrically IsIntegral x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

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

Tactic:
constructor

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝¹ : UniversallyClosed (f ≫ g)
inst✝ : Surjective f
⊢ (topologically @IsClosedMap).universally g
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' :
  eval₂ (algebraMap R (Localization.Away (f t))) (⟨(fun x ↦ t ^ x) n, ⋯⟩ • (algebraMap S (Localization.Away (f t))) r)
      p =
    0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
rw [IsScalarTower.algebraMap_eq R S, Submonoid.smul_def, Algebra.smul_def,
    IsScalarTower.algebraMap_apply R S, ← map_mul, ← hom_eval₂,
    IsLocalization.map_eq_zero_iff (.powers (f t))] at hp'

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x ↦ x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
hp' : ∃ m, ↑m * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: ⊢ @IsIntegralHom = @UniversallyClosed ⊓ @IsAffineHom

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsIntegralHom x✝ ↔ (@UniversallyClosed ⊓ @IsAffineHom) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: ⊢ @IsFinite = @IsIntegralHom ⊓ @LocallyOfFiniteType

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsFinite x✝ ↔ (@IsIntegralHom ⊓ @LocallyOfFiniteType) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: ⊢ @IsClosedImmersion = @IsFinite ⊓ monomorphisms Scheme

Tactic:
ext

Goal state after:
x✝² x✝¹ : Scheme
x✝ : x✝² ⟶ x✝¹
⊢ IsClosedImmersion x✝ ↔ (@IsFinite ⊓ monomorphisms Scheme) x✝
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: X : Scheme
inst✝ : JacobsonSpace ↥X
x : ↥X
⊢ IsClosed {x} ↔ LocallyOfFiniteType (X.fromSpecResidueField x)

Tactic:
constructor

Goal state after:
case mp
X : Scheme
inst✝ : JacobsonSpace ↥X
x : ↥X
⊢ IsClosed {x} → LocallyOfFiniteType (X.fromSpecResidueField x)

case mpr
X : Scheme
inst✝ : JacobsonSpace ↥X
x : ↥X
⊢ LocallyOfFiniteType (X.fromSpecResidueField x) → IsClosed {x}
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝² : Y.IsQuasiAffine
inst✝¹ : IsImmersion f
inst✝ : CompactSpace ↥X
this✝ : IsImmersion (X.toSpecΓ ≫ Spec.map (Hom.appTop f))
this : IsImmersion X.toSpecΓ
⊢ X.IsQuasiAffine

Tactic:
constructor

Goal state after:
Module: Mathlib.AlgebraicGeometry.QuasiAffine

Goal state before:
pp: X : Scheme
inst✝ : CompactSpace ↥X
H : ∀ (x : ↥X), ∃ r, IsAffineOpen (X.basicOpen r) ∧ x ∈ X.basicOpen r
this : IsOpenImmersion X.toSpecΓ
⊢ X.IsQuasiAffine

Tactic:
constructor

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(𝒰.f i) ∘ ⇑(pullback.fst (𝒰.f i) f) ⁻¹' s)

Tactic:
← TopCat.coe_comp,

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝² : Flat f
inst✝¹ : QuasiCompact f
inst✝ : Surjective f
s : Set ↥Y
hs : IsOpen (⇑f ⁻¹' s)
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [Flat f] [QuasiCompact f] [Surjective f] (s : Set ↥Y),
    IsOpen (⇑f ⁻¹' s) → (∃ R, Y = Spec R) → IsOpen s
hY : ¬∃ R, Y = Spec R
𝒰 : Y.OpenCover := Y.affineCover
i : 𝒰.I₀
⊢ IsOpen (⇑(ConcreteCategory.hom ((pullback.fst (𝒰.f i) f).base ≫ (𝒰.f i).base)) ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S X : Scheme
v : n → ↑Γ(X, ⊤)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
ext

Goal state after:
n : Type u
S X : Scheme
v : n → ↑Γ(X, ⊤)
x✝ : n
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel x y ↔
    ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

Tactic:
constructor

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ Relation.EqvGen F.ColimitTypeRel x y →
    ∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd

case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
x y : (j : J) × F.obj j
⊢ (∃ k f g, (ConcreteCategory.hom (F.map f)) x.snd = (ConcreteCategory.hom (F.map g)) y.snd) →
    Relation.EqvGen F.ColimitTypeRel x y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) ↔
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

Tactic:
constructor

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) →
    ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y

case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
j : J
x y : F.obj j
⊢ (∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y) →
    ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) ↔
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

Tactic:
constructor

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ Function.Injective (F.descColimitType c) →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'

case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    Function.Injective (F.descColimitType c)
Module: Mathlib.CategoryTheory.Limits.Types.ColimitTypeFiltered

Goal state before:
pp: J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') ↔
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

Tactic:
constructor

Goal state after:
case mp
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x') →
    ∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x'

case mpr
J : Type u
inst✝¹ : Category.{v, u} J
inst✝ : IsFiltered J
F : J ⥤ Type w₀
c : F.CoconeTypes
⊢ (∀ (j : J) (x x' : F.obj j),
      c.ι j x = c.ι j x' → ∃ k f, (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) x') →
    ∀ (j j' : J) (x : F.obj j) (x' : F.obj j'),
      c.ι j x = c.ι j' x' → ∃ k f f', (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) x'
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: case inr
n : Type u
S : Scheme
h : IsReduced S
this : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)

Tactic:
have : IsReduced 𝔸(n; S.affineCover.X i) := this _ ⟨_, rfl⟩

Goal state after:
case inr
n : Type u
S : Scheme
h : IsReduced S
this✝ : ∀ {n : Type u} (S : Scheme) [h : IsReduced S], (∃ R, S = Spec R) → IsReduced 𝔸(n; S)
hS : ¬∃ R, S = Spec R
i : (Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).I₀
this : IsReduced 𝔸(n; S.affineCover.X i)
⊢ IsReduced ((Precoverage.ZeroHypercover.pullback₁ (𝔸(n; S) ↘ S) S.affineCover).X i)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n

Tactic:
constructor

Goal state after:
case mp
n : Type u
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) → IsEmpty ↥S ∨ IsEmpty n

case mpr
n : Type u
S : Scheme
⊢ IsEmpty ↥S ∨ IsEmpty n → IsIntegralHom (𝔸(n; S) ↘ S)
Module: Mathlib.AlgebraicGeometry.AffineSpace

Goal state before:
pp: n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↥(Spec R)
this : Nontrivial ↑R
⊢ IsEmpty n

Tactic:
constructor

Goal state after:
n✝ : Type u
S : Scheme
n : Type u
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↥(Spec R)
this : Nontrivial ↑R
⊢ ∀ (a : n), False
Module: Mathlib.AlgebraicGeometry.AlgClosed.Basic

Goal state before:
pp: X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ (fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) ((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p) = p

Tactic:
ext

Goal state after:
X Y : Scheme
K : Type u
inst✝² : Field K
inst✝¹ : IsAlgClosed K
f : X ⟶ Spec (CommRingCat.of K)
inst✝ : LocallyOfFiniteType f
x : ↥X
hx : IsClosed {x}
p : { p // p ≫ f = 𝟙 (Spec (CommRingCat.of K)) }
⊢ ↑((fun x ↦ ⟨pointOfClosedPoint f ↑x ⋯, ⋯⟩) ((fun p ↦ ⟨↑p (IsLocalRing.closedPoint K), ⋯⟩) p)) = ↑p
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
⊢ ⇑(single x y) = Pi.single x y

Tactic:
ext

Goal state after:
X : Type u_1
inst✝² : TopologicalSpace X
Y : Type u_2
inst✝¹ : DecidableEq X
inst✝ : Zero Y
x : X
y : Y
x✝ : X
⊢ (single x y) x✝ = Pi.single x y x✝
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support ↔ x ∈ {x | D x = 0}ᶜ ∩ U

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ D.support → x ∈ {x | D x = 0}ᶜ ∩ U

case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Zero Y
inst✝ : T1Space X
D : locallyFinsuppWithin U Y
x : X
⊢ x ∈ {x | D x = 0}ᶜ ∩ U → x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ D.support ↔ x ∈ U \ {x | (fun x ↦ D x = 0 x) x}

Tactic:
constructor

Goal state after:
case mp
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ D.support → x ∈ U \ {x | (fun x ↦ D x = 0 x) x}

case mpr
X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : T1Space X
inst✝ : Zero Y
D : locallyFinsuppWithin U Y
hU : IsClosed[inst✝²] U
x : X
⊢ x ∈ U \ {x | (fun x ↦ D x = 0 x) x} → x ∈ D.support
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ f + g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}

Tactic:
constructor

Goal state after:
case left
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ Function.support (f + g) ⊆ U

case right
X : Type u_1
inst✝¹ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝ : AddMonoid Y
f g : X → Y
hf : f ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
hg : g ∈ {f | Function.support f ⊆ U ∧ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support f).Finite}
⊢ ∀ z ∈ U, ∃ t ∈ 𝓝 z, (t ∩ Function.support (f + g)).Finite
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝¹ : Lattice Y
inst✝ : Zero Y
D₁ D₂ : locallyFinsuppWithin U Y
h₁₂ : D₁ ≤ D₂
h₂₁ : D₂ ≤ D₁
⊢ D₁ = D₂

Tactic:
ext x
    exact le_antisymm (h₁₂ x) (h₂₁ x)

Goal state after:
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ f₁ x + f₂ x ≤ max (f₁ x) 0 + max (f₂ x) 0 ∧ 0 ≤ max (f₁ x) 0 + max (f₂ x) 0

Tactic:
constructor

Goal state after:
case left
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ f₁ x + f₂ x ≤ max (f₁ x) 0 + max (f₂ x) 0

case right
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ 0 ≤ max (f₁ x) 0 + max (f₂ x) 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ -f₂ x + -f₁ x ≤ max (-f₁ x) 0 + max (-f₂ x) 0 ∧ 0 ≤ max (-f₁ x) 0 + max (-f₂ x) 0

Tactic:
constructor

Goal state after:
case left
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ -f₂ x + -f₁ x ≤ max (-f₁ x) 0 + max (-f₂ x) 0

case right
X : Type u_1
inst✝³ : TopologicalSpace X
U : Set X
Y : Type u_2
inst✝² : AddCommGroup Y
inst✝¹ : LinearOrder Y
inst✝ : IsOrderedAddMonoid Y
f₁ f₂ : locallyFinsuppWithin U Y
x : X
⊢ 0 ≤ max (-f₁ x) 0 + max (-f₂ x) 0
Module: Mathlib.Topology.LocallyFinsupp

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
⊢ restrict 0 hV = 0

Tactic:
ext

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
Y : Type u_2
inst✝ : Zero Y
U V : Set X
hV : V ⊆ U
a✝ : X
⊢ (restrict 0 hV) a✝ = 0 a✝
Module: Mathlib.Topology.LocallyFinsupp.Pushforward

Goal state before:
pp: X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
w : X → R
inst✝¹ : Semiring R
c : locallyFinsupp X R
inst✝ : PrespectralSpace X
hw : ∀ (z : X), w z = 1
⊢ map id w ⋯ c = c

Tactic:
ext

Goal state after:
X : Type u_1
R : Type u_3
inst✝² : TopologicalSpace X
w : X → R
inst✝¹ : Semiring R
c : locallyFinsupp X R
inst✝ : PrespectralSpace X
hw : ∀ (z : X), w z = 1
a✝ : X
⊢ (map id w ⋯ c) a✝ = c a✝
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↥X
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt (f y)
e : f y = f y
H : MorphismProperty.injective CommRingCat (Y.presheaf.germ (f ''ᵁ ↑V) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))

Tactic:
replace H := ((MorphismProperty.injective CommRingCat).cancel_left_of_respectsIso
    (f.appIso V).inv _).mpr H

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
V : ↑X.affineOpens
hU : IsAffineOpen (f ''ᵁ ↑V)
hU' : f ''ᵁ ↑V ≤ Scheme.Hom.opensRange f
hV : (IsOpenImmersion.affineOpensEquiv f) V = ⟨⟨f ''ᵁ ↑V, hU⟩, hU'⟩
y : ↥X
hy : y ∈ ↑↑V
H✝ : Y.IsGermInjectiveAt (f y)
e : f y = f y
H :
  MorphismProperty.injective CommRingCat
    ((Scheme.Hom.appIso f ↑V).inv ≫ Y.presheaf.germ (f ''ᵁ ↑V) (f y) ⋯ ≫ Scheme.Hom.stalkMap f y)
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.presheaf.germ (↑V) y hy))
Module: Mathlib.AlgebraicGeometry.SpreadingOut

Goal state before:
pp: case refine_1
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ IsAffineOpen (PrimeSpectrum.basicOpen f)

Tactic:
rw [← basicOpen_eq_of_affine]

Goal state after:
case refine_1
R : CommRingCat
H✝ : ∀ (I : Ideal ↑R), I.IsPrime → ∃ f ∉ I, ∀ (x y : ↑R), y * x = 0 → y ∉ I → ∃ n, f ^ n * x = 0
p : ↥(Spec R)
f : ↑R
hf : f ∉ p.asIdeal
H : ∀ (x y : ↑R), y * x = 0 → y ∉ p.asIdeal → ∃ n, f ^ n * x = 0
⊢ IsAffineOpen ((Spec R).basicOpen ((ConcreteCategory.hom (ΓSpecIso R).inv) f))