-- Mathlib/RingTheory/RingHom/Integral.lean
theorem isIntegral_ofLocalizationSpan :
    OfLocalizationSpan (RingHom.IsIntegral ·)

Proof state:
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x => t ^ x) n, ⋯⟩ * r) p = 0
hp' : 1 ≤ p.natDegree
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩

Result:
case pos
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x => t ^ x) n, ⋯⟩ * r) p = 0
hp' : 1 ≤ p.natDegree
⊢ eval₂ (algebraMap R S) (↑⟨t, ht⟩ ^ (m + n) • r) (p.scaleRoots (t ^ m)) = 0

Proof state:
case neg
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n : ℕ
p : R[X]
hp : p.Monic
m : ℕ
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x => t ^ x) n, ⋯⟩ * r) p = 0
hp' : ¬1 ≤ p.natDegree
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by omega)

Result:
case neg
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝² : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝¹ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this✝ : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
this : _root_.IsIntegral (Localization.Away t) ((algebraMap S (Localization.Away (f t))) r)
n m : ℕ
hp : Monic 1
e : ↑⟨(algebraMap R S) t ^ m, ⋯⟩ * eval₂ (algebraMap R S) ((algebraMap R S) ↑⟨(fun x => t ^ x) n, ⋯⟩ * r) 1 = 0
hp' : ¬1 ≤ natDegree 1
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Proof state:
case H.mk
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
haveI : IsScalarTower R (Localization.Away t) (Localization.Away (f t)) := .of_algebraMap_eq'
  (IsLocalization.lift_comp _).symm

Result:
case H.mk
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝¹ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this✝ : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
this : IsScalarTower R (Localization.Away t) (Localization.Away (f t))
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Proof state:
case H.mk
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)

Tactic:
letI := (Localization.awayMap f t).toAlgebra

Result:
case H.mk
R S : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
s : Set R
hs : Ideal.span s = ⊤
H : ∀ (r : ↑s), (fun {R S} [CommRing R] [CommRing S] x => x.IsIntegral) (Localization.awayMap f ↑r)
r : S
this✝ : Algebra R S := f.toAlgebra
t : R
ht : t ∈ s
this : Algebra (Localization.Away t) (Localization.Away (f t)) := (Localization.awayMap f t).toAlgebra
⊢ ∃ n, ↑⟨t, ht⟩ ^ n • r ∈ Subalgebra.toSubmodule (integralClosure R S)