case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
⊢ Normal F E

case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
⊢ Normal F E
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
⊢ Normal F E
rcases eq_or_ne p 0 with (rfl | hp)
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
⊢ Normal F E
refine' normal_iff.2 fun x => _
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
have hFE : FiniteDimensional F E := IsSplittingField.finiteDimensional E p
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
have Hx : IsIntegral F x := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) x
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
⊢ ∀ {g : E[X]}, Irreducible g → g ∣ map (algebraMap F E) (minpoly F x) → degree g = 1
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
⊢ IsIntegral F x ∧ Splits (algebraMap F E) (minpoly F x)
refine' ⟨Hx, Or.inr _⟩
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
⊢ degree q = 1
case inr
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
⊢ ∀ {g : E[X]}, Irreducible g → g ∣ map (algebraMap F E) (minpoly F x) → degree g = 1
rintro q q_irred ⟨r, hr⟩
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
⊢ degree q = 1
let D := AdjoinRoot q
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this : Fact (Irreducible q)
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
⊢ degree q = 1
haveI := Fact.mk q_irred
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this : Fact (Irreducible q)
⊢ degree q = 1
let pbED := AdjoinRoot.powerBasis q_irred.ne_zero
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this : FiniteDimensional E D
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
⊢ degree q = 1
haveI : FiniteDimensional E D := PowerBasis.finiteDimensional pbED
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this : FiniteDimensional E D
⊢ degree q = 1
have finrankED : FiniteDimensional.finrank E D = q.natDegree := by
  rw [PowerBasis.finrank pbED, AdjoinRoot.powerBasis_dim]
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
⊢ degree q = 1
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
⊢ degree q = 1
haveI : FiniteDimensional F D := FiniteDimensional.trans F E D
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ degree q = 1

F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
⊢ Nonempty (D →ₐ[F] E)
case inr.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
⊢ degree q = 1
rsuffices ⟨ϕ⟩ : Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
⊢ Nonempty (D →ₐ[F] E)
let C := AdjoinRoot (minpoly F x)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
⊢ Nonempty (D →ₐ[F] E)
haveI Hx_irred := Fact.mk (minpoly.irreducible Hx)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
⊢ Nonempty (D →ₐ[F] E)
have heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0 := by
  rw [algebraMap_eq F E D, ← eval₂_map, hr, AdjoinRoot.algebraMap_eq, eval₂_mul,
    AdjoinRoot.eval₂_root, MulZeroClass.zero_mul]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝² : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝¹ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
⊢ Nonempty (D →ₐ[F] E)
letI : Algebra C D :=
  RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝³ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝² : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝¹ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝² : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝¹ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
