case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
hz : IsAlgebraic R z
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
rcases hz with ⟨p, p_ne_zero, px⟩
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
set a := p.leadingCoeff
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
have a_ne_zero : a ≠ 0 := mt Polynomial.leadingCoeff_eq_zero.mp p_ne_zero
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
x_integral : IsIntegral R (z * ↑(algebraMap R S) a)
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
have x_integral : IsIntegral R (z * algebraMap R S a) :=
  ⟨p.integralNormalization, monic_integralNormalization p_ne_zero,
    integralNormalization_aeval_eq_zero px inj⟩
no goals
case intro.intro
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : CommRing S
inst✝ : Algebra R S
z : S
inj : ∀ (x : R), ↑(algebraMap R S) x = 0 → x = 0
p : R[X]
p_ne_zero : p ≠ 0
px : ↑(aeval z) p = 0
a : R := leadingCoeff p
a_ne_zero : a ≠ 0
x_integral : IsIntegral R (z * ↑(algebraMap R S) a)
⊢ ∃ x y x_1, z * ↑(algebraMap R S) y = ↑x
exact ⟨⟨_, x_integral⟩, a, a_ne_zero, rfl⟩