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

Goal state before:
pp: case refine_2
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)

pp: case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫ Iso.hom ?refine_2

Tactic:
·

Goal state after:
case refine_2
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ Spec ((Spec (CommRingCat.of R)).residueField p) ≅ Spec (CommRingCat.of p.asIdeal.ResidueField)
Module: Mathlib.AlgebraicGeometry.Geometrically.Basic

Goal state before:
pp: case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y

Tactic:
·

Goal state after:
case refine_2
P : ObjectProperty Scheme
X Y : Scheme
f : X ⟶ Y
H : ∀ (y : ↥Y), geometrically P (Scheme.Hom.fiberToSpecResidueField f y)
K : Type u
inst✝ : Field K
Z : Scheme
fst : Z ⟶ X
snd : Z ⟶ Spec (of K)
y : ↥Y
φ : Y.residueField y ⟶ of K
h : IsPullback fst snd f (Spec.map φ ≫ Y.fromSpecResidueField y)
p : Z ⟶ Scheme.Hom.fiber f y := pullback.lift fst (snd ≫ Spec.map φ) ⋯
⊢ snd ≫ Spec.map φ = p ≫ Scheme.Hom.fiberToSpecResidueField f y
Module: Mathlib.AlgebraicGeometry.Fiber

Goal state before:
pp: case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
      (Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).symm.op).hom

Tactic:
·

Goal state after:
case refine_3
X Y : Scheme
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : PrimeSpectrum R
⊢ (pullbackSymmetry (map (CommRingCat.ofHom (algebraMap R S))) ((Spec (CommRingCat.of R)).fromSpecResidueField p) ≪≫
          (pullback.congrHom ⋯ ⋯ ≪≫
              asIso
                (pullback.map
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv ≫
                    map (CommRingCat.ofHom (algebraMap (↑(CommRingCat.of R)) p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (CommRingCat.ofHom (algebraMap R p.asIdeal.ResidueField)))
                  (map (CommRingCat.ofHom (algebraMap R S)))
                  (map (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).inv) (𝟙 (Spec (CommRingCat.of S)))
                  (𝟙 (Spec (CommRingCat.of R))) ⋯ ⋯)) ≪≫
            pullbackSpecIso R p.asIdeal.ResidueField S).hom ≫
      map (CommRingCat.ofHom (algebraMap p.asIdeal.ResidueField (p.asIdeal.Fiber S))) =
    Scheme.Hom.fiberToSpecResidueField (map (CommRingCat.ofHom (algebraMap R S))) p ≫
      (Scheme.Spec.mapIso (Scheme.Spec.residueFieldIso (CommRingCat.of R) p).symm.op).hom
Module: Mathlib.AlgebraicGeometry.Noetherian

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

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

Tactic:
·

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, ⊤)
Module: Mathlib.AlgebraicGeometry.Noetherian

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

Tactic:
·

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

Goal state before:
pp: case mpr.convert_2
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ IsLocallyNoetherian X

pp: case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ CompactSpace ↥X

Tactic:
·

Goal state after:
case mpr.convert_2
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ IsLocallyNoetherian X
Module: Mathlib.AlgebraicGeometry.Noetherian

Goal state before:
pp: case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ CompactSpace ↥X

Tactic:
·

Goal state after:
case mpr.convert_3
X : Scheme
𝒰 : X.OpenCover
inst✝¹ : Finite 𝒰.I₀
inst✝ : ∀ (i : 𝒰.I₀), IsAffine (𝒰.X i)
hNoeth : ∀ (i : 𝒰.I₀), IsNoetherianRing ↑Γ(𝒰.X i, ⊤)
⊢ CompactSpace ↥X
Module: Mathlib.AlgebraicGeometry.Morphisms.SchemeTheoreticallyDominant

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
this : ∀ (U : Y.Opens), IsAffineOpen U → Function.Injective ⇑(ConcreteCategory.hom (app f U))
hU : ¬IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))

Tactic:
·

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsSchemeTheoreticallyDominant f
inst✝ : QuasiCompact f
U : Y.Opens
hU : IsAffineOpen U
⊢ Function.Injective ⇑(ConcreteCategory.hom (app f U))
Module: Mathlib.AlgebraicGeometry.Geometrically.Reduced

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝³ : GeometricallyReduced f
inst✝² : Flat f
inst✝¹ : IsReduced Y
inst✝ : Finite ↑(irreducibleComponents ↥Y)
pt : ↑(irreducibleComponents ↥Y) → CommRingCat := fun Z ↦ Y.presheaf.stalk ⋯.genericPoint
hpt : ∀ (Z : ↑(irreducibleComponents ↥Y)), IsField ↑(pt Z)
this✝¹ : (Z : ↑(irreducibleComponents ↥Y)) → Field ↑(pt Z) := fun Z ↦ ⋯.toField
Z : Scheme := ∐ fun Z ↦ Spec (pt Z)
g : Z ⟶ Y := Sigma.desc fun Z ↦ Y.fromSpecStalk ⋯.genericPoint
this✝ : Finite ↥Z
this : QuasiCompact g
y : ↥Y
z : ↥Z :=
  (Sigma.ι (fun Z ↦ Spec (pt Z)) ⟨irreducibleComponent y, ⋯⟩)
    (IsLocalRing.closedPoint ↑(pt ⟨irreducibleComponent y, ⋯⟩))
