-- Mathlib/AlgebraicGeometry/Morphisms/Integral.lean
lemma iff_universallyClosed_and_isAffineHom {X Y : Scheme.{u}} {f : X ⟶ Y} :
    IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ IsIntegralHom f ↔ UniversallyClosed f ∧ IsAffineHom f

Tactic:
refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨H₁, H₂⟩ ↦ ?_⟩

Result:
X Y : Scheme
f : X ⟶ Y
x✝ : UniversallyClosed f ∧ IsAffineHom f
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Proof state:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
algebraize [φ.1, Polynomial.mapRingHom φ.1]

Result:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst✝¹ : Algebra ↑R ↑S := φ.hom'.toAlgebra
algInst✝ : Algebra (Polynomial ↑R) (Polynomial ↑S) := (Polynomial.mapRingHom φ.hom').toAlgebra
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

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

Tactic:
exact fun _ ↦ this inferInstance inferInstance ⟨_, rfl⟩

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
x✝ : UniversallyClosed f ∧ IsAffineHom f
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Tactic:
clear * -

Result:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

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

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := @IsAffineHom) Y.affineCover] at H₂

Result:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.1), UniversallyClosed (Scheme.Cover.pullbackHom Y.affineCover f i)
H₂ : ∀ (i : Y.affineCover.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.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

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

Tactic:
obtain ⟨R, rfl⟩ := hY

Result:
case intro
X : Scheme
R : CommRingCat
f : X ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Proof state:
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.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := @UniversallyClosed) Y.affineCover] at H₁

Result:
case inr
X Y : Scheme
f : X ⟶ Y
H₁ : ∀ (i : Y.affineCover.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.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

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

Tactic:
obtain ⟨S, rfl⟩ := hX

Result:
case intro
R S : CommRingCat
f : Spec S ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Proof state:
case intro
R S : CommRingCat
f : Spec S ⟶ Spec R
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Tactic:
obtain ⟨φ, rfl⟩ : ∃ φ, Spec.map φ = f := ⟨_, Spec.map_preimage _⟩

Result:
case intro.intro
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsIntegralHom (Spec.map φ)

Proof state:
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

Tactic:
rw [IsLocalAtTarget.iff_of_openCover (P := @IsIntegralHom) Y.affineCover]

Result:
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.1), IsIntegralHom (Scheme.Cover.pullbackHom Y.affineCover f i)

Proof state:
case intro.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 f

Tactic:
rw [← cancel_left_of_respectsIso (P := @IsIntegralHom) X.isoSpec.inv]

Result:
case intro.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)

Proof state:
case intro.intro.h
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
algInst✝¹ : Algebra ↑R ↑S := φ.hom'.toAlgebra
algInst✝ : Algebra (Polynomial ↑R) (Polynomial ↑S) := (Polynomial.mapRingHom φ.hom').toAlgebra
this : IsScalarTower (↑R) (Polynomial ↑R) (Polynomial ↑S)
⊢ IsClosedMap ⇑(PrimeSpectrum.comap (Polynomial.mapRingHom (CommRingCat.Hom.hom φ)))

Tactic:
refine H₁.out (Spec.map (CommRingCat.ofHom Polynomial.C))
  (Spec.map (CommRingCat.ofHom Polynomial.C)) (Spec.map _)
  (isPullback_Spec_map_isPushout _ _ _ _
  (CommRingCat.isPushout_of_isPushout R S (Polynomial R) (Polynomial S))).flip

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H₁ : UniversallyClosed f
H₂ : IsAffineHom f
⊢ IsIntegralHom f

Tactic:
wlog hY : ∃ R, Y = Spec R

Result:
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

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

Proof state:
case intro.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

Tactic:
have inst : IsAffine X := isAffine_of_isAffineHom f

Result:
case intro.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 f

Proof state:
case intro.intro
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ IsIntegralHom (Spec.map φ)

Tactic:
rw [SpecMap_iff]

Result:
case intro.intro
R S : CommRingCat
φ : R ⟶ S
H₁ : UniversallyClosed (Spec.map φ)
H₂ : IsAffineHom (Spec.map φ)
⊢ (CommRingCat.Hom.hom φ).IsIntegral