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

Goal state before:
pp: X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace ↥(pullback f (pullback.fst g x))

Tactic:
]

Goal state after:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝³ : GeometricallyIrreducible f
inst✝² : GeometricallyIrreducible g
inst✝¹ : UniversallyOpen f
inst✝ : UniversallyOpen g
K : Type u_1
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Z
⊢ IrreducibleSpace ↥(pullback f (pullback.fst g x))
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s)

Tactic:
]

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
⊢ ∀ (s : ↥S), GeometricallyIrreducible (Scheme.Hom.fiberToSpecResidueField (f ≫ g) 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
⊢ ∀ (i : X.affineCover.I₀),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ 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
⊢ ∀ (i : X.affineCover.I₀),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ IsOpenMap) (X.affineCover.f i ≫ f)
Module: Mathlib.AlgebraicGeometry.Geometrically.Irreducible

Goal state before:
pp: X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ (⇑(f ≫ g) ⁻¹' {s}).Nonempty

Tactic:
]

Goal state after:
X Y : Scheme
Z : Scheme
S : Scheme
f✝ : X ⟶ S
g✝ : Y ⟶ S
U : Scheme
f : U ⟶ X
g : X ⟶ S
inst✝² : IsOpenImmersion f
inst✝¹ : GeometricallyIrreducible g
inst✝ : Surjective (f ≫ g)
s : ↥S
K : Type u
x✝ : Field K
x : Spec (CommRingCat.of K) ⟶ Spec (S.residueField s)
i : pullback (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x ⟶ pullback (Scheme.Hom.fiberToSpecResidueField g s) x :=
  pullback.map (Scheme.Hom.fiberToSpecResidueField (f ≫ g) s) x (Scheme.Hom.fiberToSpecResidueField g s) x
    (pullback.map (f ≫ g) (S.fromSpecResidueField s) g (S.fromSpecResidueField s) f (𝟙 (Spec (S.residueField s))) (𝟙 S)
      ⋯ ⋯)
    (𝟙 (Spec (CommRingCat.of K))) (𝟙 (Spec (S.residueField s))) ⋯ ⋯
⊢ (⇑(f ≫ g) ⁻¹' {s}).Nonempty
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 := (CommRingCat.Hom.hom φ).toAlgebra
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap ↑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 := (CommRingCat.Hom.hom φ).toAlgebra
⊢ GeneralizingMap (PrimeSpectrum.comap (algebraMap ↑R ↑S))
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: ⊢ geometrically IsIntegral = geometrically (IsReduced ⊓ fun x ↦ IrreducibleSpace ↥x)

Tactic:
]

Goal state after:
⊢ geometrically IsIntegral = geometrically (IsReduced ⊓ fun x ↦ IrreducibleSpace ↥x)
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IrreducibleSpace ↥X ∧ IsReduced X

Tactic:
]

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝⁴ : GeometricallyIntegral f
inst✝³ : Flat f
inst✝² : UniversallyOpen f
inst✝¹ : IsIntegral S
inst✝ : IsLocallyNoetherian S
⊢ IrreducibleSpace ↥X ∧ IsReduced X
Module: Mathlib.AlgebraicGeometry.Geometrically.Integral

Goal state before:
pp: X S : Scheme
f : X ⟶ S
inst✝² : GeometricallyIntegral f
inst✝¹ : Subsingleton ↥S
inst✝ : IsIntegral S
⊢ IrreducibleSpace ↥X ∧ IsReduced X

Tactic:
]

Goal state after:
X S : Scheme
f : X ⟶ S
inst✝² : GeometricallyIntegral f
inst✝¹ : Subsingleton ↥S
inst✝ : IsIntegral S
⊢ IrreducibleSpace ↥X ∧ IsReduced X
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : Flat f
this :
  HasRingHomProperty (topologically fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
    fun {R S} [CommRing R] [CommRing S] f ↦
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom f))
⊢ ∀ (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ f ⁻¹ᵁ ↑U),
    topologically (fun {α β} [TopologicalSpace α] [TopologicalSpace β] ↦ GeneralizingMap)
      (Spec.map (CommRingCat.ofHom (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e))))
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally f ↔ (topologically @IsClosedMap).universally f

Tactic:
]

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

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ (topologically @IsClosedMap).universally f

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsClosedImmersion f
⊢ (topologically @IsClosedMap).universally f
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally.IsStableUnderComposition

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ (topologically @IsClosedMap).universally.IsStableUnderComposition
Module: Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

Goal state before:
pp: X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget (topologically @IsClosedMap).universally

Tactic:
]

Goal state after:
X Y : Scheme
f : X ⟶ Y
⊢ IsZariskiLocalAtTarget (topologically @IsClosedMap).universally
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: ⊢ StableUnderComposition fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral

Tactic:
by
  introv R hf hg; exact hf.trans _ _ hg

