-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
theorem isIntegral_appTop_of_universallyClosed (f : X ⟶ Y) [UniversallyClosed f] [IsAffine Y] :
    f.appTop.hom.IsIntegral

Proof state:
case surj.hfinj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, ⊤)).hom)

Tactic:
exact (ConcreteCategory.bijective_of_isIso (Scheme.ΓSpecIso Γ(X, ⊤)).hom).1

Result:
no goals

Proof state:
case surj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Surjective ⇑(ConcreteCategory.hom X.toSpecΓ.base)

Tactic:
apply surjective_of_isClosed_range_of_injective

Result:
case surj.hfcl
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ IsClosed (Set.range ⇑(ConcreteCategory.hom X.toSpecΓ.base))

case surj.hfinj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop X.toSpecΓ))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝² : CompactSpace ↑↑X.toPresheafedSpace
this✝¹ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this✝ : UniversallyClosed X.toSpecΓ
this : Surjective X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))

Tactic:
exact ⟨.of_comp_surjective X.toSpecΓ _, inferInstance⟩

Result:
no goals

Proof state:
case surj.hfcl
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ IsClosed (Set.range ⇑(ConcreteCategory.hom X.toSpecΓ.base))

Tactic:
exact X.toSpecΓ.isClosedMap.isClosed_range

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
have : CompactSpace X := (quasiCompact_over_affine_iff f).mp inferInstance

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
have : UniversallyClosed (X.toSpecΓ ≫ Spec.map f.appTop) := by
  rwa [← Scheme.toSpecΓ_naturality,
    MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝ : CompactSpace ↑↑X.toPresheafedSpace
this : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝² : CompactSpace ↑↑X.toPresheafedSpace
this✝¹ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this✝ : UniversallyClosed X.toSpecΓ
this : Surjective X.toSpecΓ
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
rw [← IsIntegralHom.SpecMap_iff, IsIntegralHom.iff_universallyClosed_and_isAffineHom]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝² : CompactSpace ↑↑X.toPresheafedSpace
this✝¹ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this✝ : UniversallyClosed X.toSpecΓ
this : Surjective X.toSpecΓ
⊢ UniversallyClosed (Spec.map (Scheme.Hom.appTop f)) ∧ IsAffineHom (Spec.map (Scheme.Hom.appTop f))

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Surjective X.toSpecΓ

Tactic:
constructor

Result:
case surj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Surjective ⇑(ConcreteCategory.hom X.toSpecΓ.base)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝ : CompactSpace ↑↑X.toPresheafedSpace
this : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Tactic:
have : UniversallyClosed X.toSpecΓ := .of_comp_of_isSeparated _ (Spec.map f.appTop)

Result:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ (CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

Proof state:
case surj.hfinj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.Hom.appTop X.toSpecΓ))

Tactic:
simp only [Scheme.toSpecΓ_appTop]

Result:
case surj.hfinj
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this✝¹ : CompactSpace ↑↑X.toPresheafedSpace
this✝ : UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))
this : UniversallyClosed X.toSpecΓ
⊢ Function.Injective ⇑(ConcreteCategory.hom (Scheme.ΓSpecIso Γ(X, ⊤)).hom)

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝¹ : UniversallyClosed f
inst✝ : IsAffine Y
this : CompactSpace ↑↑X.toPresheafedSpace
⊢ UniversallyClosed (X.toSpecΓ ≫ Spec.map (Scheme.Hom.appTop f))

Tactic:
rwa [← Scheme.toSpecΓ_naturality,
  MorphismProperty.cancel_right_of_respectsIso (P := @UniversallyClosed)]

Result:
no goals