-- 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
this : p = 0
⊢ False

Tactic:
simp [this] at hp

Result:
no goals

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

Tactic:
refine .inr ?_

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

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
⊢ IsEmpty n

Tactic:
have : Nontrivial R := (subsingleton_or_nontrivial R).resolve_left fun H ↦
    not_isEmpty_of_nonempty (Spec R) (inferInstanceAs (IsEmpty (PrimeSpectrum R)))

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
this : Nontrivial ↑R
⊢ 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
this : ((rename fun x => i).comp ↑(pUnitAlgEquiv ↑R).symm) p = 0
⊢ False

Tactic:
rw [AlgHom.comp_apply, map_eq_zero_iff _ (rename_injective _ (fun _ _ _ ↦ rfl))] at this

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 : ↑(pUnitAlgEquiv ↑R).symm p = 0
⊢ False

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

Tactic:
exact .inl ‹_›

Result:
no goals

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
this : (RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] f => f.IsIntegral).RespectsIso
⊢ False

Tactic:
rw [← MorphismProperty.cancel_left_of_respectsIso @IsIntegralHom (SpecIso n R).inv,
  SpecIso_inv_over, HasAffineProperty.iff_of_isAffine (P := @IsIntegralHom)] at h

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

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

Tactic:
obtain ⟨y, hy⟩ := S.affineCover.covers x

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

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

Tactic:
rintro (_ | _) <;> infer_instance

Result:
no goals

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

Tactic:
constructor

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

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

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

Tactic:
cases isEmpty_or_nonempty S

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

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

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
⊢ n → False

Tactic:
intro i

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
⊢ False

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
this : ↑(pUnitAlgEquiv ↑R).symm p = 0
⊢ False

Tactic:
simp only [AlgEquiv.toAlgHom_eq_coe, AlgHom.coe_coe, EmbeddingLike.map_eq_zero_iff] at this

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 : p = 0
⊢ False

Proof state:
case mp.inr
n : Type v
S : Scheme
h : IsIntegralHom (𝔸(n; S) ↘ S)
h✝ : Nonempty ↑↑S.toPresheafedSpace
⊢ IsEmpty n

Tactic:
wlog hS : ∃ R, S = Spec R

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

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