Module: Mathlib.FieldTheory.Minpoly.IsIntegrallyClosed

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ IsIntegral K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

pp: case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

pp: case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

pp: case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)

Tactic:
· refine isIntegral_algebraMap.mul (hs.map (IsScalarTower.toAlgHom R S L)).tower_top

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)).Monic

case refine_3
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (Polynomial.aeval ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s))
      ((minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r)) =
    0

case refine_4
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDomain S
inst✝ : IsTorsionFree R S
r : R
hr : r ≠ 0
s : S
hs : IsIntegral R s
K : Type u_1 := FractionRing R
L : Type u_2 := FractionRing S
this : Algebra K L := FractionRing.liftAlgebra R L
⊢ (minpoly K ((algebraMap S L) s)).scaleRoots ((algebraMap R K) r) ∣
    minpoly K ((algebraMap K L) ((algebraMap R K) r) * (algebraMap S L) s)