-- Mathlib/AlgebraicGeometry/AffineSpace.lean
lemma isIntegralHom_over_iff_isEmpty : IsIntegralHom (𝔸(n; S) ↘ S) ↔ IsEmpty S ∨ IsEmpty n

Proof state:
case intro.false.intro.intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ False

Tactic:
have : (rename fun _ ↦ i).comp (pUnitAlgEquiv.{_, v} _).symm.toAlgHom p = 0 := by
  simp [← hp', ← algebraMap_eq]

Result:
case intro.false.intro.intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝¹ : Nontrivial ↑R
i : n
this✝ : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
this : ((rename fun x => i).comp ↑(pUnitAlgEquiv ↑R).symm) p = 0
⊢ False

Proof state:
case intro.false
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this : Nontrivial ↑R
i : n
⊢ False

Tactic:
have := RingHom.toMorphismProperty_respectsIso_iff.mp RingHom.isIntegral_respectsIso.{max u v}

Result:
case intro.false
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ False

Proof state:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this : Nontrivial ↑R
⊢ IsEmpty n

Tactic:
constructor

Result:
case intro.false
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this : Nontrivial ↑R
⊢ n → False

Proof state:
case mp.inr.inr.intro.intro
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↑↑S.toPresheafedSpace
this :
  ∀ {n : Type v} (S : Scheme),
    IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↑↑S.toPresheafedSpace → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
x : ↑↑S.toPresheafedSpace
y : ↑↑(S.affineCover.obj (S.affineCover.f x)).toPresheafedSpace
hy : (ConcreteCategory.hom (S.affineCover.map (S.affineCover.f x)).base) y = x
⊢ IsEmpty n

Tactic:
exact this (S.affineCover.obj x) (MorphismProperty.IsStableUnderBaseChange.of_isPullback
  (isPullback_map (S.affineCover.map x)) h) ⟨y⟩ ⟨_, rfl⟩

Result:
no goals

Proof state:
case mp
n : Type v
S : Scheme
⊢ IsIntegralHom (𝔸(n; S) ↘ S) → IsEmpty ↑↑S.toPresheafedSpace ∨ IsEmpty n

Tactic:
intro h

Result:
case mp
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
⊢ IsEmpty ↑↑S.toPresheafedSpace ∨ IsEmpty n

Proof state:
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ ((rename fun x => i).comp ↑(pUnitAlgEquiv ↑R).symm) p = 0

Tactic:
simp [← hp', ← algebraMap_eq]

Result:
no goals

Proof state:
n✝ : Type v
S✝ : Scheme
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↑↑S.toPresheafedSpace
hS : ∃ R, S = Spec R
⊢ IsEmpty n

Tactic:
obtain ⟨R, rfl⟩ := hS

Result:
case intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h : IsIntegralHom (𝔸(n; Spec R) ↘ Spec R)
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
⊢ IsEmpty n

Proof state:
case intro.false
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ False

Tactic:
obtain ⟨p : Polynomial R, hp, hp'⟩ :=
  (MorphismProperty.arrow_mk_iso_iff (RingHom.toMorphismProperty RingHom.IsIntegral)
    (arrowIsoΓSpecOfIsAffine _)).mpr h.2 (X i)

Result:
case intro.false.intro.intro
n✝ : Type v
S : Scheme
n : Type v
R : CommRingCat
h :
  IsAffine (Spec (CommRingCat.of (MvPolynomial n ↑R))) ∧
    (CommRingCat.Hom.hom (Scheme.Hom.app (Spec.map (CommRingCat.ofHom C)) ⊤)).IsIntegral
h✝ : Nonempty ↑↑(Spec R).toPresheafedSpace
this✝ : Nontrivial ↑R
i : n
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
p : Polynomial ↑R
hp : p.Monic
hp' : Polynomial.eval₂ (CommRingCat.Hom.hom (CommRingCat.ofHom C)) (X i) p = 0
⊢ False

Proof state:
case mp.inr.inr
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↑↑S.toPresheafedSpace
this :
  ∀ {n : Type v} (S : Scheme),
    IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↑↑S.toPresheafedSpace → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
⊢ IsEmpty n

Tactic:
obtain ⟨x⟩ := ‹Nonempty S›

Result:
case mp.inr.inr.intro
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↑↑S.toPresheafedSpace
this :
  ∀ {n : Type v} (S : Scheme),
    IsIntegralHom (𝔸(n; S) ↘ S) → Nonempty ↑↑S.toPresheafedSpace → (∃ R, S = Spec R) → IsEmpty n
hS : ¬∃ R, S = Spec R
x : ↑↑S.toPresheafedSpace
⊢ IsEmpty n