case refine'_1
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R ↑x
⊢ IsIntegral R x

case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R x
⊢ IsIntegral R ↑x
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
⊢ IsIntegral R ↑x ↔ IsIntegral R x
refine' ⟨fun h => _, fun h => _⟩
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ IsIntegral R x
case refine'_1
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R ↑x
⊢ IsIntegral R x
obtain ⟨P, hPmo, hProot⟩ := h
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ IsIntegral R x
refine' ⟨P, hPmo, (injective_iff_map_eq_zero _).1 (algebraMap (↥S) L).injective _ _⟩
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
letI : IsScalarTower R S L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ eval₂ (algebraMap R L) (↑(algebraMap { x // x ∈ S } L) x) P = 0
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ ↑(algebraMap { x // x ∈ S } L) (eval₂ (algebraMap R { x // x ∈ S }) x P) = 0
rw [eval₂_eq_eval_map, ← eval₂_at_apply, eval₂_eq_eval_map, Polynomial.map_map, ←
  IsScalarTower.algebraMap_eq, ← eval₂_eq_eval_map, ← eval₂_eq_eval_map]
no goals
case refine'_1.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R L) (↑x) P = 0
this : IsScalarTower R { x // x ∈ S } L := IsScalarTower.of_algebraMap_eq (congr_fun rfl)
⊢ eval₂ (algebraMap R L) (↑(algebraMap { x // x ∈ S } L) x) P = 0
exact hProot
case refine'_2.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ IsIntegral R ↑x
case refine'_2
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
h : IsIntegral R x
⊢ IsIntegral R ↑x
obtain ⟨P, hPmo, hProot⟩ := h
case refine'_2.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ eval₂ (algebraMap R L) (↑x) P = 0
case refine'_2.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ IsIntegral R ↑x
refine' ⟨P, hPmo, _⟩
no goals
case refine'_2.intro.intro
K : Type u_2
L : Type u_3
L' : Type ?u.191604
inst✝⁸ : Field K
inst✝⁷ : Field L
inst✝⁶ : Field L'
inst✝⁵ : Algebra K L
inst✝⁴ : Algebra K L'
S : IntermediateField K L
R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R K
inst✝¹ : Algebra R L
inst✝ : IsScalarTower R K L
x : { x // x ∈ S }
P : R[X]
hPmo : Monic P
hProot : eval₂ (algebraMap R { x // x ∈ S }) x P = 0
⊢ eval₂ (algebraMap R L) (↑x) P = 0
rw [← aeval_def, aeval_coe, aeval_def, hProot, ZeroMemClass.coe_zero]