[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
obtain ⟨α, hα⟩ := @IsCyclic.exists_generator (Units E) _ _
[GOAL]
case intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
use α
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ F⟮↑α⟯ = ⊤
[PROOFSTEP]
apply eq_top_iff.mpr
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
⊢ ⊤ ≤ F⟮↑α⟯
[PROOFSTEP]
rintro x -
[GOAL]
case h
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
⊢ x ∈ F⟮↑α⟯
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : x = 0
⊢ x ∈ F⟮↑α⟯
[PROOFSTEP]
rw [hx]
[GOAL]
case pos
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : x = 0
⊢ 0 ∈ F⟮↑α⟯
[PROOFSTEP]
exact F⟮α.val⟯.zero_mem
[GOAL]
case neg
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
⊢ x ∈ F⟮↑α⟯
[PROOFSTEP]
obtain ⟨n, hn⟩ := Set.mem_range.mp (hα (Units.mk0 x hx))
[GOAL]
case neg.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : (fun x x_1 => x ^ x_1) α n = Units.mk0 x hx
⊢ x ∈ F⟮↑α⟯
[PROOFSTEP]
simp only at hn
[GOAL]
case neg.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x ∈ F⟮↑α⟯
[PROOFSTEP]
rw [show x = α ^ n by norm_cast; rw [hn, Units.val_mk0], Units.val_zpow_eq_zpow_val]
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑(α ^ n)
[PROOFSTEP]
norm_cast
[GOAL]
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ x = ↑(α ^ n)
[PROOFSTEP]
rw [hn, Units.val_mk0]
[GOAL]
case neg.intro
F : Type u_1
inst✝³ : Field F
E : Type u_2
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Finite E
α : Eˣ
hα : ∀ (x : Eˣ), x ∈ Subgroup.zpowers α
x : E
hx : ¬x = 0
n : ℤ
hn : α ^ n = Units.mk0 x hx
⊢ ↑α ^ n ∈ F⟮↑α⟯
[PROOFSTEP]
exact zpow_mem (mem_adjoin_simple_self F (E := E) ↑α) n
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
let sf := (f.map ϕ).roots
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
let sg := (g.map ϕ).roots
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
let s := (sf.bind fun α' => sg.map fun β' => -(α' - α) / (β' - β)).toFinset
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
s : Finset E := Multiset.toFinset (Multiset.bind sf fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg)
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
let s' := s.preimage ϕ fun x _ y _ h => ϕ.injective h
[GOAL]
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
s : Finset E := Multiset.toFinset (Multiset.bind sf fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg)
s' : Finset F := Finset.preimage s ↑ϕ (_ : ∀ (x : F), x ∈ ↑ϕ ⁻¹' ↑s → ∀ (y : F), y ∈ ↑ϕ ⁻¹' ↑s → ↑ϕ x = ↑ϕ y → x = y)
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
obtain ⟨c, hc⟩ := Infinite.exists_not_mem_finset s'
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
s : Finset E := Multiset.toFinset (Multiset.bind sf fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg)
s' : Finset F := Finset.preimage s ↑ϕ (_ : ∀ (x : F), x ∈ ↑ϕ ⁻¹' ↑s → ∀ (y : F), y ∈ ↑ϕ ⁻¹' ↑s → ↑ϕ x = ↑ϕ y → x = y)
c : F
hc : ¬c ∈ s'
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
simp_rw [Finset.mem_preimage, Multiset.mem_toFinset, Multiset.mem_bind, Multiset.mem_map] at hc
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
s : Finset E := Multiset.toFinset (Multiset.bind sf fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg)
s' : Finset F := Finset.preimage s ↑ϕ (_ : ∀ (x : F), x ∈ ↑ϕ ⁻¹' ↑s → ∀ (y : F), y ∈ ↑ϕ ⁻¹' ↑s → ↑ϕ x = ↑ϕ y → x = y)
c : F
hc : ¬∃ a, a ∈ roots (Polynomial.map ϕ f) ∧ ∃ a_1, a_1 ∈ roots (Polynomial.map ϕ g) ∧ -(a - α) / (a_1 - β) = ↑ϕ c
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
push_neg at hc
[GOAL]
case intro
F : Type u_1
inst✝² : Field F
inst✝¹ : Infinite F
E : Type u_2
inst✝ : Field E
ϕ : F →+* E
α β : E
f g : F[X]
sf : Multiset E := roots (Polynomial.map ϕ f)
sg : Multiset E := roots (Polynomial.map ϕ g)
s : Finset E := Multiset.toFinset (Multiset.bind sf fun α' => Multiset.map (fun β' => -(α' - α) / (β' - β)) sg)
s' : Finset F := Finset.preimage s ↑ϕ (_ : ∀ (x : F), x ∈ ↑ϕ ⁻¹' ↑s → ∀ (y : F), y ∈ ↑ϕ ⁻¹' ↑s → ↑ϕ x = ↑ϕ y → x = y)
c : F
hc :
  ∀ (a : E),
    a ∈ roots (Polynomial.map ϕ f) → ∀ (a_1 : E), a_1 ∈ roots (Polynomial.map ϕ g) → -(a - α) / (a_1 - β) ≠ ↑ϕ c
