-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma isIntegral_of_isClosedMap_comap_mapRingHom (h : IsClosedMap (comap (mapRingHom f))) :
    f.IsIntegral

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = ⇑(comap (mapRingHom f)) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
this : 1 ∈ q.asIdeal
⊢ False

Tactic:
exact q.2.ne_top (q.asIdeal.eq_top_iff_one.mpr this)

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = ⇑(comap (mapRingHom f)) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
⊢ False

Tactic:
have : 1 ∈ q.asIdeal := by simpa [p] using (sub_mem (q.asIdeal.mul_mem_left (C r) hXq) hpq)

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = ⇑(comap (mapRingHom f)) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
this : 1 ∈ q.asIdeal
⊢ False

Proof state:
case isIntegral
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
⊢ IsIntegral R r

Tactic:
let p : S[X] := C r * X - 1

Result:
case isIntegral
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
⊢ IsIntegral R r

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = ⇑(comap (mapRingHom f)) '' zeroLocus ↑(Ideal.span {p})
⊢ ∀ (a : PrimeSpectrum S[X]), p ∈ a.asIdeal → X ∉ a.asIdeal

Tactic:
intro q hpq hXq

Result:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
H : zeroLocus ↑(Ideal.comap (mapRingHom f) (Ideal.span {p})) = ⇑(comap (mapRingHom f)) '' zeroLocus ↑(Ideal.span {p})
q : PrimeSpectrum S[X]
hpq : p ∈ q.asIdeal
hXq : X ∈ q.asIdeal
⊢ False

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
this : p.natDegree ≤ 1
⊢ (X ^ 0).natDegree ≤ 1 + c.natDegree

Tactic:
simp

Result:
no goals

Proof state:
case isIntegral.intro.intro.intro.intro.refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h✝ : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
⊢ b.reverse.Monic

Tactic:
have : b.natTrailingDegree = 0 := by simp [h]

Result:
case isIntegral.intro.intro.intro.intro.refine_1
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
h✝ : IsClosedMap ⇑(comap (mapRingHom f))
algInst✝ : Algebra R S := f.toAlgebra
a✝¹ : Nontrivial R
a✝ : Nontrivial S
r : S
p : S[X] := C r * X - 1
this✝ : 1 ∈ Ideal.span {X} ⊔ Ideal.comap (mapRingHom f) (Ideal.span {p})
a b : R[X]
hb : b ∈ Ideal.comap (mapRingHom f) (Ideal.span {p})
e : a * X + b = 1
c : S[X]
hc : map (algebraMap R S) b = p * c
h : b.coeff 0 = 1
this : b.natTrailingDegree = 0
⊢ b.reverse.Monic