hz : g z ⤳ y
⊢ y ∈ closure (Set.range ⇑g)

Tactic:
exact hz.mem_closed isClosed_closure (subset_closure ⟨_, rfl⟩)

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
hY : ∃ R, Y = Spec R
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ R, Y = Spec R) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hY : ¬∃ R, Y = Spec R
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ IsIrreducible (⇑f ⁻¹' s)

pp: X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
H : ∃ x, s = {x}
⊢ IsIrreducible (⇑f ⁻¹' s)

Tactic:
·

Goal state after:
case inr
X S : Scheme
f : X ⟶ S
inst✝ : GeometricallyIrreducible f
hf : IsOpenMap ⇑f
s : Set ↥S
hs : IsIrreducible s
this : ∀ {s : Set ↥S}, IsIrreducible s → (∃ x, s = {x}) → IsIrreducible (⇑f ⁻¹' s)
H : ¬∃ x, s = {x}
⊢ IsIrreducible (⇑f ⁻¹' s)
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

pp: X✝¹ Y✝ : Scheme
f✝¹ : X✝¹ ⟶ Y✝
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
hX : ∃ S, X = Spec S
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f

Tactic:
·

Goal state after:
case inr
X✝ Y : Scheme
f✝ : X✝ ⟶ Y
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
inst✝ : LocallyOfFinitePresentation f
hf : GeneralizingMap ⇑f
this :
  ∀ {X Y : Scheme} (f : X ⟶ Y) {X : Scheme} (R : CommRingCat) (f : X ⟶ Spec R) [LocallyOfFinitePresentation f],
    GeneralizingMap ⇑f →
      (∃ S, X = Spec S) → topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
hX : ¬∃ S, X = Spec S
⊢ topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case convert_6
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.HasGoingDown ↑R ↑S

pp: case convert_7
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.FinitePresentation ↑R ↑S

Tactic:
·

Goal state after:
case convert_6
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.HasGoingDown ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case convert_7
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.FinitePresentation ↑R ↑S

Tactic:
·

Goal state after:
case convert_7
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
R S : CommRingCat
φ : R ⟶ S
inst✝ : LocallyOfFinitePresentation (Spec.map φ)
hf : GeneralizingMap ⇑(Spec.map φ)
algInst✝ : Algebra ↑R ↑S := ⋯
⊢ Algebra.FinitePresentation ↑R ↑S
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ geometrically IsIntegral = geometrically IsReduced ⊓ @GeometricallyIrreducible

Tactic:
GeometricallyIrreducible.eq_geometrically,

Goal state after:
⊢ geometrically IsIntegral = geometrically IsReduced ⊓ geometrically fun x ↦ IrreducibleSpace ↥x
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
this : ∀ {X : Scheme} (f : X ⟶ Y), (∃ S, X = Spec S) → UniversallyOpen f
hX : ¬∃ S, X = Spec S
⊢ UniversallyOpen f

pp: X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
X : Scheme
f : X ⟶ Y
hX : ∃ S, X = Spec S
⊢ UniversallyOpen f

Tactic:
·

Goal state after:
case inr
X✝ Y✝ : Scheme
f✝ : X✝ ⟶ Y✝
X Y : Scheme
f : X ⟶ Y
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
this : ∀ {X : Scheme} (f : X ⟶ Y), (∃ S, X = Spec S) → UniversallyOpen f
hX : ¬∃ S, X = Spec S
⊢ UniversallyOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y✝ : Scheme
f✝ : X ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme} [IsIntegral Y] [Subsingleton ↥Y] (f : Spec S ⟶ Y), (∃ K, Y = Spec K ∧ IsField ↑K) → UniversallyOpen f
hY : ¬∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

pp: X Y✝ : Scheme
f✝ : X ⟶ Y✝
S : CommRingCat
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
f : Spec S ⟶ Y
hY : ∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f

Tactic:
·

Goal state after:
case inr
X Y✝ : Scheme
f✝ : X ⟶ Y✝
Y : Scheme
inst✝¹ : IsIntegral Y
inst✝ : Subsingleton ↥Y
S : CommRingCat
f : Spec S ⟶ Y
this :
  ∀ {Y : Scheme} [IsIntegral Y] [Subsingleton ↥Y] (f : Spec S ⟶ Y), (∃ K, Y = Spec K ∧ IsField ↑K) → UniversallyOpen f
hY : ¬∃ K, Y = Spec K ∧ IsField ↑K
⊢ UniversallyOpen f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    (∃ R, T = Spec R) → topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
hT : ¬∃ R, T = Spec R
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))

pp: X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
hT : ∃ R, T = Spec R
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
T : Scheme
g : T ⟶ Spec K
x✝ : HasPullback g (Spec.map φ)
this :
  ∀ {T : Scheme} (g : T ⟶ Spec K) (x : HasPullback g (Spec.map φ)),
    (∃ R, T = Spec R) → topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
hT : ¬∃ R, T = Spec R
⊢ topologically (@IsOpenMap) (pullback.fst g (Spec.map φ))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: case e'_4
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
x✝ : HasPullback (Spec.map ψ) (Spec.map φ)
algInst✝¹ : Algebra ↑K ↑S := ⋯
algInst✝ : Algebra ↑K ↑R := ⋯
e_3✝ : Spec R = Spec (CommRingCat.of ↑R)
⊢ (pullbackSpecIso ↑K ↑R ↑S).inv ≫ pullback.fst (Spec.map ψ) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (algebraMap (↑R) (TensorProduct ↑K ↑R ↑S)))