⊢ Nonempty (D →ₐ[F] E)
letI : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (minpoly.aeval F x))
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁴ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝³ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝² : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝¹ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this : IsScalarTower F C D
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝³ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝² : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝¹ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
⊢ Nonempty (D →ₐ[F] E)
haveI : IsScalarTower F C D := of_algebraMap_eq fun y => (AdjoinRoot.lift_of heval).symm
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
⊢ Nonempty (D →ₐ[F] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁴ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝³ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝² : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝¹ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this : IsScalarTower F C D
⊢ Nonempty (D →ₐ[F] E)
haveI : IsScalarTower F C E := by
  refine' of_algebraMap_eq fun y => (AdjoinRoot.lift_of _).symm
rw [← aeval_def, minpoly.aeval]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
⊢ Nonempty (D →ₐ[C] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
⊢ Nonempty (D →ₐ[F] E)
suffices Nonempty (D →ₐ[C] E) by exact Nonempty.map (AlgHom.restrictScalars F) this
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Nonempty (D →ₐ[C] E)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
⊢ Nonempty (D →ₐ[C] E)
let S : Set D := ((p.map (algebraMap F E)).roots.map (algebraMap E D)).toFinset
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ ⊤ ≤ (IntermediateField.adjoin C S).toSubalgebra
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ ⊤ ≤ IntermediateField.adjoin C S
rw [← IntermediateField.toSubalgebra_le_toSubalgebra, IntermediateField.top_toSubalgebra]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Algebra.adjoin C S ≥ ⊤
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ ⊤ ≤ (IntermediateField.adjoin C S).toSubalgebra
apply ge_trans (IntermediateField.algebra_adjoin_le_adjoin C S)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F (Algebra.adjoin C S) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Algebra.adjoin C S ≥ ⊤
suffices
  (Algebra.adjoin C S).restrictScalars F =
    (Algebra.adjoin E {AdjoinRoot.root q}).restrictScalars F by
  rw [AdjoinRoot.adjoinRoot_eq_top, Subalgebra.restrictScalars_top, ←
    @Subalgebra.restrictScalars_top F C] at this
  exact top_le_iff.mpr (Subalgebra.restrictScalars_injective F this)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin C ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F (Algebra.adjoin C S) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
change Subalgebra.restrictScalars F (Algebra.adjoin C
  (((p.map (algebraMap F E)).roots.map (algebraMap E D)).toFinset : Set D)) = _
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin C (↑(algebraMap E D) '' ↑(Multiset.toFinset (roots (map (algebraMap F E) p))))) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin C ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
rw [← Finset.image_toFinset, Finset.coe_image]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F (Algebra.adjoin E (↑(algebraMap C D) '' {AdjoinRoot.root (minpoly F x)})) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F
      (Algebra.adjoin C (↑(algebraMap E D) '' ↑(Multiset.toFinset (roots (map (algebraMap F E) p))))) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
apply
  Eq.trans
    (Algebra.adjoin_res_eq_adjoin_res F E C D hFEp.adjoin_roots AdjoinRoot.adjoinRoot_eq_top)
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁵ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁴ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝³ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝² : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝¹ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝ : IsScalarTower F C D
this : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
⊢ Subalgebra.restrictScalars F (Algebra.adjoin E (↑(algebraMap C D) '' {AdjoinRoot.root (minpoly F x)})) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
rw [Set.image_singleton, RingHom.algebraMap_toAlgebra, AdjoinRoot.lift_root]
case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F ↑(Multiset.toFinset (roots (map (algebraMap F E) 0))) = ⊤
⊢ Normal F E
case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
⊢ Normal F E
have := hFEp.adjoin_roots
case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E
case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
this : Algebra.adjoin F ↑(Multiset.toFinset (roots (map (algebraMap F E) 0))) = ⊤
⊢ Normal F E
simp only [Polynomial.map_zero, roots_zero, Multiset.toFinset_zero, Finset.coe_empty,
  Algebra.adjoin_empty] at this
no goals
case inl
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
hFEp : IsSplittingField F E 0
this : ⊥ = ⊤
⊢ Normal F E
exact
  Normal.of_algEquiv
    (AlgEquiv.ofBijective (Algebra.ofId F E) (Algebra.bijective_algebraMap_iff.2 this.symm))
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this : FiniteDimensional E D
⊢ FiniteDimensional.finrank E D = natDegree q
rw [PowerBasis.finrank pbED, AdjoinRoot.powerBasis_dim]
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ degree q = ↑1
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ degree q = 1
change degree q = ↑(1 : ℕ)
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ FiniteDimensional.finrank E D = 1
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ degree q = ↑1
rw [degree_eq_iff_natDegree_eq q_irred.ne_zero, ← finrankED]
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
nat_lemma : ∀ (a b c : ℕ), a * b = c → c ≤ a → 0 < c → b = 1
⊢ FiniteDimensional.finrank E D = 1
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ FiniteDimensional.finrank E D = 1
have nat_lemma : ∀ a b c : ℕ, a * b = c → c ≤ a → 0 < c → b = 1 := by
  intro a b c h1 h2 h3
  nlinarith
no goals
case inr.intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
nat_lemma : ∀ (a b c : ℕ), a * b = c → c ≤ a → 0 < c → b = 1
⊢ FiniteDimensional.finrank E D = 1
exact
  nat_lemma _ _ _ (FiniteDimensional.finrank_mul_finrank F E D)
    (LinearMap.finrank_le_finrank_of_injective
      (show Function.Injective ϕ.toLinearMap from ϕ.toRingHom.injective))
    FiniteDimensional.finrank_pos
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
a b c : ℕ
h1 : a * b = c
h2 : c ≤ a
h3 : 0 < c
⊢ b = 1
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
⊢ ∀ (a b c : ℕ), a * b = c → c ≤ a → 0 < c → b = 1
intro a b c h1 h2 h3
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
ϕ : D →ₐ[F] E
a b c : ℕ
h1 : a * b = c
h2 : c ≤ a
h3 : 0 < c
⊢ b = 1
nlinarith
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝¹ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
⊢ eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
rw [algebraMap_eq F E D, ← eval₂_map, hr, AdjoinRoot.algebraMap_eq, eval₂_mul,
  AdjoinRoot.eval₂_root, MulZeroClass.zero_mul]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁴ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝³ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝² : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝¹ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this : IsScalarTower F C D
y : F
⊢ eval₂ (algebraMap F E) x (minpoly F x) = 0
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁴ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝³ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝² : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝¹ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this : IsScalarTower F C D
⊢ IsScalarTower F C E
refine' of_algebraMap_eq fun y => (AdjoinRoot.lift_of _).symm
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁴ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝³ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝² : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝¹ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝ : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this : IsScalarTower F C D
y : F
⊢ eval₂ (algebraMap F E) x (minpoly F x) = 0
rw [← aeval_def, minpoly.aeval]
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
this : Nonempty (D →ₐ[C] E)
⊢ Nonempty (D →ₐ[F] E)
exact Nonempty.map (AlgHom.restrictScalars F) this
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
⊢ Nonempty (D →ₐ[C] E)
refine' IntermediateField.algHom_mk_adjoin_splits' (top_le_iff.mp this) fun y hy => _
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
rcases Multiset.mem_map.mp (Multiset.mem_toFinset.mp hy) with ⟨z, hz1, hz2⟩
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
have Hz : IsIntegral F z := isIntegral_of_noetherian (IsNoetherian.iff_fg.2 hFE) z
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap C E) (minpoly C y)
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ IsIntegral C y ∧ Splits (algebraMap C E) (minpoly C y)
use
  show IsIntegral C y from
    isIntegral_of_noetherian (IsNoetherian.iff_fg.2 (FiniteDimensional.right F C D)) y
