-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem IsIntegral.of_mul_unit {x y : B} {r : R} (hr : algebraMap R B r * y = 1)
    (hx : IsIntegral R (x * y)) : IsIntegral R x

Proof state:
case intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ IsIntegral R x

Tactic:
refine ⟨scaleRoots p r, (monic_scaleRoots_iff r).2 p_monic, ?_⟩

Result:
case intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x (p.scaleRoots r) = 0

Proof state:
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
hx : IsIntegral R (x * y)
⊢ IsIntegral R x

Tactic:
obtain ⟨p, p_monic, hp⟩ := hx

Result:
case intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ IsIntegral R x

Proof state:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval x)

Tactic:
rfl

Result:
no goals

Proof state:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))

Tactic:
rw [mul_assoc, hr, mul_one]

Result:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval x)

Proof state:
case intro.intro
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x (p.scaleRoots r) = 0

Tactic:
convert scaleRoots_aeval_eq_zero hp

Result:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval ((algebraMap R B) r * (x * y)))

Proof state:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : (algebraMap R B) r * y = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval ((algebraMap R B) r * (x * y)))

Tactic:
rw [Algebra.commutes] at hr ⊢

Result:
case h.e'_2.h.e
R : Type u_1
B : Type u_3
inst✝² : CommRing R
inst✝¹ : Ring B
inst✝ : Algebra R B
x y : B
r : R
hr : y * (algebraMap R B) r = 1
p : R[X]
p_monic : p.Monic
hp : eval₂ (algebraMap R B) (x * y) p = 0
⊢ eval₂ (algebraMap R B) x = ⇑(aeval (x * y * (algebraMap R B) r))