⊢ ∃ c,
    ∀ (α' : E),
      α' ∈ roots (Polynomial.map ϕ f) → ∀ (β' : E), β' ∈ roots (Polynomial.map ϕ g) → -(α' - α) / (β' - β) ≠ ↑ϕ c
[PROOFSTEP]
exact ⟨c, hc⟩
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
have hα := IsSeparable.isIntegral F α
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
have hβ := IsSeparable.isIntegral F β
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
let f := minpoly F α
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
let g := minpoly F β
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
let ιFE := algebraMap F E
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
let ιEE' := algebraMap E (SplittingField (g.map ιFE))
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
obtain ⟨c, hc⟩ := primitive_element_inf_aux_exists_c (ιEE'.comp ιFE) (ιEE' α) (ιEE' β) f g
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
let γ := α + c • β
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
suffices β_in_Fγ : β ∈ F⟮γ⟯
[GOAL]
case intro
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ ∃ γ, F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
use γ
[GOAL]
case h
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮α, β⟯ = F⟮γ⟯
[PROOFSTEP]
apply le_antisymm
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮α, β⟯ ≤ F⟮γ⟯
[PROOFSTEP]
rw [adjoin_le_iff]
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ {α, β} ≤ ↑F⟮γ⟯
[PROOFSTEP]
have α_in_Fγ : α ∈ F⟮γ⟯ := by
  rw [← add_sub_cancel α (c • β)]
  exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ α ∈ F⟮γ⟯
[PROOFSTEP]
rw [← add_sub_cancel α (c • β)]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ α + c • β - c • β ∈ F⟮γ⟯
[PROOFSTEP]
exact F⟮γ⟯.sub_mem (mem_adjoin_simple_self F γ) (F⟮γ⟯.toSubalgebra.smul_mem β_in_Fγ c)
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
⊢ {α, β} ≤ ↑F⟮γ⟯
[PROOFSTEP]
exact fun x hx => by
  -- Porting note: was `by cases hx <;> cases hx <;> cases hx <;> assumption`
  cases' hx with hx hx
  · rwa [← hx] at α_in_Fγ
  · cases hx; norm_cast
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
x : E
hx : x ∈ {α, β}
⊢ x ∈ ↑F⟮γ⟯
[PROOFSTEP]
cases' hx with hx hx
[GOAL]
case inl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
x : E
hx : x = α
⊢ x ∈ ↑F⟮γ⟯
[PROOFSTEP]
rwa [← hx] at α_in_Fγ
[GOAL]
case inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
x : E
hx : x ∈ {β}
⊢ x ∈ ↑F⟮γ⟯
[PROOFSTEP]
cases hx
[GOAL]
case inr.refl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
⊢ β ∈ ↑F⟮γ⟯
[PROOFSTEP]
norm_cast
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ F⟮γ⟯ ≤ F⟮α, β⟯
[PROOFSTEP]
rw [adjoin_simple_le_iff]
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
⊢ γ ∈ F⟮α, β⟯
[PROOFSTEP]
have α_in_Fαβ : α ∈ F⟮α, β⟯ := subset_adjoin F { α, β } (Set.mem_insert α { β })
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fαβ : α ∈ F⟮α, β⟯
⊢ γ ∈ F⟮α, β⟯
[PROOFSTEP]
have β_in_Fαβ : β ∈ F⟮α, β⟯ := subset_adjoin F { α, β } (Set.mem_insert_of_mem α rfl)
[GOAL]
case h.a
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fαβ : α ∈ F⟮α, β⟯
β_in_Fαβ : β ∈ F⟮α, β⟯
⊢ γ ∈ F⟮α, β⟯
[PROOFSTEP]
exact F⟮α, β⟯.add_mem α_in_Fαβ (F⟮α, β⟯.smul_mem β_in_Fαβ)
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
let p :=
  EuclideanDomain.gcd ((f.map (algebraMap F F⟮γ⟯)).comp (C (AdjoinSimple.gen F γ) - (C ↑c : F⟮γ⟯[X]) * X))
    (g.map (algebraMap F F⟮γ⟯))
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
let h := EuclideanDomain.gcd ((f.map ιFE).comp (C γ - C (ιFE c) * X)) (g.map ιFE)
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
have map_g_ne_zero : g.map ιFE ≠ 0 := map_ne_zero (minpoly.ne_zero hβ)
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
have h_ne_zero : h ≠ 0 := mt EuclideanDomain.gcd_eq_zero_iff.mp (not_and.mpr fun _ => map_g_ne_zero)
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
suffices p_linear : p.map (algebraMap F⟮γ⟯ E) = C h.leadingCoeff * (X - C β)
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
have finale : β = algebraMap F⟮γ⟯ E (-p.coeff 0 / p.coeff 1) :=
  by
  rw [map_div₀, RingHom.map_neg, ← coeff_map, ← coeff_map, p_linear]
    -- Porting note: had to add `-map_add` to avoid going in the wrong direction.
  simp [mul_sub, coeff_C, mul_div_cancel_left β (mt leadingCoeff_eq_zero.mp h_ne_zero), -map_add]
    -- Porting note: an alternative solution is:
          -- simp_rw [Polynomial.coeff_C_mul, Polynomial.coeff_sub, mul_sub,
          --   Polynomial.coeff_X_zero, Polynomial.coeff_X_one, mul_zero, mul_one, zero_sub, neg_neg,
          --   Polynomial.coeff_C, eq_self_iff_true, Nat.one_ne_zero, if_true, if_false, mul_zero,
          --   sub_zero, mul_div_cancel_left β (mt leadingCoeff_eq_zero.mp h_ne_zero)]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
⊢ β = ↑(algebraMap { x // x ∈ F⟮γ⟯ } E) (-coeff p 0 / coeff p 1)
[PROOFSTEP]
rw [map_div₀, RingHom.map_neg, ← coeff_map, ← coeff_map, p_linear]
  -- Porting note: had to add `-map_add` to avoid going in the wrong direction.
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
⊢ β = -coeff (↑C (leadingCoeff h) * (X - ↑C β)) 0 / coeff (↑C (leadingCoeff h) * (X - ↑C β)) 1
[PROOFSTEP]
simp [mul_sub, coeff_C, mul_div_cancel_left β (mt leadingCoeff_eq_zero.mp h_ne_zero), -map_add]
  -- Porting note: an alternative solution is:
        -- simp_rw [Polynomial.coeff_C_mul, Polynomial.coeff_sub, mul_sub,
        --   Polynomial.coeff_X_zero, Polynomial.coeff_X_one, mul_zero, mul_one, zero_sub, neg_neg,
        --   Polynomial.coeff_C, eq_self_iff_true, Nat.one_ne_zero, if_true, if_false, mul_zero,
        --   sub_zero, mul_div_cancel_left β (mt leadingCoeff_eq_zero.mp h_ne_zero)]
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
finale : β = ↑(algebraMap { x // x ∈ F⟮γ⟯ } E) (-coeff p 0 / coeff p 1)
⊢ β ∈ F⟮γ⟯
[PROOFSTEP]
rw [finale]
[GOAL]
case β_in_Fγ
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
p_linear : Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
finale : β = ↑(algebraMap { x // x ∈ F⟮γ⟯ } E) (-coeff p 0 / coeff p 1)
⊢ ↑(algebraMap { x // x ∈ F⟮γ⟯ } E) (-coeff p 0 / coeff p 1) ∈ F⟮γ⟯
[PROOFSTEP]
exact Subtype.mem (-p.coeff 0 / p.coeff 1)
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
[PROOFSTEP]
have h_sep : h.Separable := separable_gcd_right _ (IsSeparable.separable F β).map
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
[PROOFSTEP]
have h_root : h.eval β = 0 := by
  apply eval_gcd_eq_zero
  ·
    rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map, ← aeval_def, ← Algebra.smul_def,
      add_sub_cancel, minpoly.aeval]
  · rw [eval_map, ← aeval_def, minpoly.aeval]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
⊢ eval β h = 0
[PROOFSTEP]
apply eval_gcd_eq_zero
[GOAL]
case hf
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
⊢ eval β (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) = 0
[PROOFSTEP]
rw [eval_comp, eval_sub, eval_mul, eval_C, eval_C, eval_X, eval_map, ← aeval_def, ← Algebra.smul_def, add_sub_cancel,
  minpoly.aeval]
[GOAL]
case hg
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
⊢ eval β (Polynomial.map ιFE g) = 0
[PROOFSTEP]
rw [eval_map, ← aeval_def, minpoly.aeval]
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
[PROOFSTEP]
have h_splits : Splits ιEE' h := splits_of_splits_gcd_right ιEE' map_g_ne_zero (SplittingField.splits _)
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
[PROOFSTEP]
have h_roots : ∀ x ∈ (h.map ιEE').roots, x = ιEE' β :=
  by
  intro x hx
  rw [mem_roots_map h_ne_zero] at hx
  specialize
    hc (ιEE' γ - ιEE' (ιFE c) * x)
      (by
        have f_root := root_left_of_root_gcd hx
        rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
        exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
  specialize
    hc x
      (by
        rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
        exact root_right_of_root_gcd hx)
  by_contra a
  apply hc
  apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
  simp only [Algebra.smul_def, RingHom.map_add, RingHom.map_mul, RingHom.comp_apply]
  ring
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
⊢ ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
[PROOFSTEP]
intro x hx
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : x ∈ roots (Polynomial.map ιEE' h)
⊢ x = ↑ιEE' β
[PROOFSTEP]
rw [mem_roots_map h_ne_zero] at hx
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
⊢ x = ↑ιEE' β
[PROOFSTEP]
specialize
  hc (ιEE' γ - ιEE' (ιFE c) * x)
    (by
      have f_root := root_left_of_root_gcd hx
      rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
      exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root)
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
⊢ ↑ιEE' γ - ↑ιEE' (↑ιFE c) * x ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f)
[PROOFSTEP]
have f_root := root_left_of_root_gcd hx
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
f_root : eval₂ ιEE' x (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) = 0
⊢ ↑ιEE' γ - ↑ιEE' (↑ιFE c) * x ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f)
[PROOFSTEP]
rw [eval₂_comp, eval₂_sub, eval₂_mul, eval₂_C, eval₂_C, eval₂_X, eval₂_map] at f_root
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
f_root : eval₂ (RingHom.comp ιEE' ιFE) (↑ιEE' γ - ↑ιEE' (↑ιFE c) * x) f = 0
⊢ ↑ιEE' γ - ↑ιEE' (↑ιFE c) * x ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f)
[PROOFSTEP]
exact (mem_roots_map (minpoly.ne_zero hα)).mpr f_root
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc :
  ∀ (β' : SplittingField (Polynomial.map ιFE g)),
    β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
      -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
⊢ x = ↑ιEE' β
[PROOFSTEP]
specialize
  hc x
    (by
      rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
      exact root_right_of_root_gcd hx)
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc :
  ∀ (β' : SplittingField (Polynomial.map ιFE g)),
    β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
      -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
⊢ x ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g)
[PROOFSTEP]
rw [mem_roots_map (minpoly.ne_zero hβ), ← eval₂_map]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc :
  ∀ (β' : SplittingField (Polynomial.map ιFE g)),
    β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
      -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
⊢ eval₂ ιEE' x (Polynomial.map ιFE (minpoly F β)) = 0
[PROOFSTEP]
exact root_right_of_root_gcd hx
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc : -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
⊢ x = ↑ιEE' β
[PROOFSTEP]
by_contra a
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc : -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
a : ¬x = ↑ιEE' β
⊢ False
[PROOFSTEP]
apply hc
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc : -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
a : ¬x = ↑ιEE' β
⊢ -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) = ↑(RingHom.comp ιEE' ιFE) c
[PROOFSTEP]
apply (div_eq_iff (sub_ne_zero.mpr a)).mpr
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc : -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
a : ¬x = ↑ιEE' β
⊢ -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) = ↑(RingHom.comp ιEE' ιFE) c * (x - ↑ιEE' β)
[PROOFSTEP]
simp only [Algebra.smul_def, RingHom.map_add, RingHom.map_mul, RingHom.comp_apply]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
x : SplittingField (Polynomial.map ιFE g)
hx : eval₂ ιEE' x h = 0
hc : -(↑ιEE' γ - ↑ιEE' (↑ιFE c) * x - ↑ιEE' α) / (x - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
a : ¬x = ↑ιEE' β
⊢ -(↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) α +
            ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) (↑(algebraMap F E) c) *
              ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) β -
          ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) (↑(algebraMap F E) c) * x -
        ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) α) =
    ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) (↑(algebraMap F E) c) *
      (x - ↑(algebraMap E (SplittingField (Polynomial.map (algebraMap F E) (minpoly F β)))) β)
[PROOFSTEP]
ring
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = ↑C (leadingCoeff h) * (X - ↑C β)
[PROOFSTEP]
rw [← eq_X_sub_C_of_separable_of_root_eq h_sep h_root h_splits h_roots]
[GOAL]
case p_linear
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = h
[PROOFSTEP]
trans EuclideanDomain.gcd (?_ : E[X]) (?_ : E[X])
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E) p = EuclideanDomain.gcd ?p_linear.p_linear_1 ?p_linear.p_linear_2
[PROOFSTEP]
dsimp only
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ Polynomial.map (algebraMap { x // x ∈ F⟮α + c • β⟯ } E)
      (EuclideanDomain.gcd
        (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F α))
          (↑C (AdjoinSimple.gen F (α + c • β)) -
            ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮α + c • β⟯) } * X))
        (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F β))) =
    EuclideanDomain.gcd ?p_linear.p_linear_1 ?p_linear.p_linear_2
[PROOFSTEP]
convert (gcd_map (algebraMap F⟮γ⟯ E)).symm
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ EuclideanDomain.gcd
      (Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E)
        (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F α))
          (↑C (AdjoinSimple.gen F (α + c • β)) -
            ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮α + c • β⟯) } * X)))
      (Polynomial.map (algebraMap { x // x ∈ F⟮γ⟯ } E)
        (Polynomial.map (algebraMap F { x // x ∈ F⟮α + c • β⟯ }) (minpoly F β))) =
    h
[PROOFSTEP]
simp [map_comp, Polynomial.map_map, ← IsScalarTower.algebraMap_eq]
[GOAL]
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
ϕ : F →+* E
α β : E
inst✝¹ : Algebra F E
inst✝ : IsSeparable F E
hα : IsIntegral F α
hβ : IsIntegral F β
f : F[X] := minpoly F α
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* SplittingField (Polynomial.map ιFE g) := algebraMap E (SplittingField (Polynomial.map ιFE g))
c : F
hc :
  ∀ (α' : SplittingField (Polynomial.map ιFE g)),
    α' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) f) →
      ∀ (β' : SplittingField (Polynomial.map ιFE g)),
        β' ∈ roots (Polynomial.map (RingHom.comp ιEE' ιFE) g) →
          -(α' - ↑ιEE' α) / (β' - ↑ιEE' β) ≠ ↑(RingHom.comp ιEE' ιFE) c
γ : E := α + c • β
p : { x // x ∈ F⟮γ⟯ }[X] :=
  EuclideanDomain.gcd
    (comp (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) f)
      (↑C (AdjoinSimple.gen F γ) - ↑C { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮γ⟯) } * X))
    (Polynomial.map (algebraMap F { x // x ∈ F⟮γ⟯ }) g)
h : E[X] := EuclideanDomain.gcd (comp (Polynomial.map ιFE f) (↑C γ - ↑C (↑ιFE c) * X)) (Polynomial.map ιFE g)
map_g_ne_zero : Polynomial.map ιFE g ≠ 0
h_ne_zero : h ≠ 0
h_sep : Separable h
h_root : eval β h = 0
h_splits : Splits ιEE' h
h_roots : ∀ (x : SplittingField (Polynomial.map ιFE g)), x ∈ roots (Polynomial.map ιEE' h) → x = ↑ιEE' β
⊢ EuclideanDomain.gcd
      (comp (Polynomial.map (algebraMap F E) (minpoly F α))
        (↑C α + ↑C (c • β) -
          ↑C
              (↑(algebraMap { x // x ∈ F⟮α + c • β⟯ } E)
                { val := ↑(algebraMap F E) c, property := (_ : ↑(algebraMap F E) c ∈ F⟮α + c • β⟯) }) *
            X))
      (Polynomial.map (algebraMap F E) (minpoly F β)) =
    EuclideanDomain.gcd
      (comp (Polynomial.map (algebraMap F E) (minpoly F α)) (↑C α + ↑C (c • β) - ↑C (↑(algebraMap F E) c) * X))
      (Polynomial.map (algebraMap F E) (minpoly F β))
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
rcases isEmpty_or_nonempty (Fintype F) with (F_inf | ⟨⟨F_finite⟩⟩)
[GOAL]
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
let P : IntermediateField F E → Prop := fun K => ∃ α : E, F⟮α⟯ = K
[GOAL]
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
have base : P ⊥ := ⟨0, adjoin_zero⟩
[GOAL]
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
have ih : ∀ (K : IntermediateField F E) (x : E), P K → P (K⟮x⟯.restrictScalars F) :=
  by
  intro K β hK
  cases' hK with α hK
  rw [← hK, adjoin_simple_adjoin_simple]
  haveI : Infinite F := isEmpty_fintype.mp F_inf
  cases' primitive_element_inf_aux F α β with γ hγ
  exact ⟨γ, hγ.symm⟩
[GOAL]
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
⊢ ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
[PROOFSTEP]
intro K β hK
[GOAL]
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β : E
hK : P K
⊢ P (restrictScalars F { x // x ∈ K }⟮β⟯)
[PROOFSTEP]
cases' hK with α hK
[GOAL]
case intro
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P (restrictScalars F { x // x ∈ K }⟮β⟯)
[PROOFSTEP]
rw [← hK, adjoin_simple_adjoin_simple]
[GOAL]
case intro
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
⊢ P F⟮α, β⟯
[PROOFSTEP]
haveI : Infinite F := isEmpty_fintype.mp F_inf
[GOAL]
case intro
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
⊢ P F⟮α, β⟯
[PROOFSTEP]
cases' primitive_element_inf_aux F α β with γ hγ
[GOAL]
case intro.intro
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
K : IntermediateField F E
β α : E
hK : F⟮α⟯ = K
this : Infinite F
γ : E
hγ : F⟮α, β⟯ = F⟮γ⟯
⊢ P F⟮α, β⟯
[PROOFSTEP]
exact ⟨γ, hγ.symm⟩
[GOAL]
case inl
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_inf : IsEmpty (Fintype F)
P : IntermediateField F E → Prop := fun K => ∃ α, F⟮α⟯ = K
base : P ⊥
ih : ∀ (K : IntermediateField F E) (x : E), P K → P (restrictScalars F { x // x ∈ K }⟮x⟯)
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
exact induction_on_adjoin P base ih ⊤
[GOAL]
case inr.intro
F : Type u_1
E : Type u_2
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
inst✝¹ : FiniteDimensional F E
inst✝ : IsSeparable F E
F_finite : Fintype F
⊢ ∃ α, F⟮α⟯ = ⊤
[PROOFSTEP]
exact exists_primitive_element_of_finite_bot F E
[GOAL]
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁷ : Field F
inst✝⁶ : Field E
inst✝⁵ : Field K
inst✝⁴ : IsAlgClosed K
inst✝³ : Algebra F E
inst✝² : FiniteDimensional F E
inst✝¹ : IsSeparable F E
inst✝ : Algebra F K
⊢ Fintype.card (E →ₐ[F] K) = finrank F E
[PROOFSTEP]
convert
  (AlgHom.card_of_powerBasis (L := K) (Field.powerBasisOfFiniteOfSeparable F E) (IsSeparable.separable _ _)
        (IsAlgClosed.splits_codomain _)).trans
    (PowerBasis.finrank _).symm