[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
classical
have hi : ∀ x : K, IsIntegral F x := fun x ↦ (isIntegral_algebraMap_iff (algebraMap K L).injective).mp (h.isIntegral _)
refine' le_antisymm (iSup_le _) (iSup_le fun x => adjoin_le_iff.mpr fun y hy => _)
· rintro f _ ⟨x, rfl⟩
  refine' le_iSup (fun x => adjoin F ((minpoly F x).rootSet L)) x (subset_adjoin F ((minpoly F x).rootSet L) _)
  rw [mem_rootSet_of_ne (minpoly.ne_zero (hi x)), AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
    Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
· rw [Polynomial.rootSet, Finset.mem_coe, Multiset.mem_toFinset] at hy 
  let g := (algHomAdjoinIntegralEquiv F (hi x)).symm ⟨y, hy⟩
  refine'
    le_iSup (fun f : K →ₐ[F] L => f.fieldRange) ((g.liftNormal L).comp (toAlgHom F K L))
      ⟨x, (g.liftNormal_commutes L (AdjoinSimple.gen F x)).trans _⟩
  rw [Algebra.id.map_eq_id, RingHom.id_apply]
    -- Porting note: in mathlib3 this next `apply` closed the goal.
        -- Now it can't find a proof by unification, so we have to do it ourselves.
  apply PowerBasis.lift_gen
  change aeval y (minpoly F (AdjoinSimple.gen F x)) = 0
  exact minpoly_gen (hi x) ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
have hi : ∀ x : K, IsIntegral F x := fun x ↦ (isIntegral_algebraMap_iff (algebraMap K L).injective).mp (h.isIntegral _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
⊢ restrictScalars F (normalClosure F K L) = ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
refine' le_antisymm (iSup_le _) (iSup_le fun x => adjoin_le_iff.mpr fun y hy => _)
[GOAL]
case refine'_1
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
⊢ ∀ (i : K →ₐ[F] L), AlgHom.fieldRange i ≤ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
rintro f _ ⟨x, rfl⟩
[GOAL]
case refine'_1.intro
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
f : K →ₐ[F] L
x : K
⊢ ↑↑f x ∈ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L)
[PROOFSTEP]
refine' le_iSup (fun x => adjoin F ((minpoly F x).rootSet L)) x (subset_adjoin F ((minpoly F x).rootSet L) _)
[GOAL]
case refine'_1.intro
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
f : K →ₐ[F] L
x : K
⊢ ↑↑f x ∈ rootSet (minpoly F x) L
[PROOFSTEP]
rw [mem_rootSet_of_ne (minpoly.ne_zero (hi x)), AlgHom.toRingHom_eq_coe, AlgHom.coe_toRingHom,
  Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ rootSet (minpoly F x) L
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
rw [Polynomial.rootSet, Finset.mem_coe, Multiset.mem_toFinset] at hy 
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
let g := (algHomAdjoinIntegralEquiv F (hi x)).symm ⟨y, hy⟩
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ y ∈ ↑(restrictScalars F (normalClosure F K L))
[PROOFSTEP]
refine'
  le_iSup (fun f : K →ₐ[F] L => f.fieldRange) ((g.liftNormal L).comp (toAlgHom F K L))
    ⟨x, (g.liftNormal_commutes L (AdjoinSimple.gen F x)).trans _⟩
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(algebraMap L L) (↑g (AdjoinSimple.gen F x)) = y
[PROOFSTEP]
rw [Algebra.id.map_eq_id, RingHom.id_apply]
  -- Porting note: in mathlib3 this next `apply` closed the goal.
      -- Now it can't find a proof by unification, so we have to do it ourselves.
[GOAL]
case refine'_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑g (AdjoinSimple.gen F x) = y
[PROOFSTEP]
apply PowerBasis.lift_gen
[GOAL]
case refine'_2.hy
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(aeval
          ↑(↑(Equiv.subtypeEquiv (Equiv.refl L)
                    (_ :
                      ∀ (x_1 : L),
                        ↑(aeval x_1) (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen) = 0 ↔
                          ↑(Equiv.refl L) x_1 ∈
                            roots
                              (Polynomial.map (algebraMap F L)
                                (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen)))).symm
              (↑(Equiv.subtypeEquiv (Equiv.refl L)
                      (_ :
                        ∀ (x_1 : L),
                          x_1 ∈
                              roots
                                (Polynomial.map (algebraMap F L)
                                  (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen)) ↔
                            ↑(Equiv.refl L) x_1 ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x)))).symm
                { val := y, property := hy })))
      (minpoly F (adjoin.powerBasis (_ : IsIntegral F x)).gen) =
    0
[PROOFSTEP]
change aeval y (minpoly F (AdjoinSimple.gen F x)) = 0
[GOAL]
case refine'_2.hy
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
hi : ∀ (x : K), IsIntegral F x
x : K
y : L
hy : y ∈ roots (Polynomial.map (algebraMap F L) (minpoly F x))
g : (fun x_1 => { x_2 // x_2 ∈ F⟮x⟯ } →ₐ[F] L) { val := y, property := hy } :=
  ↑(algHomAdjoinIntegralEquiv F (_ : IsIntegral F x)).symm { val := y, property := hy }
⊢ ↑(aeval y) (minpoly F (AdjoinSimple.gen F x)) = 0
[PROOFSTEP]
exact minpoly_gen (hi x) ▸ aeval_eq_zero_of_mem_rootSet (Multiset.mem_toFinset.mpr hy)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
⊢ Normal F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
let ϕ := algebraMap K L
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ Normal F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
rw [← IntermediateField.restrictScalars_normal, restrictScalars_eq_iSup_adjoin]
  -- Porting note: use the `(_)` trick to obtain an instance by unification.
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ Normal F { x // x ∈ ⨆ (x : K), adjoin F (rootSet (minpoly F x) L) }
[PROOFSTEP]
apply IntermediateField.normal_iSup (h := _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
⊢ ∀ (i : K), Normal F { x // x ∈ adjoin F (rootSet (minpoly F i) L) }
[PROOFSTEP]
intro x
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
x : K
⊢ Normal F { x_1 // x_1 ∈ adjoin F (rootSet (minpoly F x) L) }
[PROOFSTEP]
apply Normal.of_isSplittingField (p := minpoly F x) (hFEp := _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁶ : Field F
inst✝⁵ : Field K
inst✝⁴ : Field L
inst✝³ : Algebra F K
inst✝² : Algebra F L
inst✝¹ : Algebra K L
inst✝ : IsScalarTower F K L
h : Normal F L
ϕ : K →+* L := algebraMap K L
x : K
⊢ IsSplittingField F { x_1 // x_1 ∈ adjoin F (rootSet (minpoly F x) L) } (minpoly F x)
[PROOFSTEP]
exact
  adjoin_rootSet_isSplittingField
    ((minpoly.eq_of_algebraMap_eq ϕ.injective ((isIntegral_algebraMap_iff ϕ.injective).mp (h.isIntegral (ϕ x)))
          rfl).symm ▸
      h.splits _)
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower F K L
inst✝ : FiniteDimensional F K
⊢ FiniteDimensional F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
haveI : ∀ f : K →ₐ[F] L, FiniteDimensional F f.fieldRange := fun f => f.toLinearMap.finiteDimensional_range
[GOAL]
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field K
inst✝⁵ : Field L
inst✝⁴ : Algebra F K
inst✝³ : Algebra F L
inst✝² : Algebra K L
inst✝¹ : IsScalarTower F K L
inst✝ : FiniteDimensional F K
this : ∀ (f : K →ₐ[F] L), FiniteDimensional F { x // x ∈ AlgHom.fieldRange f }
⊢ FiniteDimensional F { x // x ∈ normalClosure F K L }
[PROOFSTEP]
apply IntermediateField.finiteDimensional_iSup_of_finite