Goal state after:
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem (e (e.symm x))

Tactic:
]

Goal state after:
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
e : R ≃+* S
x : S
⊢ e.toRingHom.IsIntegralElem (e (e.symm x))
Module: Mathlib.RingTheory.RingHom.Integral

Goal state before:
pp: R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
int : Algebra.IsIntegral R T
⊢ Algebra.IsIntegral S (S ⊗[R] T)

Tactic:
]

Goal state after:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
int : Algebra.IsIntegral R T
⊢ Algebra.IsIntegral S (S ⊗[R] T)
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' : ∃ 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)

Tactic:
]

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.RingTheory.RingHom.Integral

Goal state before:
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 : ℕ
hp' : 1 ≤ p.natDegree
e : t ^ m • eval₂ (algebraMap R S) (t ^ n • r) p = 0
this :
  eval₂ (algebraMap R S) (t ^ m • t ^ n • r) (p.scaleRoots (t ^ m)) =
    (t ^ m) ^ p.natDegree • eval₂ (algebraMap R S) (t ^ n • r) p
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: X Y Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral

Tactic:
]

Goal state after:
X Y Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsIntegralHom f ↔
      IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔ (CommRingCat.Hom.hom φ).IsIntegral

pp: R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S)

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map φ) ⊤)).IsIntegral ↔ (CommRingCat.Hom.hom φ).IsIntegral

R S : CommRingCat
φ : R ⟶ S
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f ↦ f.IsIntegral).RespectsIso
⊢ IsAffine (Spec S)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f

Tactic:
]

Goal state after:
Z S : Scheme
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y) [universally (@IsIntegralHom) f], (topologically @IsClosedMap).universally f
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
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)

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
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)
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

Tactic:
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover,
      IsZariskiLocalAtTarget.iff_of_openCover (P := topologically _) Y.affineCover]

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
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) →
    ∀ (i : Y.affineCover.toPreZeroHypercover.1),
      topologically (@IsClosedMap) (Scheme.Cover.pullbackHom Y.affineCover f i)
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
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ 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
H : IsIntegralHom f
inst : IsAffine X
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ 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
inst : IsAffine X
H : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ 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
inst : IsAffine X
H : IsIntegralHom (X.isoSpec.inv ≫ f)
⊢ topologically (@IsClosedMap) (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: Z S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)

Tactic:
]

Goal state after:
Z S✝ : Scheme
R S : CommRingCat
φ : R ⟶ S
⊢ (CommRingCat.Hom.hom φ).IsIntegral → topologically (@IsClosedMap) (Spec.map φ)
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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.toPreZeroHypercover.1), UniversallyClosed (Scheme.Cover.pullbackHom Y.affineCover f i)
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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.toPreZeroHypercover.1), UniversallyClosed (Scheme.Cover.pullbackHom Y.affineCover f i)
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
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

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

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.toPreZeroHypercover.1), UniversallyClosed (Scheme.Cover.pullbackHom Y.affineCover f i)
H₂ : ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsAffineHom (Scheme.Cover.pullbackHom Y.affineCover f i)
this : ∀ {X Y : Scheme} {f : X ⟶ Y}, UniversallyClosed f → IsAffineHom f → (∃ R, Y = Spec R) → IsIntegralHom f
hY : ¬∃ R, Y = Spec R
⊢ ∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)
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
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ 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
inst : IsAffine X
⊢ IsIntegralHom (X.isoSpec.inv ≫ f)
Module: Mathlib.AlgebraicGeometry.Morphisms.Integral

Goal state before:
pp: R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral

Tactic:
]

Goal state after:
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: ⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite

Tactic:
]

Goal state after:
⊢ ∀ {X Y : Scheme} (f : X ⟶ Y),
    IsFinite f ↔ IsAffineHom f ∧ ∀ (U : Y.Opens), IsAffineOpen U → (CommRingCat.Hom.hom (Scheme.Hom.app f U)).Finite
Module: Mathlib.AlgebraicGeometry.Morphisms.Finite

Goal state before:
pp: R S : CommRingCat
f : R ⟶ S
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite ↔
    (CommRingCat.Hom.hom (Scheme.Hom.appTop (Spec.map f))).Finite

Tactic:
]

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

Goal state before:
pp: case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
]

Goal state after:
case inr
X Y : Scheme
f : X ⟶ Y
this : ∀ {X Y : Scheme} (f : X ⟶ Y), IsAffine Y → (IsFinite f ↔ IsIntegralHom f ∧ LocallyOfFiniteType f)
hY : ¬IsAffine Y
⊢ (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsFinite (Scheme.Cover.pullbackHom Y.affineCover f i)) ↔
    (∀ (i : Y.affineCover.toPreZeroHypercover.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)) ∧
      ∀ (i : Y.affineCover.toPreZeroHypercover.1), LocallyOfFiniteType (Scheme.Cover.pullbackHom Y.affineCover f i)