case intro.intro.hf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap C E) (map ?m.151496 (minpoly F z))

case intro.intro.hgf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ minpoly C y ∣ map ?m.151496 (minpoly F z)

F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ F →+* C
case intro.intro
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap C E) (minpoly C y)
apply splits_of_splits_of_dvd (algebraMap C E) (map_ne_zero (minpoly.ne_zero Hz))
case intro.intro.hf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap F E) (minpoly F z)
case intro.intro.hf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap C E) (map ?m.151496 (minpoly F z))
rw [splits_map_iff, ← algebraMap_eq F C E]
no goals
case intro.intro.hf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ Splits (algebraMap F E) (minpoly F z)
exact
  splits_of_splits_of_dvd _ hp hFEp.splits
    (minpoly.dvd F z (Eq.trans (eval₂_eq_eval_map _) ((mem_roots (map_ne_zero hp)).mp hz1)))
case intro.intro.hgf.hp
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ ↑(aeval y) (map (algebraMap F C) (minpoly F z)) = 0
case intro.intro.hgf
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ minpoly C y ∣ map (algebraMap F C) (minpoly F z)
apply minpoly.dvd
no goals
case intro.intro.hgf.hp
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : ⊤ ≤ IntermediateField.adjoin C S
y : D
hy : y ∈ S
z : E
hz1 : z ∈ roots (map (algebraMap F E) p)
hz2 : ↑(algebraMap E D) z = y
Hz : IsIntegral F z
⊢ ↑(aeval y) (map (algebraMap F C) (minpoly F z)) = 0
rw [← hz2, aeval_def, eval₂_map, ← algebraMap_eq F C D, algebraMap_eq F E D, ← hom_eval₂, ←
  aeval_def, minpoly.aeval F z, RingHom.map_zero]
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : Subalgebra.restrictScalars F (Algebra.adjoin C S) = Subalgebra.restrictScalars F ⊤
⊢ Algebra.adjoin C S ≥ ⊤
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this :
  Subalgebra.restrictScalars F (Algebra.adjoin C S) =
    Subalgebra.restrictScalars F (Algebra.adjoin E {AdjoinRoot.root q})
⊢ Algebra.adjoin C S ≥ ⊤
rw [AdjoinRoot.adjoinRoot_eq_top, Subalgebra.restrictScalars_top, ←
  @Subalgebra.restrictScalars_top F C] at this
no goals
F : Type u_1
K : Type ?u.87123
inst✝¹¹ : Field F
inst✝¹⁰ : Field K
inst✝⁹ : Algebra F K
E : Type u_2
inst✝⁸ : Field E
inst✝⁷ : Algebra F E
inst✝⁶ : Algebra K E
inst✝⁵ : IsScalarTower F K E
E' : Type ?u.87603
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : Field E'
inst✝ : Algebra F E'
p : F[X]
hFEp : IsSplittingField F E p
hp : p ≠ 0
x : E
hFE : FiniteDimensional F E
Hx : IsIntegral F x
q : E[X]
q_irred : Irreducible q
r : E[X]
hr : map (algebraMap F E) (minpoly F x) = q * r
D : Type u_2 := AdjoinRoot q
this✝⁶ : Fact (Irreducible q)
pbED : PowerBasis E (AdjoinRoot q) := AdjoinRoot.powerBasis (_ : q ≠ 0)
this✝⁵ : FiniteDimensional E D
finrankED : FiniteDimensional.finrank E D = natDegree q
this✝⁴ : FiniteDimensional F D
C : Type u_1 := AdjoinRoot (minpoly F x)
Hx_irred : Fact (Irreducible (minpoly F x))
heval : eval₂ (algebraMap F D) (AdjoinRoot.root q) (minpoly F x) = 0
this✝³ : Algebra C D := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F D) (AdjoinRoot.root q) heval)
this✝² : Algebra C E := RingHom.toAlgebra (AdjoinRoot.lift (algebraMap F E) x (_ : ↑(aeval x) (minpoly F x) = 0))
this✝¹ : IsScalarTower F C D
this✝ : IsScalarTower F C E
S : Set D := ↑(Multiset.toFinset (Multiset.map (↑(algebraMap E D)) (roots (map (algebraMap F E) p))))
this : Subalgebra.restrictScalars F (Algebra.adjoin C S) = Subalgebra.restrictScalars F ⊤
⊢ Algebra.adjoin C S ≥ ⊤
exact top_le_iff.mpr (Subalgebra.restrictScalars_injective F this)