pp: case convert_2
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
x✝ : HasPullback (Spec.map ψ) (Spec.map φ)
algInst✝¹ : Algebra ↑K ↑S := (CommRingCat.Hom.hom φ).toAlgebra
algInst✝ : Algebra ↑K ↑R := (CommRingCat.Hom.hom ψ).toAlgebra
⊢ topologically (@IsOpenMap) (Spec.map (CommRingCat.ofHom (algebraMap (↑R) (TensorProduct ↑K ↑R ↑S))))

Tactic:
·

Goal state after:
case e'_4
X Y : Scheme
f : X ⟶ Y
S K : CommRingCat
hK : IsField ↑K
inst✝¹ : IsIntegral (Spec K)
inst✝ : Subsingleton ↥(Spec K)
φ : K ⟶ S
R : CommRingCat
ψ : K ⟶ R
x✝ : HasPullback (Spec.map ψ) (Spec.map φ)
algInst✝¹ : Algebra ↑K ↑S := ⋯
algInst✝ : Algebra ↑K ↑R := ⋯
e_3✝ : Spec R = Spec (CommRingCat.of ↑R)
⊢ (pullbackSpecIso ↑K ↑R ↑S).inv ≫ pullback.fst (Spec.map ψ) (Spec.map φ) =
    Spec.map (CommRingCat.ofHom (algebraMap (↑R) (TensorProduct ↑K ↑R ↑S)))
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: case neg
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : ¬1 ≤ p.natDegree
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

pp: case pos
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : 1 ≤ p.natDegree
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
·

Goal state after:
case neg
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : ¬1 ≤ p.natDegree
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)
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
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x ↦ t ^ x) n, ⋯⟩ * r) p = 0
hp' : ¬1 ≤ p.natDegree
⊢ p.natDegree = 0

Tactic:
by lia

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

Goal state before:
pp: case inr
Z S X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

pp: Z S X Y : Scheme
f : X ⟶ Y
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
·

Goal state after:
case inr
Z S X Y : Scheme
f : X ⟶ Y
this : ∀ ⦃X Y : Scheme⦄ (f : X ⟶ Y), (∃ R, Y = Spec R) → IsIntegralHom f → topologically (@IsClosedMap) f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

pp: Z S : Scheme
R : CommRingCat
X : Scheme
f : X ⟶ Spec R
hX : ∃ S, X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f

Tactic:
·

Goal state after:
case inr
Z S X : Scheme
R : CommRingCat
f : X ⟶ Spec R
this : ∀ ⦃X : Scheme⦄ (f : X ⟶ Spec R), (∃ S, X = Spec S) → IsIntegralHom f → topologically (@IsClosedMap) f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f → topologically (@IsClosedMap) f
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f

pp: X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hY : ∃ R, Y = Spec R
⊢ IsIntegralHom f

Tactic:
·

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ IsIntegralHom f
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f

pp: X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
hX : ∃ S, X = Spec S
⊢ IsIntegralHom f

Tactic:
·

Goal state after:
case inr
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
this :
  ∀ {X : Scheme} (R : CommRingCat) {f : X ⟶ Spec R},
    UniversallyClosed f → IsAffineHom f → (∃ S, X = Spec S) → IsIntegralHom f
hX : ¬∃ S, X = Spec S
⊢ IsIntegralHom f